from Hacker News

A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom

by jessup on 3/1/18, 9:19 PM with 15 comments

• by mbid on 3/2/18, 3:07 AM

  It is misleading to say that elementary toposes/zfc don't have something like identity types. Every elementary topos is locally cartesian closed, and locally cartesian closed categories are (equivalent to) models of extensional Martin-Löf type theory, which is an extension of intensional type theory. Identity types in extensional type theory are responsible for the existence of equalizers in its model categories. Universes in type theory correspond to inaccessible cardinals/Grothendieck universes in ZFC or object classifiers in elementary toposes, at least informally (I doubt there is published work here).

  Thus, the term asserting the univalence axiom corresponds to a certain morphism in an elementary topos with object classifiers. The point is, I guess, that such a morphism exists only in the degenerate topos, i.e. the one equivalent to the single object-single morphism category. Only in higher toposes/categories can non-degenerate examples of the univalence axiom be found.

  It should also be noted that you can already identify isomorphic objects ("types") of 1-categories without much harm. Formally, if you have a contractible groupoid G contained in a category C, then the quotient map C -> C/G that collapses all objects of G onto a single object and all morphisms in G onto the identity at that object is an equivalence of categories. This works in particular if G is given by an isomorphism of distinct objects.

  It still boggles my mind why type theorists think that "function extensionality" and quotients, two entirely 1-categorical concepts, are best treated using homotopy coherent diagrams. And it is unclear since when proving theorems in less generality (because additional axioms are assumed) is considered progress.

• by Jeff_Brown on 3/2/18, 4:42 PM

  Is there any obvious application of this in software design?