--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com.
The isomorphism invariance might be useful when you don't care about the actual stuff you get after transporting. If you have two different definitions of the same set, you can transport its properties along the isomorphism (that you still need to construct). For example, we can define rational numbers in two different ways: as arbitrary quotients and as reduced quotients. Then you can prove that they are isomorphic and that one of them gives you a field. Then you know that the other one is also a field. You may be interested in the actual definitions of the operations, but you dob't usually care about the actual proof of the properties. So, you construct the addition and the multiplication explicitly, but you get proofs that they determine a field "for free" from the other definition. If the proofs for one of the definitions is easier than for the other one, this might be a significant simplification.Regards,Valery Isaev
вс, 3 нояб. 2019 г. в 22:13, Michael Shulman <shu...@sandiego.edu>:
But does univalence a la Book HoTT *actually* make it easier to reason
about such things? It allows us to write "=" rather than "\cong", but
to construct such an equality we have to construct an isomorphism
first, and to *use* such an equality we have to transport along it,
and then we get lots of univalence-redexes that we have to manually
reduce away. My experience formalizing math in HoTT/Coq is that it's
much easier if you *avoid* turning equivalences into equalities except
when absolutely necessary. (I don't have any experience formalizing
math in a cubical proof assistant, but in that case at least you
wouldn't have to manually reduce the univalence-redexes -- although it
seems to me you'd still have to construct the isomorphism before you
can apply univalence to make it an equality.)
>>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
>>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz.
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
But does univalence a la Book HoTT *actually* make it easier to reason
about such things?
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com.
He once told me that he wasn't interested in formalizing his proof of Bloch-Kato, because he was sure it was right. (I should have asked him at the time how he could be so sure!)
It is exactly the interaction between constructivism and univalence which I do not understand well, and I think that a very good way to investigate it would be to do some highly non-constructive modern mathematics in a univalent type theory
Kevin, I would like to second Michael's interest in seeing these 20
commutative diagrams. Moreover, I'd also be very interested in seeing
your "spaghetti code" (quote from the slides of your Big Proof talk): it
seems it should be informative to see where your initial approach went
wrong, and how much these problems and their solution had anything to do
at all with the formal system you were working in. Are your original
files perhaps available somewhere?
--
Nicolas
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz.
On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard
> However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong.
This doesn't really make sense to me; I can't figure out what you mean
by "too strong".
HoTT instead expands the notion of "equality" to
essentially mean "isomorphism" and requires transporting along it as a
nontrivial action. I doubt that that's what you have in mind, but
maybe you could explain what you do mean?
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com.
What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal).
You wrote:
<<Personally, I'm doubtful that one can ascribe any precise meaning to
"canonical isomorphism", and therefore doubtful that one will be able
to implement a computer proof assistant that can distinguish a
"canonical isomorphism" from an arbitrary one. >>
The notion of canonical isomorphism depends obviously on the context.
For example, the "canonical isomorphism"
(AxB)xC = Ax(BxC)
is likely to be the associativity isomorphism.
Maybe AI (deep learning) could be trained
to recognise the correct canonical isomorphism from the context
(=the proof). It may automatise
what is already automatic in our thinking.
Best,
André
________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Tuesday, November 26, 2019 5:18 PM
To: Kevin Buzzard
Cc: Martín Hötzel Escardó; Homotopy Type Theory
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%40mail.gmail.com.
Personally, I'm doubtful that one can ascribe any precise meaning to
"canonical isomorphism",
So writing "x = y" for the identity type is a bit perverse.
People may say, and they have said "but there is no other sensible
notion of equality for such type theories.
That may be so, but because, in any case, *it is not the same
notion of equality*, we should not use the same symbol.
Two mathematical objects are equal if they have the same properties. This is exactly what equals means in HoTT and hence we should use the same symbol and call it equality. Everything else is confusing especially for the newcomer: “we have something in HoTT which is basically equality but we call it by a different name and we use a different symbol”???
Yes, it is different because equality of structures is not a proposition but a structure. But to insist that equality of structure is a proposition is just a confusion of conventional Mathematics.
Independent of conventional Mathematics there is something like a naïve idea of equality which is preformal. And equality in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to objects can be equal?
As far is the notion of “canonical isomorphism”, Kevin is interested in, is concerned, I think this is an intensional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical.
Thorsten
From: <homotopyt...@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo...@gmail.com>
Date: Tuesday, 26 November 2019 at 19:15
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com.
This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.