RE: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?

["Joyal, André" <joyal.andre@uqam.ca>]

Dear Michael,

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: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@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'?

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.  It's certainly worth
thinking about, but my personal opinion is that instead of designing a
proof assistant to match the way mathematicians think about "canonical
isomorphisms", mathematicians are going to need to change the way they
think.  But it's just a question of going all the way down a road that
they've already taken one step along.

In formal systems like ZFC and Lean, almost no isomorphisms are
equalities.  Being willing to treat "canonical" isomorphisms as
equalities is a first step into the brave new world of homotopy theory
and higher category theory, but it's hard to find a place to stand
when you've only taken that one step.  In trying to make things
precise, I think one feels inexorably pulled to the more consistent,
and formalizable, position that *all* isomorphisms should be treated
as equalities.  It's not the same notion of equality, as Martin says,
but it's a better replacement for it, which in particular can do
everything that the old notion of equality could do when used
"correctly" (e.g. equality of numbers and functions).


On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard
<kevin.m.buzzard@gmail.com> wrote:
>
> Nicolas originally asked
>
> "So, to put this into one concrete question, how (if at all) is HoTT-Coq
> more practical than Mizar for the purpose of formalizing mathematics,
> outside the specific realm of synthetic homotopy theory?"
>
> One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question.
>
> I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). 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).
>
> It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well.
>
> Kevin
>
>
> On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote:
>>
>>
>>
>> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote:
>>>
>>> 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?
>>
>>
>>  I think terminology and notation alone cause a lot of confusion (and I
>> have said this many times in this list in the past, before Kevin joined in).
>>
>> Much of the disagreement is not a real disagreement but a
>> misunderstanding.
>>
>>  * In HoTT, or in univalent mathematics, we use the terminology
>>    "equals" and the notation "=" for something that is not the same
>>    notion as in "traditional mathematics".
>>
>>  * Before the univalence axiom, we had Martin-Loef's identity type.
>>
>>  * It was *intended* to capture equality *as used by mathematicians*
>>    (constructive or not).
>>
>>  * But it didn't. Hofmann and Streicher proved that.
>>
>>  * The identity type captures something else.
>>
>>    It certainly doesn't capture truth-valued equality by default.
>>
>>    In particular, Voevosdky showed that it captures isomorphism of
>>    sets, and more generality equivalence of ∞-groupoids.
>>
>>    But this is distorting history a bit.
>>
>>    In the initial drafts of his "homotopy lambda calculus", he tried
>>    come up with a new construction in type theory to capture
>>    equivalence.
>>
>>    It was only later that he found out that what he needed was
>>    precisely Martin-Loef's identity type.
>>
>>  * 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.
>>
>>  * Similarly, writing "X ≃ Y" is a bit perverse, too.
>>
>>    In truth-valued mathematics, "X ≃ Y" is most of the time intended
>>    to be truth-valued, not set-valued.
>>
>>    (Exception: category theory. E.g. we write a long chain of
>>    isomorphisms to establish that two objects are isomorphic. Then we
>>    learn that the author of such a proof was not interested in the
>>    existence of an isomorphism, but instead to provide an
>>    example. Such a proof/construction is usually concluded by saying
>>    something like "by chasing the isomorphism, we see that we can take
>>    [...] as our desired isomorphism.)
>>
>>
>>  * With the above out of the way, we can consider the imprecise slogan
>>    "isomorphic types are equal".
>>
>>    The one thing that the univalence axiom doesn't say is that
>>    isomorphic type are equal.
>>
>>    What it does say is that the *identity type* Id X Y is in canonical
>>    bijection with the type X ≃ Y of equivalences.
>>
>>  * What is the effect of this?
>>
>>    - That the identity type behaves like isomorphism, rather than like
>>      equality.
>>
>>    - And that isomorphism behaves a little bit like equality.
>>
>>    The important thing above is "a little bit".
>>
>>    In particular, we cannot *substitute* things by isomorphic
>>    things. We can only *transport* them (just like things work as
>>    usual with isomorphisms).
>>
>>  * Usually, the univalence axioms is expressed as a relation between
>>    equality and isomorphism.
>>
>>    Where by equality we don't mean equality but instead the identity
>>    type.
>>
>>    A way to avoid these terminological problems is to formulate
>>    univalence as a property of isomorphisms, or more precisely
>>    equivalences.
>>
>>    To show that all equivalences satisfy a given property, it is
>>    enough to prove that all the identity equivalence between any two
>>    types have this property.
>>
>>  * So, as Mike says above, most of the time we can work with type
>>    equivalence rather than "type equality". And I do too.
>>
>>    Something that is not well explained at all in the literature is
>>    when and how the univalence axiom *actually makes a difference*.
>>
>>    (I guess this is not well understood. I used to thing that the
>>    univalence axioms makes a difference only for types that are not
>>    sets. But actually, for example, the univalence axiom is needed (in
>>    the absence of the K axiom) to prove that the type of ordinals is a
>>    set.)
>>
>>       * One example: object classifiers, subtype classifiers, ...
>>
>>  * Sometimes the univalence axiom may be *convenient* but *not needed*.
>>
>>    I guess that Kevin is, in particular, saying precisely that. In all
>>    cases where he needs to transport constructions along isomorphisms,
>>    he is confident that this can be done without univalence. And I
>>    would agree with this assessment.
>>
>> Best,
>> Martin
>>
>>
>>
>>
>> --
>> 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+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.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+unsubscribe@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652BA70E%40Pli.gst.uqam.ca.