Thanks, that's very interesting!
The reason I ask is that I was wondering to what extent the type "A=B"
can be regarded as "a coherent definition of equivalence" alongside
half-adjoint equivalences, maps with contractible fibers, etc. Of
course in some sense it is (even in Book HoTT), since it's equivalent
to Equiv(A,B); but the question is how practical it is -- for
instance, is it reasonable when doing synthetic homotopy theory to
state all equivalences as equalities?
In practice, the way we often construct equivalences is to make them
out of a quasi-inverse pair, and all the standard definitions of
equivalence have the nice property that they remember the two
functions in the quasi-inverse pair judgmentally. My experience with
the HoTT/Coq library is that this property is very useful, which is
one reason we state equivalences as equivalences rather than making
use of univalence to state them as equalities (another reason is that
it avoids "univalence-redexes" all over the theory). Half-adjoint
equivalences have the additional nice property that they remember one
of the homotopies judgmentally, and if you're willing to prove the
coherence 2-path by hand then they can be made to remember both of the
homotopies; this seems to be much less useful than I thought it would
be when we made the choice to use half-adjoint equivalences in the
HoTT/Coq library, but it has proven useful at least once.
So I was wondering to what extent equality of types in cubical type
theory has properties like this. It sounds from what you say like the
answer is "not much". This makes the lack of regularity seem like a
rather more serious problem than I had previously thought.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu