Nathaniel Arkor suggested that info about univalence being consistent with excluded middle be added to this article

]]>I don’t think it’s really correct to cite Hofmann-Streicher for “the univalence axiom”. Their universe extensionality axiom is stated only for a universe of sets, and would be incorrect if generalized naively beyond that domain. I would say they stated a *version* of the univalence axiom that applies to h-sets. Note that the version of the univalence axiom that applies to h-propositions is already true in set theory.

added pointer to:

- Cyril Cohen, Enzo Crance, Assia Mahboubi,
*Trocq: Proof Transfer for Free, With or Without Univalence*, in:*Programming Languages and Systems. ESOP 2024*, Lecture Notes in Computer Science**14576**, Springer (2024) [arXiv:2310.14022, doi:10.1007/978-3-031-57262-3_10]

re #42:

finally found a reference by a type theorist who admits that the univalence axiom is due to Hofmann & Streicher:

- Thorsten Altenkirch,
*Martin Hofmann’s contributions to type theory: Groupoids and univalence*, Mathematical Structures in Computer Science**31**9 (2021) 953-957 [doi:10.1017/S0960129520000316]

(though still without concretely referencing their statement…)

]]>Fix a confusion between retractions and sections.

]]>added pointer to:

- Martín Escardó,
*Voevodsky’s univalence axiom*, §3.11 in:*Introduction to Univalent Foundations of Mathematics with Agda*[arXiv:1911.00580, webpage]

P.S.: Though the section title is debatable: The univalence axiom was stated by Hofmann & Steicher in 1996 (§5.4 p. 23-24) under the name “universe extensionality” (arguably the more appropriate naming). Vladimir’s contribution was not the axiom as such, but to fix a subtlety in the definition of the type of type equivalences.

]]>added pointer to:

]]>After saying (here) that the univalence axiom is “almost” due to Hofman & Streicher, the entry continued to say, somewhat mysteriously, that:

the only difference is the lack of a coherent definition of equivalence.

I have now expanded this out as follows:

]]>The only issue is that these authors refer to a subtly incorrect type of equivalences in homotopy type theory (see there for details).

It is this notion of equivalence in homotopy type theory which was fixed by Vladimir Voevodsky (…reference?), ever since the univalence axiom is widely attributed to him.

separated definitions from its categorical semantics

Anonymous

]]>added an explanation how different notions of sameness of types leads to different notions of univalence

Anonymous

]]>added motivation for the transport definition of univalence: strongly predicative Tarski universes which are not closed under function types.

Anonymous

]]>Added redirect for definitional univalence

Anonymous

]]>Adding section on definitional univalence.

Anonymous

]]>Added link to extensionality

Anonymous

]]>Added redirect for universe extensionality

Anonymous

]]>Adding a section about the relation between univalence and axiom K.

Anonymous

]]>Adding a section on the univalence axiom for Tarski universes and its equivalence to an “external” version of the univalence axiom where the canonical transport function is an equivalence.

Anonymous

]]>I have added pointer to

- Chris Kapulkin, Peter LeFanu Lumsdaine,
*The Simplicial Model of Univalent Foundations (after Voevodsky)*, Journal of the European Mathematical Society**23**(2021) 2071–2126 $[$arXiv:1211.2851, doi:10.4171/jems/1050$]$

and correspondingly expanded the parenthesis below the pointer to Bousfield 06

]]>Thanks!

I have worked that into the list of references, here.

]]>Quote from Voevodsky:

"I have been working on the ideas that led to the discovery of univalent models since 2005 and gave the first public presentation on this subject at Ludwig-Maximilians-Universität München in November 2009. While I have constructed my models independently, advances in this direction started to appear as early as 1995 and are associated with Martin Hofmann, Thomas Streicher, Steve Awodey, and Michael Warren."

However, the date of birth of univalence is arguably May 1st 2006, since this is when Bousfield sketched a proof of a baby version of it (express any homotopy equivalence between two Kan complexes as a Kan fibration to \Delta^1). Grayson did post a copy of a series of E-mail exchanges between Voevodsky, Grayson, May and Bousfield here: https://groups.google.com/g/homotopytypetheory/c/K_4bAZEDRvE/m/FSfFdoJ3AAAJ ]]>

After pointing out that the univalence axiom is due to Hofmann and Streicher, the References section here claims that, 7 years later:

The univalence axiom in its modern form was introduced and promoted by Vladimir Voevodsky around 2005. (?)

Can anyone replace that question mark by a pointer?

The next references offered is from 12 years later:

- Vladimir Voevodsky,
*Univalent Foundations Project*, 2010 (pdf)

I have added a remark “see Section 4” to that, but even with such a remark it won’t be easy for outsiders to recognize the description of an axiom in that text.

Digging around on vv’s old webpage, I see that next, 16 years later, there is this, which I have added now:

- Vladimir Voevodsky,
*The equivalence axiom and univalent models of type theory*(Talk at CMU on February 4, 2010) (arXiv:1402.5556)

But again, the uninitiated will have a hard time recognizing the advertized axiom in this text.

If prose is not the venue of choice here, maybe there is a time-stamped Coq-file which one could reference, where the “modern” axiom is first coded.

]]>added publication details and links to:

- Martin Hofmann, Thomas Streicher
*The groupoid interpretation of type theory*, in: Giovanni Sambin et al. (eds.),*Twenty-five years of constructive type theory*, Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ISBN:9780198501275, ps, pdf)

Added pointer to *univalent foundations for mathematics*.

Just to say that Darin has sent a reply

github.com/freebroccolo/agda-nr-cats/issues/4#issuecomment-503789479

to Eric’s request from #21 above.

]]>