Introduction E9F5FC

Questions FFFFC0

• View
• Edit
• History
• Print

维基百科

• Univalent foundations
• Univalence Axiom

读物

• Based on the work of Escardo, and applying Coquand’s technique of reducing the J-rule to the transport and the contractibility of singleton types, we derive the univalence axiom from its Yoneda lemma-formulation.
• Escardo has derived the J-rule from Rijke’s type-theoretic formulation of the Yoneda lemma.
• Rijke has given a type-theoretic formulation of the Yoneda lemma and a proof of it from Martin-L ̈of’s J-rule and the function extensionality axiom.

Ahrens, Kapulkin, Shulman. Univalent categories and the Rezk completion

• They define "saturated" or "univalent" categories for which equality and equivalence of categories agree. They satisfy a version of the Univalence Axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects.
• nLab: Rezk completion
• nLab: Complete Segal space

HoTT Book, page 172: In category theory, the Yoneda lemma tells us that for any category {$A$} and object {$a_0$}, the functor freely generated by an element of {$F(a_0)$} is the representable functor {$\textrm{hom}A(a_0, – )$}. Thus, we should expect the identity type {$(a_0 =A – )$} to be this representable functor, and this is indeed exactly how we view it: {$(a0 =A b)$} is the space of morphisms (paths) in {$A$} from {$a_0$} to {$b$}.

HoTT Book (back cover): The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the “official” doctrines of conventional foundations.

HoTT Book, page 4: The univalence axiom also further strengthens the homotopical view of type theory, since it holds in the simplicial model and other related models, while failing under the view of types as sets.

• Voevodsky constructed an interpretation of type theory in Kan simplicial sets, and recognized that this interpretation satisfied a further crucial property which he dubbed univalence.
  • Church’s principle of extensionality for propositions turns out to be a very special case of it
  • Hofmann and Streicher had considered another special case under the name “universe extensionality”.

HoTT Book, pages 4-5: The basic idea of the univalence axiom can be explained as follows. In type theory, one can have a universe type, U , the terms of which are themselves types, A : U , etc. Those types that are terms of U are commonly called small types. Like any type, U has an identity type IdU , which expresses the identity relation A = B between small types. Thinking of types as spaces, U is a space, the points of which are spaces; to understand its identity type, we must ask, what is a path p : A ; B between spaces in U ? The univalence axiom says that such paths correspond to homotopy equivalences A ≃ B, (roughly) as explained above. A bit more precisely, given any (small) types A and B, in addition to the primitive type IdU (A, B) of identifications of A with B, there is the defined type Equiv(A, B) of equivalences from A to B. Since the identity map on any object is an equivalence, there is a canonical map, IdU (A, B) → Equiv(A, B). The univalence axiom states that this map is itself an equivalence. At the risk of oversimplifying, we can state this succinctly as follows: Univalence Axiom: (A = B) ≃ (A ≃ B). In other words, identity is equivalent to equivalence. In particular, one may say that “equivalent types are identical”. However, this phrase is somewhat misleading, since it may sound like a sort of “skeletality” condition which collapses the notion of equivalence to coincide with identity, whereas in fact univalence is about expanding the notion of identity so as to coincide with the (unchanged) notion of equivalence. From the homotopical point of view, univalence implies that spaces of the same homotopy type are connected by a path in the universe U , in accord with the intuition of a classifying space for (small) spaces. From the logical point of view, however, it is a radically new idea: it says that isomorphic things can be identified! Mathematicians are of course used to identifying isomorphic structures in practice, but they generally do so by “abuse of notation”, or some other informal device, knowing that the objects involved are not “really” identical. But in this new foundational scheme, such structures can be formally identified, in the logical sense that every property or construction involving one also applies to the other. Indeed, the identification is now made explicit, and properties and constructions can be systematically transported along it. Moreover, the different ways in which such identifications may be made themselves form a structure that one can (and should!) take into account. Thus in sum, for points A and B of the universe U (i.e., small types), the univalence axiom identifies the following three notions: • (logical) an identification p : A = B of A and B • (topological) a path p : A ; B from A to B in U • (homotopical) an equivalence p : A ≃ B between A and B.

Yoneda lemma in type theory

• Iosif Petrakis. A Yoneda lemma-formulation of the univalence axiom.
• Martin Escardo. Using Yoneda rather than J to present the identity type We take Yoneda as primitive and then construct J (based path induction) from Yoneda, so that its computation rule holds *definitionally*. This is intended to (1) try to explain the identity type to category theorists in familiar terms and (2) try to explain why "defining functions on refl" is enough for defining them on all paths to (pre HoTT/UF) type theorists.
• Egbert Rijke. Yoneda lemma for dependent types
• Egbert Rijke. Yoneda lemma, adjunctions in HoTT theory`
• Martin Escardo. The Yoneda Lemma for types

Discussion at HOTTest Summer School

How are the Univalence Axiom and the Yoneda Lemma related? I asked this question today at the end of the session led by Ulrik. I got some very helpful answers but had trouble writing down and understand everything and I also don't know who said what. The first answer (by Egbert Rijke?) was about the link between identity types and homsets as types on a groupoid and how that relates to embeddings as types. Another answer was about Retz completeness. Another answer related a sum type with the identity. Another answer was that the Univalence Axiom and the Yoneda Lemma are not equivalent in the case when type theory is dealing with sets. A source given was an article by Ahrens, Kapulkin, Shulman, is it this: Univalent categories and the Rezk completion https://arxiv.org/abs/1303.0584 ? Thank you for helping me. I look forward to working to understand this. It is why I am taking this course. I am relating the Yoneda Lemma to four levels of knowledge: Whether, What, How, Why, how it functions as a knowledge switch, how it relates two worldviews: finite automata and pushdown automata.

Ulrik Buchholtz: This notes by @Martin Escardo also discuss some relations of the yoneda lemma for types to univalence, see near the end: https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html

Ulrik Buchholtz: So I think Egbert's answer relates to a blog post of his, https://homotopytypetheory.org/2012/05/02/a-type-theoretical-yoneda-lemma/ – which is the yoneda lemma for dependent types. This is super useful, but as mentioned, not directly related to univalence. Now, if you specialize that to families over the universe, it begins to be more related to univalence, as discussed here by Petrakis: https://www.math.lmu.de/~petrakis/Univalence.pdf

Martin Escardo: Thanks, Ulrik. I also discuss Yoneda here: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#yoneda

Naïm Camille Favier ncfavier: now the η rule for products simply says that applying the universal property to the projections themselves gives us the identity from the product to itself, which i guess might be some form of the yoneda lemma?

• HoTTest Summer School
  • HoTTest: Propositional Truncation
  • HoTTest: The Univalence Axiom
  • HoTTest: Univalent Combinatorics

Licata. Computing with Univalence., Talk

Univalence from a computer science point-of-view - Dan Licata

Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. (Univalent mathematics)