re #42:
finally found a reference by a type theorist who admits that the univalence axiom is due to Hofmann & Streicher:
(though still without concretely referencing their statement…)
]]>Fix a confusion between retractions and sections.
]]>added pointer to:
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
and correspondingly expanded the parenthesis below the pointer to Bousfield 06
]]>Thanks!
I have worked that into the list of references, here.
]]>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:
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:
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:
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.
]]>