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

[Michael Shulman <shulman@sandiego.edu>]

Thanks for sharing the details, Kevin!

On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard
<kevin.m.buzzard@gmail.com> wrote:
> In HoTT one might naively say that these problems would not arise because isomorphic things are equal.

This thought is indeed too naive, but, I think, not for the reason you
give.  In a non-univalent type theory, you have to prove manually that
everything in sight respects isomorphisms.  This is I think the point
you were making about why the original approach got so messy.  HoTT
does solve this problem: because isomorphisms can be made into
equalities, everything automatically respects isomorphisms.

The problem is that in traditional "Book" HoTT, when you make an
isomorphism into an equality, the original isomorphism is only
remembered "up to homotopy", and then when you apply the transport
across that equality (i.e. you use the fact that everything
automatically respects it), it takes work to prove that what you get
out in fact coincides with what you thought it was supposed to be
(i.e. the result of actually applying the isomorphism you started by
defining).  In fact, dealing with these "univalence-redexes" is so
painful that when formalizing mathematics in Book HoTT we (at least,
in the HoTT/Coq library) generally avoid making isomorphisms into
equalities as much as possible!  The only place you might get some
mileage is when, as Valery pointed out, what you're transporting is
the mere truth of a proposition and so it doesn't matter what the
"result" of the transport is.  So while it might be interesting to try
to formalize schemes in Book HoTT, I wouldn't expect much improvement,
and it's not a project I would wish on anyone.

What I do think would be worth doing and comparing would be to
formalize schemes in some kind of cubical type theory.  In that case,
univalence actually computes and so you can hope that the proof
assistant can actually recover the original isomorphism for you
automatically.  This may not be quite true
(https://groups.google.com/d/topic/homotopytypetheory/wCU0V8RD1LQ/discussion)
but it's much closer to true, and I think it would be extremely
interesting to formalize schemes in a cubical type theory and compare
to your developments.  In a nutshell, one could say that the
composition algorithms of cubical type theory are a generic
implementation of the fact that everything definable in type theory
respects isomorphisms, so that essentially all of the nasty lemmas
should be proven for you already -- with, moreover, the proofs that
you would have given, rather than (as in Book HoTT) a proof that isn't
very useful because it takes a lot of effort to extract the "correct"
proof.

> 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".  It's certainly not inconsistent, since we have
semantic models; in particular, schemes defined in HoTT would
specialize in the simplicial set model to the classical notion of
scheme.  And I can't imagine any way that the presence of univalence
could "get in the way" or "backfire".  Usually when people say that
univalence sounds "wrong", it's because they're thinking of "equality"
as a substitutive mere property and "isomorphic types as equal" as
somehow collapsing to a categorical skeleton, which is of course a
misconception -- 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?

> By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory.

It would be nice if there were a phrase for this that didn't sound
insulting to us "improper" mathematicians.  Mac Lane's similar phrase
"working mathematician" is not really any more flattering to the
"non-working" mathematicians.  (-:

Mike

-- 
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/CAOvivQz3jn5jcjbeeK%2BG2dJ_n_AuZT43pSQ%2Bq5z8Roq_YFzQpw%40mail.gmail.com.