Martin Escardo, 7 May 2015. This is a literate Agda file. Using Yoneda rather than J to present the identity type ------------------------------------------------------- Abstract. 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. However, at the moment, this is addressed to HoTT/UF practitioners. Related work. Egbert Rijke formulated and proved the type-theoretical Yoneda Lemma in his master thesis under Andrej Bauer: http://homotopytypetheory.org/2012/05/02/a-type-theoretical-yoneda-lemma/ https://hottheory.files.wordpress.com/2012/08/hott2.pdf (Section 2.8). This gives the construction J ↦ Yoneda. What we show here is the opposite construction Yoneda ↦ J. Remark. This is about HoTT/UF, but we don't use funext, univalence, or any postulate (and we disable K). We work in MLTT with Π, Σ, Id, U. No other type is needed in this discussion. Brief introduction ------------------ Here by the Yoneda Lemma (or rather the Yoneda Construction) we mean a particular equivalence ((y : X) → x = y → A y) ≃ A x for any X:U, x:X, A:X→U. We regard a function with the lhs type as a natural transformation from Id x to A, and we write Nat (Id x) A ≃ A x. Regarding the type X as an ω-groupoid, its identity type is its Hom, and we write the above as Nat (Hom x) A ≃ A x, in more familiar categorical notation. We start from Yoneda, constructed by pattern matching on the identity path. There are only two definitions by pattern matching for this (and pattern matching on the identity path is not used anywhere else in this file). The use of pattern matching rather than J here is deliberate. The path-induction construction J itself is defined by pattern matching in Agda and in MLTT. Here we instead have Yoneda as primitive, defined by pattern matching. We then construct J (based path induction) from Yoneda, so that its computation rule holds *definitionally*. We could of course have used J to derive Yoneda, but we deliberately don't do that, to make the point that it is possible to present identity types via Yoneda rather than path induction J, and then derive J. But both Yoneda and path induction say essentially the same thing, although in significantly different ways, namely that to define something on all paths, it is enough to say what it does to the identity path. We can view path induction as an alternative, type theoretic, presentation of the categorical Yoneda Lemma. We don't advocate that one is better than the other. In fact, both are rather elegant, in different ways, and equally useful. For category theorists that like "just" explanations: Martin-Lӧf's J is just the Yoneda Lemma presented as an induction principle. See also http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda-concise.html http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda2.html Technical exposition -------------------- The elements of the universe U are called (homotopy) types and we regard them as ω-groupoids. In Agda the universe is called Set, but this terminology/notation has its origin before HoTT and univalent foundations. \begin{code} {-# OPTIONS --without-K #-} U = Set U₁ = Set₁ \end{code} The Hom of an ω-groupoid is inductively defined under the traditional (homotopy) type-theoretic view, by specifying only the identity paths. This is justified by Yoneda. We perform this justification "synthetically". \begin{code} data Hom {X : U} : X → X → U where idp : (x : X) → Hom x x \end{code} Hom {X} x y is the hom type of paths from x to y, which is itself another ω-groupoid for every x,y:X. Traditional (homotopy) type theoretic synonyms are the following: \begin{code} Id : {X : U} → X → X → U Id = Hom refl : {X : U} (x : X) → Id x x refl = idp _≡_ : {X : U} → X → X → U x ≡ y = Id x y infix 1 _≡_ \end{code} A "presheaf" on an ω-groupoid X is a function into the universe. It is automatically functorial in the synthetic approach (see the HoTT book). But (perhaps surprisingly) this is not needed here. \begin{code} PrShf : U → U₁ PrShf X = (X → U) \end{code} Nat {X} A B is the type of natural transformations of presheaves on the ω-groupoid X. The naturality of an element of this type is discussed in the HoTT book, but (again perhaps surprisingly) it is not needed here. \begin{code} Nat : {X : U} → PrShf X → PrShf X → U Nat {X} A B = {x : X} → A x → B x \end{code} The following is defined as in the classical (i.e. non-synthetic) case, by applying the natural transformation to the identity: \begin{code} yoneda-elem : {X : U} {x : X} {A : PrShf X} → Nat (Hom x) A → A x yoneda-elem {X} {x} η = η (idp x) \end{code} The following is the first use of pattern matching on the identity path (out of two) in this document, to construct the inverse of the above: \begin{code} yoneda-nat : {X : U} {x : X} {A : PrShf X} → A x → Nat (Hom x) A yoneda-nat a (idp x) = a \end{code} The following is the HoTT synonym of this, with the arguments permuted: \begin{code} transport : {X : U} (A : X → U) {x y : X} → x ≡ y → A x → A y transport {X} A {x} p a = yoneda-nat {X} {x} {A} a p \end{code} The essence of the Yoneda Lemma is that every natural transformation is a transport. This is the second and last use of pattern matching on identity paths in this file: \begin{code} yoneda-lemma : {X : U} {x : X} {A : PrShf X} (η : Nat (Hom x) A) (y : X) (p : x ≡ y) → transport A p (yoneda-elem η) ≡ η p yoneda-lemma η x (idp .x) = idp (yoneda-elem η) \end{code} We could use funext (twice) to get η ≡ yoneda-nat (yoneda-elem η). But we deliberately work in plain MLTT, and in fact in a very spartan subset of it as explained in the introduction. The following is the official formulation, which is definitionally equivalent to the above: \begin{code} yoneda-lemma-official : {X : U} {x : X} {A : PrShf X} (η : Nat (Hom x) A) (y : X) (p : x ≡ y) → yoneda-nat (yoneda-elem η) p ≡ η p yoneda-lemma-official = yoneda-lemma \end{code} The other way round is trivial (it holds definitionally), and is the computation rule for the Yoneda Construction: \begin{code} yoneda-computation : {X : U} {x : X} {A : PrShf X} (a : A x) → yoneda-elem {X} {x} {A} (yoneda-nat a) ≡ a yoneda-computation {X} {x} {A} = idp {A x} \end{code} There are a number of special cases of interest. Path composition, inversion and application are defined from transport (that is, from yoneda-nat): \begin{code} _•_ : {X : U} {x y z : X} → x ≡ y → y ≡ z → x ≡ z p • q = transport (Id _) q p Id⁻¹ : {X : U} → X → X → U Id⁻¹ x y = Id y x _⁻¹ : {X : U} {x y : X} → x ≡ y → y ≡ x p ⁻¹ = transport (Id⁻¹ _) p (idp _) ap : {X Y : U} (f : X → Y) {x y : X} → x ≡ y → f x ≡ f y ap f p = transport (λ y → f _ ≡ f y) p (idp(f _)) \end{code} As in the classical (i.e. non-synthetic) situation, we have that every natural transformation η of representable presheaves is pre-composition with a fixed morphism, that is, a path q in our case, namely q = yoneda-elem η. \begin{code} yoneda-nat' : {X : U} {x y : X} → Hom x y → Nat (Hom y) (Hom x) yoneda-nat' = yoneda-nat yoneda-elem' : {X : U} {x y : X} → Nat (Hom y) (Hom x) → Hom x y yoneda-elem' = yoneda-elem yoneda-lemma' : {X : U} {x y : X} (η : Nat (Hom x) (Hom y)) (u : X) (p : x ≡ u) → (yoneda-elem' η) • p ≡ η p yoneda-lemma' = yoneda-lemma yoneda-computation' : {X : U} {x y : X} (p : Hom x y) → yoneda-elem' {X} {x} {y} (yoneda-nat' p) ≡ p yoneda-computation' {X} {x} a = idp a \end{code} The above is a generalized version of the main lemma in Hedberg's Theorem: \begin{code} hedberg-lemma : {X : U} {x : X} (η : Nat (Hom x) (Hom x)) (y : X) (p : x ≡ y) → (yoneda-elem' η) • p ≡ η p hedberg-lemma = yoneda-lemma \end{code} The following is an alternative construction of the identity type, using the identity type, where path composition becomes simply composition of natural transformations, and hence is definitionally associative with the identity path definitionally its (left and right) neutral element. \begin{code} Id' : {X : U} → X → X → U Id' x y = Nat (Id y) (Id x) idp' : {X : U} (x : X) → Id' x x idp' x p = p _◦_ : {X : U} {A B C : PrShf X} → Nat B C → Nat A B → Nat A C μ ◦ η = λ p → μ (η p) _•'_ : {X : U} {x y z : X} → Id' x y → Id' y z → Id' x z _•'_ = _◦_ -- Cheating (because we chase equivalences): _⁻¹' : {X : U} {x y : X} → Id' x y → Id' y x _⁻¹' {X} {x} {y} η {u} p = transport (Id⁻¹ u) (yoneda-elem' η) p \end{code} To prove (idp x) • p = p, we apply Yoneda to the identity natural transformation. Right neutrality holds definitionally. \begin{code} idp-left-neutral : {X : U} {x y : X} {p : x ≡ y} → (idp x) • p ≡ p idp-left-neutral {X} {x} {y} {p} = yoneda-lemma (idp' x) y p idp-right-neutral : {X : U} {x y : X} (p : x ≡ y) → p ≡ p • (idp y) idp-right-neutral = idp \end{code} Another crucial particular case is when the presheaf A is constant with value B:U. Then every natural tranformation η is constant with value yoneda-elem η. \begin{code} constPrShf : {X : U} → U → PrShf X constPrShf B _ = B yoneda-const : {X B : U} {x : X} (η : Nat (Hom x) (constPrShf B)) (y : X) (p : x ≡ y) → yoneda-elem η ≡ η p yoneda-const {X} {B} {x} η y p = v ⁻¹ • u where u : transport (constPrShf B) p (yoneda-elem η) ≡ η p u = yoneda-lemma η y p v : transport (constPrShf B) p (yoneda-elem η) ≡ yoneda-elem η v = yoneda-lemma ((λ p → yoneda-elem η)) y p \end{code} We now derive (based) path-induction, called J, from the Yoneda Construction. The idea is that J can be reduced to transport and "sigletons are contractible" (or the type of paths from a given point is contractible). I learned this reduction from Thierry Coquand. Added 8 May 2015: See also http://www.carloangiuli.com/blog/j-is-singleton-contractibility-plus-transport-definitionally/ To apply it in our situation, we need to prove that singletons are contractible from Yoneda, but we have already done our homework in yoneda-const. \begin{code} data Σ {X : U} (A : X → U) : U where _,_ : (x : X) → A x → Σ \(x : X) → A x paths-from : {X : U} → X → U paths-from {X} x = Σ \(y : X) → x ≡ y singletons-contractible : {X : U} {x : X} (w : paths-from x) → (x , idp x) ≡ w singletons-contractible {X} {x} (y , p) = yoneda-const η y p where η : Nat (Hom x) (constPrShf(paths-from x)) η {y} p = (y , p) J' : (X : U) (x : X) (B' : paths-from x → U) → B' (x , idp x) → ∀ w → B' w J' X x B' b w = transport B' (singletons-contractible w) b \end{code} Based path induction then reduces to J' in the obvious way: \begin{code} uncurry : {X : U}{x : X} → ((y : X) → x ≡ y → U) → (paths-from x → U) uncurry B (y , p) = B y p J : (X : U) (x : X) (B : (y : X) → x ≡ y → U) → B x (idp x) → (y : X) (p : x ≡ y) → B y p J X x B b y p = J' X x (uncurry B) b (y , p) \end{code} The computation rule holds definitionally (and this amounts to yoneda-computation, which doesn't need to be mentioned, as it itself holds definitionally): \begin{code} J-computation : {X : U} {x : X} {B : (y : X) → x ≡ y → U} (b : B x (idp x)) → J X x B b x (idp x) ≡ b J-computation = idp \end{code} J constructed in this way has the following normal form, with all implicit arguments given, computed by Agda. It is not very enlightening: \begin{code} J-normal-form : (X : U) (x : X) (B : (y : X) → x ≡ y → U) (b : B x (idp x)) (y : X) (p : x ≡ y) → J X x B b y p ≡ yoneda-nat {Σ {X} (λ y₂ → Hom {X} x y₂)} {x , idp x} {uncurry B} b {y , p} (yoneda-nat {Σ {X} (λ y₂ → Hom {X} x y₂)} {yoneda-nat {X} {x} {λ _ → Σ {X} (λ y₂ → Hom {X} x y₂)} (x , idp x) {y} p} {Hom {Σ {X} (λ y₂ → Hom {X} x y₂)} (x , idp x)} (yoneda-nat {Σ {X} (λ y₂ → Hom {X} x y₂)} {yoneda-nat {X} {x} {λ _ → Σ {X} (λ y₂ → Hom {X} x y₂)} (x , idp x) {y} p} {λ y₂ → Hom {Σ {X} (λ y₃ → Hom {X} x y₃)} y₂ (yoneda-nat {X} {x} {λ _ → Σ {X} (λ y₃ → Hom {X} x y₃)} (x , idp x) {y} p)} (idp (yoneda-nat {X} {x} {λ _ → Σ {X} (λ y₂ → Hom {X} x y₂)} (x , idp x) {y} p)) {x , idp x} (yoneda-lemma {X} {x} {λ _ → Σ {X} (λ y₂ → Hom {X} x y₂)} (λ {y₂} p₂ → x , idp x) y p)) {y , p} (yoneda-lemma {X} {x} {λ _ → Σ {X} (λ y₂ → Hom {X} x y₂)} (λ {x₂} p₂ → x₂ , p₂) y p)) J-normal-form X x B b y p = idp (J X x B b y p) infixl 6 _•_ \end{code} Is there a better definition of J from Yoneda, with a shorter normal form? Added 12 May 2015: Contractibility also arises as follows with the Yoneda Lemma. A representation of A:X→U is a given x:X together with a natural equivalence Π(y:X).x=y → A y (i.e. a y-indexed family of equivalences). Then a universal element of A is nothing but a center of contraction (x:X, a:A(x)) of the type Σ(x:X).A(x). So A:X→U is representable iff Σ(x:X).A(x) is contractible. In particular this generalizes that singletons are contractible. Another important example is when X is U, B:U and A(C)=(B≃C), we get that A is representable iff Σ(C:U).B≃C is contractible. But saying that, for any given B:U, the above "presheaf" A is representable is the same as saying that U is univalent. Hence U is univalent = (Pi(B:U).contractible(Σ(C:U).B≃C)). I will write down this below in Agda when I find time.