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.

]]>At a quick glance, your approach seems reminiscent of Penon’s approach to higher categories. Did his work have any influence on yours?

]]>Hi Eric, regarding #20, this sounds interesting. In #14, it was mentioned that one might be able to see the issue around the level of 4-categories. Are you able to say a little bit about that concretely?

Could it not be that the gadgets you define are interesting in their own right?

]]>Also, I submitted an issue on Darin’s github page asking for an example of how to use his definition to define the interchange law. Perhaps a simple example like this will serve to clarify his approach.

]]>Unfortunately, it seems that Paolo’s flaw will turn out to be fatal for my approach, at least in vanilla Martin-Lof type theory. I had a number of possible “quick-fixes” in mind, but working through them in Stockholm with Peter and Guillaume, we could not seem to get any of them to go through. A rough way to describe the problem is that, while my definition generates an infinite number of coherences, these coherences are not “compatible” enough with the coherences of the universe (which is the terminal example of the structure i was trying to axiomatize). In order to make them compatible, we would have to finish the construction of the universe itself and hence we end up with the usual kind of circularity. So it looks bad … :(

]]>Maybe not. All that I am aware of is a Twitter message of his from months ago, where he essentially just pointed to his github repository (and now I don’t find that tweet anymore – not that it would matter much). But he says he is not in academia anymore and didn’t find time to make a prose writeup. Hm.

]]>