2
$\begingroup$

I have heard that Homotopy Type Theory makes it so that isomorphic objects are “equal”. I wonder how this squares with a lot of mathematical examples from Algebra and Set Theory, where the nature of the isomorphism, or a certain class of isomorphisms, and how they interact with other morphisms, is relevant. How can you do any of this math if you just say “isomorphic objects are equal” and that’s that?

$\endgroup$
2

2 Answers 2

2
$\begingroup$

In type theory identity types are allowed to have more than one element. Univalence implies that the type of proofs that two structures are equal is equivalent to the type of isomorphisms between them. This more careful phrasing is consistent with the fact that the set of isomorphisms is non trivial. E.g. if there are many isomorphisms between two structures, then the identity type will have multiple distinct elements (exactly one for each isomorphism).

$\endgroup$
0
$\begingroup$

An equivalence relation in a theory can be called 'equality' when it satisfies the classical principle of "Indiscernability of identicals", that is to say, for our purpose, the "Indiscernability of equivalent objects".

With the way type equivalence is defined in Homotopy Type Theory, "the nature of isomorphisms" is unchanged. But the theory is built so that we have an indiscernability of equivalent types, and therefore type equivalence is, in this theory, a type equality.

More accurately, the HoTT book axiomatizes first identity types, that define a type equality. Type equivalence is then defined based on identity types, and, without the Univalence axiom, it almost satisfies the property of "indiscernability of equivalent types", with the exception of the reflexivity constructor of type identity, that is "too strict". The Univalence axiom introduces a sort of "alternative constructor" for type identity, making it less strict, more rich, so that type equivalence now satisfies the criteria of "indiscernibility of equivalent types", and therefore becomes a type equality. Moreover, the univalence axiom ensures that the two resulting concepts of equality, namely type identity and type equivalence, are themselves... equivalent!

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .