A self contained proof of the Yoneda lemma

This file — which is independent of the rest of the simplicial HoTT repository but references a few HoTT preliminaries — contains a self-contained proof of the ∞-categorical Yoneda lemma in the special case where both functors are contravariantly representable. This is intended for expository purposes.

As the Yoneda lemma does not require Rezk's "completeness" condition, an axiom that says that paths are equivalent to isomorphisms, here we only introduce pre-∞-categories, which are simpler to define.

We capitalize the first letter of the terms defined here when they are either duplications of or specializations of terms defined in the broader repository.

This is a literate rzk file:

#lang rzk-1

Prerequisites

The definitions and proofs reference standard concepts from homotopy type theory including a universe of types denoted U, the notion of contractible types, and the notion of equivalence between types. The universe is built into rzk, while the homotopy type theory predicates is-contr and is-equiv can be found in the HoTT folder of this repository.

Some of the definitions in this file rely on function extensionality:

#assume funext : FunExt

an axiom which characterizes the identity types of function types.

Simplices

The language for synthetic ∞-categories includes a primative notion called shapes which can be used to index type-valued diagrams. Shapes are carved out of directed cubes, which are cartesian products of the directed 1-cube 2, via predicates called topes. The cube 2 has two axiomatic terms 0₂ 1₂ : 2 and a binary tope ≤ satisfying the axioms of a strict interval. In particular, for any t : 2, 0₂ ≤ t and t ≤ 1₂ hold.

To state and prove the Yoneda lemma we require only two examples of shapes, the 1-simplex and 2-simplex defined by the topes below. In the rest of the library, these shapes are denoted using the more common superscripts.

The 1-simplex

#def Δ₁
  : 2 → TOPE
  := \ t → TOP

The 2-simplex

#def Δ₂
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

Hom types

The language for synthetic ∞-categories includes a new family of types called extension types. Given a cube I, a shape Ψ : I → TOPE, a subshape (Φ : Ψ → TOPE), a type family A : Ψ → U over the larger shape, and a function a : (t : Φ) → A t out of the smaller shape, there is a type ( t : Ψ) → A [ Φ t ↦ a t] whose terms are functions f : (t : Ψ) → A t so that f t ≡ a t whenever `#!rzk Φ t holds.

Extension types are used to define the type of arrows between fixed terms. Note that rzk allows the function out of a subshape formed by a union of topes to be specified by a list of functions defined for those terms satisfying each tope individually. The tope solver built into rzk then checks that these partial functions are compatible on the intersection of the topes.

RS17, Definition 5.1

#def Hom
  ( A : U)
  ( x y : A)
  : U
  :=
    ( t : Δ₁)
  → A [ t ≡ 0₂ ↦ x , -- the left endpoint is exactly x
        t ≡ 1₂ ↦ y]   -- the right endpoint is exactly y

Extension types are also used to define the type of commutative triangles:

RS17, Definition 5.2

#def Hom2
  ( A : U)
  ( x y z : A)
  ( f : Hom A x y)
  ( g : Hom A y z)
  ( h : Hom A x z)
  : U
  :=
    ( ( t₁ , t₂) : Δ₂)
  → A [ t₂ ≡ 0₂ ↦ f t₁ , -- the top edge is exactly `f`,
        t₁ ≡ 1₂ ↦ g t₂ , -- the right edge is exactly `g`, and
        t₂ ≡ t₁ ↦ h t₂]   -- the diagonal is exactly `h`

Types with composition

A type is a pre-∞-category if every composable pair of arrows has a unique composite, meaning that the type of composites is contractible.

Note this is a considerable simplification of the usual Segal condition, which also requires homotopical uniqueness of higher-order composites. Here this higher-order uniqueness is a consequence of the uniqueness of binary composition.

RS17, Definition 5.3

#def Is-pre-∞-category
  ( A : U)
  : U
  :=
    ( x : A) → (y : A) → (z : A)
  → ( f : Hom A x y) → (g : Hom A y z)
  → is-contr (Σ (h : Hom A x z) , (Hom2 A x y z f g h))

Pre-∞-categories have a composition functor and witnesses to the composition relation. Composition is written in diagrammatic order to match the order of arguments in is-pre-∞-category.

#def Comp-is-pre-∞-category
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( x y z : A)
  ( f : Hom A x y)
  ( g : Hom A y z)
  : Hom A x z
  := first (first (is-pre-∞-category-A x y z f g))

#def Witness-comp-is-pre-∞-category
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( x y z : A)
  ( f : Hom A x y)
  ( g : Hom A y z)
  : Hom2 A x y z f g (Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
  := second (first (is-pre-∞-category-A x y z f g))

Composition in a pre-∞-category is unique in the following sense. If there is a witness that an arrow h is a composite of f and g, then the specified composite equals h.

#def Uniqueness-comp-is-pre-∞-category
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( x y z : A)
  ( f : Hom A x y)
  ( g : Hom A y z)
  ( h : Hom A x z)
  ( alpha : Hom2 A x y z f g h)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h
  :=
    first-path-Σ
      ( Hom A x z)
      ( Hom2 A x y z f g)
      ( Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g
      , Witness-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
      ( h , alpha)
      ( homotopy-contraction
        ( Σ ( k : Hom A x z) , (Hom2 A x y z f g k))
        ( is-pre-∞-category-A x y z f g)
        ( h , alpha))

Identity

All types have identity arrows and witnesses to the identity composition law.

RS17, Definition 5.7

#def Id-hom
  ( A : U)
  ( x : A)
  : Hom A x x
  := \ t → x

Witness for the right identity law:

RS17, Proposition 5.8a

#def Comp-id-witness
  ( A : U)
  ( x y : A)
  ( f : Hom A x y)
  : Hom2 A x y y f (Id-hom A y) f
  := \ (t , s) → f t

Witness for the left identity law:

RS17, Proposition 5.8b

#def Id-comp-witness
  ( A : U)
  ( x y : A)
  ( f : Hom A x y)
  : Hom2 A x x y (Id-hom A x) f f
  := \ (t , s) → f s

In a pre-∞-category, where composition is unique, it follows that composition with an identity arrow recovers the original arrow. Thus, an identity axiom was not needed in the definition of pre-∞-categories.

If A is a pre-∞-category then the right unit law holds

#def Comp-id-is-pre-∞-category
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( x y : A)
  ( f : Hom A x y)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y y f (Id-hom A y))
    = f
  :=
    Uniqueness-comp-is-pre-∞-category
      ( A)
      ( is-pre-∞-category-A)
      ( x) (y) (y)
      ( f)
      ( Id-hom A y)
      ( f)
      ( Comp-id-witness A x y f)

If A is a pre-∞-category then the left unit law holds

#def Id-comp-is-pre-∞-category
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( x y : A)
  ( f : Hom A x y)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x x y (Id-hom A x) f)
    = f
  :=
    Uniqueness-comp-is-pre-∞-category
      ( A)
      ( is-pre-∞-category-A)
      ( x) (x) (y)
      ( Id-hom A x)
      ( f)
      ( f)
      ( Id-comp-witness A x y f)

Associativity is similarly automatic for pre-∞-categories, but since this is not needed to prove the Yoneda lemma, this will not be proven here.

Natural transformations between representable functors

Fix a pre-∞-category A and terms a b : A. The Yoneda lemma characterizes natural transformations between the type families contravariantly represented by these terms.

One might expect that such a natural transformation would involve a family of maps

ϕ : (z : A) → Hom A z a → Hom A z b

together with a proof of naturality of these components, but we will prove in naturality-contravariant-fiberwise-representable-transformation that naturality is automatic.

To see this, consider a composable pair of morphisms f : Hom A x y and v : Hom A y a in a pre-∞-category and form the square in A whose vertical boundary is given by f and Id-hom A a and whose horizontal boundary is given by the composite morphism and by v.

#def id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  : ( t : Δ¹) → (s : Δ¹) → A
  :=
    \ t s →
      recOR
      ( s ≤ t ↦
        ( Witness-comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)
          ( t , s)
      , t ≤ s ↦
        ( Comp-id-witness A x a
          ( Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) (s , t))

Next apply the fiberwise transformation ϕ to this square.

#def square-representable-transformation
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : ( t : Δ¹) → Hom A (f t) b
  :=
    \ t →
      ϕ
      ( f t)
      ( \ s → id-codomain-square A is-pre-∞-category-A a b x y f v t s)

We give a name to the diagonal composite arrow in this square.

#def diagonal-square-representable-transformation
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : Hom A x b
  :=
    \ t →
    square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ t t

The two halves of square-representable-transformation define witnesses for composition relations in A. We extract both witnesses and apply Uniqueness-comp-is-pre-∞-category to prove that the composite of the exterior edges equals the diagonal edge.

-- One half of transformation-id-codomain-square.
#def witness-comp-transformation-id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : Hom2 A x y b f (ϕ y v)
    ( diagonal-square-representable-transformation
      A is-pre-∞-category-A a b x y f v ϕ)
  :=
    \ (t , s) →
   square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ t s

-- The associated coherence.
#def coherence-witness-comp-transformation-id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v))
    = ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
  :=
    Uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)
      ( diagonal-square-representable-transformation
          A is-pre-∞-category-A a b x y f v ϕ)
      ( witness-comp-transformation-id-codomain-square
          A is-pre-∞-category-A a b x y f v ϕ)

-- The other half of transformation-id-codomain-square.
#def witness-id-transformation-id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : Hom2 A x b b
    ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
    ( Id-hom A b)
    ( diagonal-square-representable-transformation
      A is-pre-∞-category-A a b x y f v ϕ)
  :=
    \ (t , s) →
   square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ s t

-- The associated coherence.
#def coherence-witness-id-transformation-id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x b b
      ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
      ( Id-hom A b))
    = ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
  :=
    Uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x b b
    ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
    ( Id-hom A b)
    ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
    ( witness-id-transformation-id-codomain-square
          A is-pre-∞-category-A a b x y f v ϕ)

By the identity law Comp-id-is-pre-∞-category, this latter equality can be simplified.

#def simplified-coherence-witness-id-transformation-id-codomain-square
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
    = ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
  :=
    zag-zig-concat (Hom A x b)
    ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
    ( Comp-is-pre-∞-category A is-pre-∞-category-A x b b
      ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
      ( Id-hom A b))
    ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
    ( Comp-id-is-pre-∞-category A is-pre-∞-category-A x b
      ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)))
    ( coherence-witness-id-transformation-id-codomain-square
      A is-pre-∞-category-A a b x y f v ϕ)

By composing these equalities, we now prove that a fiberwise natural transformation ϕ : (z : A) → Hom A z a → Hom A z b is automatically natural: for arrows f : Hom A x y and v : Hom A y a in a pre-∞-category, the composite of f with ϕ y v equals the arrow obtained byϕ x applied to the composite of f with v.

#def Naturality-contravariant-fiberwise-representable-transformation
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b x y : A)
  ( f : Hom A x y)
  ( v : Hom A y a)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v))
  = ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
  :=
    zig-zag-concat (Hom A x b)
    ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v))
    ( diagonal-square-representable-transformation
        A is-pre-∞-category-A a b x y f v ϕ)
    ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))
    ( coherence-witness-comp-transformation-id-codomain-square
        A is-pre-∞-category-A a b x y f v ϕ)
    ( simplified-coherence-witness-id-transformation-id-codomain-square
        A is-pre-∞-category-A a b x y f v ϕ)

The Yoneda lemma

For any pre-∞-category A terms a b : A, the contravariant Yoneda lemma provides an equivalence between the type (z : A) → Hom A z a → Hom A z b of natural transformations and the type Hom A a b.

One of the maps in this equivalence is evaluation at the identity. The inverse map makes use of the contravariant transport operation.

The following map, contra-evid evaluates a natural transformation out of a representable functor at the identity arrow.

#def Contra-evid
  ( A : U)
  ( a b : A)
  : ( ( z : A) → Hom A z a → Hom A z b) → Hom A a b
  := \ ϕ → ϕ a (Id-hom A a)

The inverse map only exists for pre-∞-categories.

#def Contra-yon
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b : A)
  : Hom A a b → ((z : A) → Hom A z a → Hom A z b)
  := \ v z f → Comp-is-pre-∞-category A is-pre-∞-category-A z a b f v

It remains to show that the Yoneda maps are inverses. One retraction is straightforward:

#def Contra-evid-yon
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b : A)
  ( v : Hom A a b)
  : Contra-evid A a b (Contra-yon A is-pre-∞-category-A a b v) = v
  :=
    Id-comp-is-pre-∞-category A is-pre-∞-category-A a b v

The other composite carries ϕ to an a priori distinct natural transformation. We first show that these are pointwise equal at all x : A and f : Hom A x a in two steps.

#section contra-yon-evid

#variable A : U
#variable is-pre-∞-category-A : Is-pre-∞-category A
#variables a b : A

The composite Contra-yon-evid of ϕ equals ϕ at all x : A and f : Hom A x a.

#def Contra-yon-evid-twice-pointwise
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  ( x : A)
  ( f : Hom A x a)
  : ( ( Contra-yon A is-pre-∞-category-A a b)
        ( ( Contra-evid A a b) ϕ)) x f = ϕ x f
  :=
    concat
      ( Hom A x b)
      ( ( ( Contra-yon A is-pre-∞-category-A a b)
            ( ( Contra-evid A a b) ϕ)) x f)
      ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x a a f (Id-hom A a)))
      ( ϕ x f)
      ( Naturality-contravariant-fiberwise-representable-transformation
          A is-pre-∞-category-A a b x a f (Id-hom A a) ϕ)
      ( ap
        ( Hom A x a)
        ( Hom A x b)
        ( Comp-is-pre-∞-category A is-pre-∞-category-A x a a
          f (Id-hom A a))
        ( f)
        ( ϕ x)
        ( Comp-id-is-pre-∞-category A is-pre-∞-category-A x a f))

By funext, these are equals as functions of f pointwise in x.

#def Contra-yon-evid-once-pointwise uses (funext)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  ( x : A)
  : ( ( Contra-yon A is-pre-∞-category-A a b)
        ( ( Contra-evid A a b) ϕ)) x = ϕ x
  :=
    eq-htpy funext
      ( Hom A x a)
      ( \ f → Hom A x b)
      ( \ f →
        ( ( Contra-yon A is-pre-∞-category-A a b)
          ( ( Contra-evid A a b) ϕ)) x f)
      ( \ f → (ϕ x f))
      ( \ f → Contra-yon-evid-twice-pointwise ϕ x f)

By funext again, these are equal as functions of x and f.

#def Contra-yon-evid uses (funext)
  ( ϕ : (z : A) → Hom A z a → Hom A z b)
  : Contra-yon A is-pre-∞-category-A a b (Contra-evid A a b ϕ) = ϕ
  :=
    eq-htpy funext
      ( A)
      ( \ x → (Hom A x a → Hom A x b))
      ( Contra-yon A is-pre-∞-category-A a b (Contra-evid A a b ϕ))
      ( ϕ)
      ( Contra-yon-evid-once-pointwise ϕ)

#end contra-yon-evid

The contravariant Yoneda lemma says that evaluation at the identity defines an equivalence.

#def Contra-yoneda-lemma uses (funext)
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a b : A)
  : is-equiv ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Contra-evid A a b)
  :=
    ( ( ( Contra-yon A is-pre-∞-category-A a b)
      , ( Contra-yon-evid A is-pre-∞-category-A a b))
    , ( ( Contra-yon A is-pre-∞-category-A a b)
      , ( Contra-evid-yon A is-pre-∞-category-A a b)))

Contravariant Naturality

The equivalences of the Yoneda lemma is natural in both a : A and b : A. Naturality of the mapContra-yon follows formally from naturality of Contra-evid, so we prove only the latter, which is easier.

Naturality in b is not automatic but can be proven by reflexivity:

RS17, Lemma 9.2(i), dual

#def Is-natural-in-family-contra-evid
  ( A : U)
  ( a b b' : A)
  ( ψ : (z : A) → Hom A z b → Hom A z b')
  ( φ : (z : A) → Hom A z a → Hom A z b)
  : ( comp ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Hom A a b')
      ( ψ a) (Contra-evid A a b)) φ
  = ( comp ((z : A) → Hom A z a → Hom A z b) ((z : A) → Hom A z a → Hom A z b')
      ( Hom A a b')
      ( Contra-evid A a b') (\ α z g → ψ z (α z g))) φ
  := refl

Naturality in a in fact follows formally. By a generalization of Naturality-contravariant-fiberwise-representable-transformation which is no harder to prove, any fiberwise map between contravariant families over a : A is automatically natural. Since it would take time to introduce the notion of contravariant family and prove that the domain of Contra-evidis one, we instead give a direct proof of naturality in a : A.

RS17, Lemma 9.2(i), dual

#def Is-natural-in-object-contra-evid
  ( A : U)
  ( is-pre-∞-category-A : Is-pre-∞-category A)
  ( a' a b : A)
  ( k : Hom A a' a)
  ( φ : (z : A) → Hom A z a → Hom A z b)
  : ( comp ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Hom A a' b)
      ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)
      ( Contra-evid A a b)) φ
  = ( comp ((z : A) → Hom A z a → Hom A z b) ((z : A) → Hom A z a' → Hom A z b)
      ( Hom A a' b)
      ( Contra-evid A a' b)
      ( \ α z g →
          α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k))) φ
  :=
    concat (Hom A a' b)
    ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k (φ a (Id-hom A a)))
    ( φ a'
      ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a)))
    ( φ a'
      ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k))
    ( Naturality-contravariant-fiberwise-representable-transformation
      A is-pre-∞-category-A a b a' a k (Id-hom A a) φ)
    ( ap (hom A a' a) (hom A a' b)
      ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a))
      ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k)
      ( \ h → φ a' h)
      ( concat (hom A a' a)
        ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a))
        ( k)
        ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k)
        ( Comp-id-is-pre-∞-category A is-pre-∞-category-A a' a k)
        ( rev (hom A a' a)
          ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a
            ( Id-hom A a') k)
          ( k)
          ( Id-comp-is-pre-∞-category A is-pre-∞-category-A a' a k))))