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