\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF.Yoneda where

open import MLTT.Spartan
open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Retracts
open import UF.Equiv
open import UF.FunExt
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples

\end{code}

We now consider "natural transformations" Nat A B (defined elsewhere)
and the Yoneda-machinery for them as discussed in
http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html

The Yoneda element induced by a natural transformation:

\begin{code}

yoneda-elem : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
            β†’ Nat (Id x) A β†’ A x
yoneda-elem x A Ξ· = Ξ· x refl

\end{code}

We use capital Yoneda for the same constructions with the definition
of "Nat" expanded, beginning here:

\begin{code}

Yoneda-elem : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
            β†’ ((y : X) β†’ x ＝ y β†’ A y) β†’ A x
Yoneda-elem = yoneda-elem

\end{code}

The natural transformation induced by an element:

\begin{code}

yoneda-nat : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
           β†’ A x β†’ Nat (Id x) A
yoneda-nat x A a y p = transport A p a

Yoneda-nat : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
           β†’ A x β†’ (y : X) β†’ x ＝ y β†’ A y
Yoneda-nat = yoneda-nat

\end{code}

Notice that this is the based recursion principle for the identity type.

The Yoneda Lemma says that every natural transformation is induced by
its Yoneda element:

\begin{code}

yoneda-lemma : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ ) (Ξ· : Nat (Id x) A)
             β†’ yoneda-nat x A (yoneda-elem x A Ξ·) β‰ˆ Ξ·
yoneda-lemma x A Ξ· y refl = refl

Yoneda-lemma : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
               (Ξ· : (y : X) β†’ x ＝ y β†’ A y) (y : X) (p : x ＝ y)
             β†’ transport A p (Ξ· x refl) ＝ Ξ· y p
Yoneda-lemma = yoneda-lemma

\end{code}

From another point of view, the Yoneda Lemma says that every natural
transformation Ξ· is recursively defined.

\begin{code}

yoneda-lemma' : FunExt
              β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ ) (Ξ· : Nat (Id x) A)
              β†’ yoneda-nat x A (yoneda-elem x A Ξ·) ＝ Ξ·
yoneda-lemma' {𝓀} {π“₯} fe x A Ξ· = dfunext (fe 𝓀 (𝓀 βŠ” π“₯))
                                   (Ξ» y β†’ dfunext (fe 𝓀 π“₯)
                                            (Ξ» p β†’ yoneda-lemma x A Ξ· y p))

\end{code}

The word "computation" here arises from a tradition in MLTT and should
not be taken too seriously:

\begin{code}

Yoneda-computation : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ ) (a : A x)
                   β†’ transport A refl a ＝ a
Yoneda-computation x A a = refl

yoneda-computation : {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ ) (a : A x)
                   β†’ yoneda-elem x A (yoneda-nat x A a) ＝ a
yoneda-computation x A = Yoneda-computation x A

yoneda-elem-is-equiv : FunExt
                     β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
                     β†’ is-equiv (yoneda-elem x A)
yoneda-elem-is-equiv fe x A = qinvs-are-equivs (yoneda-elem x A)
                                               (yoneda-nat x A ,
                                                yoneda-lemma' fe x A ,
                                                yoneda-computation x A)

yoneda-nat-is-equiv : FunExt
                    β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
                    β†’ is-equiv (yoneda-nat x A)
yoneda-nat-is-equiv fe {X} x A = qinvs-are-equivs (yoneda-nat x A)
                                                  (yoneda-elem x A ,
                                                   yoneda-computation x A ,
                                                   yoneda-lemma' fe x A)

yoneda-equivalence : FunExt
                   β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
                   β†’ A x ≃ Nat (Id x) A
yoneda-equivalence fe x A = yoneda-nat x A , yoneda-nat-is-equiv fe x A

Yoneda-equivalence : FunExt
                   β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ )
                   β†’ A x ≃ (βˆ€ y β†’ x ＝ y β†’ A y)
Yoneda-equivalence = yoneda-equivalence

\end{code}

Next we observe that "only elements", or centers of contraction, are
universal elements in the sense of category theory.

\begin{code}

is-universal-element-of : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) β†’ Ξ£ A β†’ 𝓀 βŠ” π“₯ Μ‡
is-universal-element-of {𝓀} {π“₯} {X} A (x , a) =
   (y : X) (b : A y) β†’ Ξ£ p κž‰ x ＝ y , yoneda-nat x A a y p ＝ b

universal-element-is-central : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (Οƒ : Ξ£ A)
                             β†’ is-universal-element-of A Οƒ
                             β†’ is-central (Ξ£ A) Οƒ
universal-element-is-central (x , a) u (y , b) = to-Σ-＝ (u y b)

central-point-is-universal : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (Οƒ : Ξ£ A)
                           β†’ is-central (Ξ£ A) Οƒ
                           β†’ is-universal-element-of A Οƒ
central-point-is-universal A (x , a) Ο† y b = from-Ξ£-＝ (Ο†(y , b))

\end{code}

The following says that if the pair (x,a) is a universal element, then
the natural transformation it induces (namely yoneda-nat x a)
has a section and a retraction (which can be taken to be the same
function), and hence is an equivalence. Here having a section or
retraction is data not property in general, but it is in some cases
considered below.

\begin{code}

universality-section : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (a : A x)
                     β†’ is-universal-element-of A (x , a)
                     β†’ (y : X) β†’ has-section (yoneda-nat x A a y)
universality-section {𝓀} {π“₯} {X} {A} x a u y = s y , Ο† y
 where
  s : (y : X) β†’ A y β†’ x ＝ y
  s y b = pr₁ (u y b)
  Ο† : (y : X) (b : A y) β†’ yoneda-nat x A a y (s y b) ＝ b
  Ο† y b = prβ‚‚ (u y b)

section-universality : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (a : A x)
                     β†’ ((y : X) β†’ has-section(yoneda-nat x A a y))
                     β†’ is-universal-element-of A (x , a)
section-universality x a Ο† y b = pr₁(Ο† y) b , prβ‚‚(Ο† y) b

\end{code}

NB. Notice that Yoneda-nat gives two different natural
transformations, depending on the number of arguments it takes, namely
the natural transformation (x : X) β†’ A x β†’ Nat (Id x) A and the
natural transformation Nat (Id x) β†’ A (or (y : X) β†’ x ＝ y β†’ A y) if
two additional arguments x and a are given.

Then the Yoneda Theorem (proved below) says that any Ξ· : Nat (Id x) A)
is a natural equivalence iff Ξ£ A is a singleton. This, in turn, is
equivalent to Ξ· being a natural retraction, and we start with it:

\begin{code}

Yoneda-section-forth : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                     β†’ βˆƒ! A β†’ (y : X) β†’ has-section (Ξ· y)
Yoneda-section-forth {𝓀} {π“₯} {X} {A} x Ξ· i y = g
 where
  u : is-universal-element-of A (x , yoneda-elem x A Ξ·)
  u = central-point-is-universal A
        (x , yoneda-elem x A Ξ·)
        (singletons-are-props i (x , yoneda-elem x A Ξ·))
  h : yoneda-nat x A (yoneda-elem x A η) y ∼ η y
  h = yoneda-lemma x A Ξ· y
  g : has-section (Ξ· y)
  g = has-section-closed-under-∼' (universality-section x (yoneda-elem x A η) u y) h

Yoneda-section-back : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                    β†’ ((y : X) β†’ has-section (Ξ· y)) β†’ βˆƒ! A
Yoneda-section-back {𝓀} {π“₯} {X} {A} x Ξ· Ο† = c
 where
  h : βˆ€ y β†’ yoneda-nat x A (yoneda-elem x A Ξ·) y ∼ Ξ· y
  h = yoneda-lemma x A Ξ·
  g : βˆ€ y β†’ has-section (yoneda-nat x A (yoneda-elem x A Ξ·) y)
  g y = has-section-closed-under-∼ (Ξ· y) (yoneda-nat x A (yoneda-elem x A Ξ·) y) (Ο† y) (h y)
  u : is-universal-element-of A (x , yoneda-elem x A Ξ·)
  u = section-universality x (yoneda-elem x A Ξ·) g
  c : βˆƒ! A
  c = (x , yoneda-elem x A Ξ·) , (universal-element-is-central (x , yoneda-elem x A Ξ·) u)

Yoneda-section : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
               β†’ βˆƒ! A ⇔ ((y : X) β†’ has-section (Ξ· y))
Yoneda-section x Ξ· = Yoneda-section-forth x Ξ· , Yoneda-section-back x Ξ·

\end{code}

Here is a direct application (24th April 2018).

\begin{code}

equiv-adj : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (g : Y β†’ X)
            (Ξ· : (x : X) (y : Y) β†’ f x ＝ y β†’ g y ＝ x)
          β†’ ((x : X) (y : Y) β†’ has-section (Ξ· x y)) ⇔ is-vv-equiv g
equiv-adj f g Ξ· = (Ξ» i x β†’ Yoneda-section-back (f x) (Ξ· x) (i x)) ,
                  (Ξ» Ο† x β†’ Yoneda-section-forth (f x) (Ξ· x) (Ο† x))

\end{code}

This motivates the following definition.

\begin{code}

has-adj : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (Y β†’ X) β†’ 𝓀 βŠ” π“₯ Μ‡
has-adj g = Ξ£ f κž‰ (codomain g β†’ domain g)
          , Ξ£ Ξ· κž‰ (βˆ€ x y β†’ f x ＝ y β†’ g y ＝ x)
          , (βˆ€ x y β†’ has-section(Ξ· x y))

is-vv-equiv-has-adj : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (g : Y β†’ X)
                    β†’ is-vv-equiv g β†’ has-adj g
is-vv-equiv-has-adj {𝓀} {π“₯} {X} {Y} g isv = f , Ξ· , hass
 where
  f : X β†’ Y
  f = pr₁ (pr₁ (vv-equivs-are-equivs g isv))
  gf : (x : X) β†’ g (f x) ＝ x
  gf = prβ‚‚ (pr₁ (vv-equivs-are-equivs g isv))
  Ξ· : (x : X) (y : Y) β†’ f x ＝ y β†’ g y ＝ x
  Ξ· x y p = transport (Ξ» - β†’ g - ＝ x) p (gf x )
  hass : (x : X) (y : Y) β†’ has-section (Ξ· x y)
  hass x = Yoneda-section-forth (f x) (Ξ· x) (isv x)

has-adj-is-vv-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (g : Y β†’ X)
                    β†’ has-adj g β†’ is-vv-equiv g
has-adj-is-vv-equiv g (f , Ξ· , hass) x = Yoneda-section-back (f x) (Ξ· x) (hass x)

\end{code}

A natural transformation of the above kind is an equivalence iff it has a section,
as shown in https://github.com/HoTT/book/issues/718#issuecomment-65378867:

\begin{code}

Hedberg-lemma : {X : 𝓀 Μ‡ } (x : X) (Ξ· : (y : X) β†’ x ＝ y β†’ x ＝ y) (y : X) (p : x ＝ y)
              β†’ Ξ· x refl βˆ™ p ＝ Ξ· y p
Hedberg-lemma x Ξ· = yoneda-lemma x (Id x) Ξ·

idemp-is-id : {X : 𝓀 Μ‡ } {x : X} (e : (y : X) β†’ x ＝ y β†’ x ＝ y) (y : X) (p : x ＝ y)
            β†’ e y (e y p) ＝ e y p
            β†’ e y p ＝ p
idemp-is-id {𝓀} {X} {x} e y p idemp = cancel-left (
        e x refl βˆ™ e y p ＝⟨ Hedberg-lemma x e y (e y p) ⟩
        e y (e y p)      ＝⟨ idemp ⟩
        e y p            ＝⟨ (Hedberg-lemma x e y p)⁻¹ ⟩
        e x refl βˆ™ p     ∎)

nat-retraction-is-section : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                          β†’ ((y : X) β†’ has-section(Ξ· y))
                          β†’ ((y : X) β†’ is-section(Ξ· y))
nat-retraction-is-section {𝓀} {π“₯} {X} {A} x Ξ· hs = hr
 where
  s : (y : X) β†’ A y β†’ x ＝ y
  s y = pr₁ (hs y)
  Ξ·s : {y : X} (a : A y) β†’ Ξ· y (s y a) ＝ a
  Ξ·s {y} = prβ‚‚ (hs y)
  e : (y : X) β†’ x ＝ y β†’ x ＝ y
  e y p = s y (Ξ· y p)
  idemp : (y : X) (p : x ＝ y) β†’ e y (e y p) ＝ e y p
  idemp y p = ap (s y) (Ξ·s (Ξ· y p))
  i : (y : X) (p : x ＝ y) β†’ e y p ＝ p
  i y p = idemp-is-id e y p (idemp y p)
  hr : (y : X) β†’ is-section(Ξ· y)
  hr y = s y , i y

\end{code}

The above use of the word "is" is justified by the following:

\begin{code}

nat-retraction-is-section-uniquely : FunExt
                                   β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                                     (x : X) (Ξ· : Nat (Id x) A)
                                   β†’ ((y : X) β†’ has-section(Ξ· y))
                                   β†’ ((y : X) β†’ is-singleton(is-section(Ξ· y)))
nat-retraction-is-section-uniquely fe x Ξ· hs y = pointed-props-are-singletons
                                                  (nat-retraction-is-section x Ξ· hs y)
                                                  (sections-have-at-most-one-retraction fe (Ξ· y) (hs y))

nat-having-section-is-prop : FunExt
                           β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                             (x : X) (Ξ· : Nat (Id x) A)
                           β†’ is-prop ((y : X) β†’ has-section (Ξ· y))
nat-having-section-is-prop {𝓀} {π“₯} fe {X} x Ξ· Ο† = Ξ -is-prop (fe 𝓀 (𝓀 βŠ” π“₯)) Ξ³ Ο†
  where
   Ξ³ : (y : X) β†’ is-prop (has-section (Ξ· y))
   Ξ³ y = retractions-have-at-most-one-section fe (Ξ· y) (nat-retraction-is-section x Ξ· Ο† y)

nats-with-sections-are-equivs : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                              β†’ ((y : X) β†’ has-section(Ξ· y))
                              β†’ is-fiberwise-equiv Ξ·
nats-with-sections-are-equivs x Ξ· hs y = (hs y , nat-retraction-is-section x Ξ· hs y)

\end{code}

We are interested in the following corollaries:

\begin{code}

universality-equiv : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (a : A x)
                   β†’ is-universal-element-of A (x , a)
                   β†’ is-fiberwise-equiv (yoneda-nat x A a)
universality-equiv {𝓀} {π“₯} {X} {A} x a u = nats-with-sections-are-equivs x
                                             (yoneda-nat x A a)
                                             (universality-section x a u)

equiv-universality : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (a : A x)
                   β†’ is-fiberwise-equiv (yoneda-nat x A a )
                   β†’ is-universal-element-of A (x , a)
equiv-universality x a Ο† = section-universality x a (Ξ» y β†’ pr₁ (Ο† y))

Yoneda-Theorem-forth : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                     β†’ βˆƒ! A β†’ is-fiberwise-equiv Ξ·
Yoneda-Theorem-forth x Ξ· i = nats-with-sections-are-equivs x Ξ· (Yoneda-section-forth x Ξ· i)

\end{code}

Here is another proof, from the MGS'2019 lecture notes (https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes):

\begin{code}

Yoneda-Theorem-forth' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X) (Ξ· : Nat (Id x) A)
                      β†’ βˆƒ! A β†’ is-fiberwise-equiv Ξ·
Yoneda-Theorem-forth' {𝓀} {π“₯} {X} A x Ξ· u = Ξ³
 where
  g : singleton-type x β†’ Ξ£ A
  g = NatΞ£ Ξ·

  e : is-equiv g
  e = maps-of-singletons-are-equivs g (singleton-types-are-singletons x) u

  Ξ³ : is-fiberwise-equiv Ξ·
  Ξ³ = NatΞ£-equiv-gives-fiberwise-equiv Ξ· e

\end{code}

Here is an application:

\begin{code}

fiberwise-equiv-criterion : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                            (x : X)
                          β†’ ((y : X) β†’ A y ◁ (x ＝ y))
                          β†’ (Ο„ : Nat (Id x) A) β†’ is-fiberwise-equiv Ο„
fiberwise-equiv-criterion A x ρ Ο„ = Yoneda-Theorem-forth x Ο„
                                     (Yoneda-section-back x
                                       (Ξ» x β†’ retraction (ρ x))
                                       (Ξ» x β†’ retraction-has-section (ρ x)))

fiberwise-equiv-criterion' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                             (x : X)
                           β†’ ((y : X) β†’ (x ＝ y) ≃ A y)
                           β†’ (Ο„ : Nat (Id x) A) β†’ is-fiberwise-equiv Ο„
fiberwise-equiv-criterion' A x e = fiberwise-equiv-criterion A x
                                    (Ξ» y β†’ ≃-gives-β–· (e y))

\end{code}

This says that is there is any fiberwise equivalence whatsoever (or
even just a fiberwise retraction), then any natural transformation is
a fiberwise equivalence.

\begin{code}

Yoneda-Theorem-back : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X) (Ξ· : Nat (Id x) A)
                    β†’ is-fiberwise-equiv Ξ· β†’ βˆƒ! A
Yoneda-Theorem-back x Ξ· Ο† = Yoneda-section-back x Ξ· (Ξ» y β†’ pr₁(Ο† y))

\end{code}

Next we conclude that a presheaf A is representable iff Ξ£ A is a
singleton.

\begin{code}

_β‰Š_ : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
A β‰Š B = Ξ£ Ξ· κž‰ Nat A B , is-fiberwise-equiv Ξ·

is-representable : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
is-representable A = Ξ£ x κž‰ domain A , Id x β‰Š A

singleton-representable : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                        β†’ βˆƒ! A β†’ is-representable A
singleton-representable {𝓀} {π“₯} {X} {A} ((x , a) , cc) =
  x , yoneda-nat x A a , Yoneda-Theorem-forth x (yoneda-nat x A a) ((x , a) , cc)

representable-singleton : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                        β†’ is-representable A β†’ βˆƒ! A
representable-singleton (x , (Ξ· , Ο†)) = Yoneda-Theorem-back x Ξ· Ο†

\end{code}

We also have the following corollaries:

\begin{code}

is-vv-equiv-has-adj' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (g : Y β†’ X)
                     β†’ is-vv-equiv g
                     β†’ Ξ£ f κž‰ (X β†’ Y) , ((x : X) (y : Y) β†’ (f x ＝ y) ≃ (g y ＝ x))
is-vv-equiv-has-adj' g Ο† = pr₁ Ξ³ ,
                           Ξ» x y β†’ pr₁ (prβ‚‚ Ξ³) x y ,
                                   nats-with-sections-are-equivs
                                     (pr₁ Ξ³ x) (pr₁ (prβ‚‚ Ξ³) x) (prβ‚‚ (prβ‚‚ Ξ³) x) y
 where
  Ξ³ : has-adj g
  Ξ³ = is-vv-equiv-has-adj g Ο†

has-adj-is-vv-equiv' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (g : Y β†’ X)
                     β†’ (Ξ£ f κž‰ (X β†’ Y) , ((x : X) (y : Y) β†’ (f x ＝ y) ≃ (g y ＝ x)))
                     β†’ is-vv-equiv g
has-adj-is-vv-equiv' g (f , ψ) =
  has-adj-is-vv-equiv g (f , (Ξ» x y β†’ pr₁(ψ x y)) , (Ξ» x y β†’ pr₁(prβ‚‚(ψ x y))))

\end{code}

Here is an application of the Yoneda machinery to a well-known result
by Voevodsky. If products preserve contractibility, then function
extensionality holds (happly is an equivalence).

\begin{code}

funext-via-singletons :
    ((X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ )
  β†’ ((x : X) β†’ is-singleton (Y x)) β†’ is-singleton (Ξ  Y))
  β†’ funext 𝓀 π“₯
funext-via-singletons {𝓀} {π“₯} Ο† {X} {Y} f = Ξ³
 where
  c : is-singleton (Ξ  x κž‰ X , Ξ£ y κž‰ Y x , f x ＝ y)
  c = Ο† X (Ξ» x β†’ Ξ£ y κž‰ Y x , f x ＝ y) (Ξ» x β†’ singleton-types-are-singletons (f x))
  A : Ξ  Y β†’ 𝓀 βŠ” π“₯ Μ‡
  A g = (x : X) β†’ f x ＝ g x
  r : (Ξ  x κž‰ X , Ξ£ y κž‰ Y x , f x ＝ y) β†’ Ξ£ A
  r = TT-choice
  r-has-section : has-section r
  r-has-section = TT-choice-has-section
  d : βˆƒ! A
  d = retract-of-singleton (r , r-has-section) c
  Ξ· : Nat (Id f) A
  Ξ· = happly' f
  Ξ³ : (g : Ξ  Y) β†’ is-equiv (happly' f g)
  Ξ³ = Yoneda-Theorem-forth f Ξ· d

\end{code}

We also have the following characterization of univalence from the
Yoneda machinery.

The fact that this is the case was announced on 5th August
2014 with the techniques of the HoTT Book
(https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ)),
and the proof given here via Yoneda was announced on 12th May 2015
(http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html).

\begin{code}

open import UF.Univalence

univalence-via-singletonsβ†’ : is-univalent 𝓀 β†’ (X : 𝓀 Μ‡ ) β†’ βˆƒ! Y κž‰ 𝓀 Μ‡  , X ≃ Y
univalence-via-singletons→ ua X = representable-singleton (X , (idtoeq X , ua X))

univalence-via-singletons← : ((X : 𝓀 Μ‡ ) β†’ βˆƒ! Y κž‰ 𝓀 Μ‡  , X ≃ Y) β†’ is-univalent 𝓀
univalence-via-singletons← Ο† X = universality-equiv X (≃-refl X)
                                  (central-point-is-universal
                                     (X ≃_)
                                     (X , ≃-refl X)
                                     (singletons-are-props (Ο† X) (X , ≃-refl X)))

univalence-via-singletons : is-univalent 𝓀 ⇔ ((X : 𝓀 Μ‡ ) β†’ βˆƒ! Y κž‰ 𝓀 Μ‡  , X ≃ Y)
univalence-via-singletons = (univalence-via-singletonsβ†’ , univalence-via-singletons←)

\end{code}

Notice that is-singleton can be replaced by is-prop in the formulation
of this logical equivalence (exercise).


Appendix.

Two natural transformations with the same Yoneda elements are
(point-point-wise) equal. This can be proved using J (or equivalently
pattern matching), but we use the opportunity to illustrate how to use
the Yoneda Lemma.

\begin{code}

yoneda-elem-lc : {X : 𝓀 Μ‡ } {x : X} {A : X β†’ π“₯ Μ‡ }
                 (Ξ· ΞΈ : Nat (Id x) A)
               β†’ yoneda-elem x A Ξ· ＝ yoneda-elem x A ΞΈ β†’ Ξ· β‰ˆ ΞΈ
yoneda-elem-lc {𝓀} {π“₯} {X} {x} {A} Ξ· ΞΈ q y p =
  η y p                                ＝⟨ (yoneda-lemma x A η y p)⁻¹ ⟩
  yoneda-nat x A (yoneda-elem x A Ξ·) y p ＝⟨ ap (Ξ» - β†’ yoneda-nat x A - y p) q ⟩
  yoneda-nat x A (yoneda-elem x A θ) y p ＝⟨ yoneda-lemma x A θ y p ⟩
  θ y p ∎

Yoneda-elem-lc : {X : 𝓀 Μ‡ } {x : X} {A : X β†’ π“₯ Μ‡ } (Ξ· ΞΈ : (y : X) β†’ x ＝ y β†’ A y)
              β†’ Ξ· x refl ＝ ΞΈ x refl β†’ (y : X) (p : x ＝ y) β†’ Ξ· y p ＝ ΞΈ y p
Yoneda-elem-lc = yoneda-elem-lc

\end{code}

Some special cases of interest, which probably speak for themselves:

\begin{code}

yoneda-nat-Id : {X : 𝓀 Μ‡ } (x {y} : X) β†’ Id x y β†’ Nat (Id y) (Id x)
yoneda-nat-Id x {y} = yoneda-nat y (Id x)

Yoneda-nat-Id : {X : 𝓀 Μ‡ } (x {y} : X) β†’ x ＝ y β†’ (z : X) β†’ y ＝ z β†’ x ＝ z
Yoneda-nat-Id = yoneda-nat-Id

Id-charac : FunExt
          β†’ {X : 𝓀 Μ‡ } (x {y} : X) β†’ (x ＝ y) ≃ Nat (Id y) (Id x)
Id-charac fe {X} x {y} = yoneda-equivalence fe y (Id x)

yoneda-nat-Eq : (X {Y} : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ Nat (Y ＝_) (X ≃_)
yoneda-nat-Eq X {Y} = yoneda-nat Y (X ≃_)

yoneda-elem-Id : {X : 𝓀 Μ‡ } (x {y} : X) β†’ Nat (Id y) (Id x) β†’ Id x y
yoneda-elem-Id x {y} = yoneda-elem y (Id x)

Yoneda-elem-Id : {X : 𝓀 Μ‡ } (x {y} : X) β†’ ((z : X) β†’ y ＝ z β†’ x ＝ z) β†’ x ＝ y
Yoneda-elem-Id = yoneda-elem-Id

yoneda-lemma-Id : {X : 𝓀 Μ‡ } (x {y} : X) (Ξ· : Nat (Id y) (Id x)) (z : X) (p : y ＝ z)
                β†’ (yoneda-elem-Id x Ξ·) βˆ™ p ＝ Ξ· z p
yoneda-lemma-Id x {y} = yoneda-lemma y (Id x)

Yoneda-lemma-Id : {X : 𝓀 Μ‡ } (x {y} : X) (Ξ· : (z : X) β†’ y ＝ z β†’ x ＝ z) (z : X) (p : y ＝ z)
                β†’ Ξ· y refl βˆ™ p ＝ Ξ· z p
Yoneda-lemma-Id = yoneda-lemma-Id

yoneda-const : {X : 𝓀 Μ‡ } {B : π“₯ Μ‡ } {x : X} (Ξ· : Nat (Id x) (Ξ» _ β†’ B)) (y : X) (p : x ＝ y)
             β†’ yoneda-elem x (Ξ» _ β†’ B) Ξ· ＝ Ξ· y p
yoneda-const Ξ· = yoneda-elem-lc (Ξ» y p β†’ yoneda-elem _ _ Ξ·) Ξ· refl

Yoneda-const : {X : 𝓀 Μ‡ } {B : π“₯ Μ‡ } {x : X} (Ξ· : (y : X) β†’ x ＝ y β†’ B) (y : X) (p : x ＝ y)
             β†’ Ξ· x refl ＝ Ξ· y p
Yoneda-const = yoneda-const

\end{code}

The following is traditionally proved by induction on the identity
type (as articulated by Jbased or J in the module UF.MLTT.Spartan), but
here we use the Yoneda machinery instead, again for the sake of
illustration.

\begin{code}

singleton-types-are-singletons-bis : {X : 𝓀 Μ‡ } (x : X)
                                   β†’ is-central (singleton-type x) (x , refl)
singleton-types-are-singletons-bis {𝓀} {X} x (y , p) = yoneda-const Ξ· y p
 where
  Ξ· : (y : X) β†’ x ＝ y β†’ singleton-type x
  Ξ· y p = (y , p)

\end{code}

What the following says is that the Yoneda machinery could have been
taken as primitive, as an alternative to Jbased or J, in the sense
that the latter can be recovered from the former.

\begin{code}

private

 Jbased'' : {X : 𝓀 Μ‡ } (x : X) (A : singleton-type x β†’ π“₯ Μ‡ )
          β†’ A (x , refl) β†’ Ξ  A
 Jbased'' x A a w = yoneda-nat (x , refl) A a w (singleton-types-are-singletons' w)

 Jbased' : {X : 𝓀 Μ‡ } (x : X) (B : (y : X) β†’ x ＝ y β†’ π“₯ Μ‡ )
         β†’ B x refl β†’ (y : X) β†’ Ξ  (B y)
 Jbased' x B b y p = Jbased'' x (uncurry B) b (y , p)

\end{code}

And now some more uses of Yoneda to prove things that traditionally
are proved using J(based), again for the sake of illustration:

\begin{code}

refl-left-neutral-bis : {X : 𝓀 Μ‡ } {x y : X} {p : x ＝ y} β†’ refl βˆ™ p ＝ p
refl-left-neutral-bis {𝓀} {X} {x} {y} {p} = yoneda-lemma x (Id x) (Ξ» y p β†’ p) y p

⁻¹-involutive-bis : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y) β†’ (p ⁻¹)⁻¹ ＝ p
⁻¹-involutive-bis {𝓀} {X} {x} {y} = yoneda-elem-lc (Ξ» x p β†’ (p ⁻¹)⁻¹) (Ξ» x p β†’ p) refl y

⁻¹-contravariant-bis : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y) {z : X} (q : y ＝ z)
                β†’ q ⁻¹ βˆ™ p ⁻¹ ＝ (p βˆ™ q)⁻¹
⁻¹-contravariant-bis {𝓀} {X} {x} {y} p {z} = yoneda-elem-lc (Ξ» z q β†’ q ⁻¹ βˆ™ p ⁻¹)
                                                       (Ξ» z q β†’ (p βˆ™ q) ⁻¹)
                                                       refl-left-neutral-bis
                                                       z
\end{code}

Associativity also follows from the Yoneda Lemma, again with the same
proof method. Notice that we prove that two functions (in a context)
are equal without using function extensionality:

\begin{code}

ext-assoc : {X : 𝓀 Μ‡ } {z t : X} (r : z ＝ t)
          β†’ (Ξ» (x y : X) (p : x ＝ y) (q : y ＝ z) β†’ (p βˆ™ q) βˆ™ r)
          ＝ (Ξ» (x y : X) (p : x ＝ y) (q : y ＝ z) β†’ p βˆ™ (q βˆ™ r))
ext-assoc {𝓀} {X} {z} {t} = yoneda-elem-lc {𝓀} {𝓀} {X} {z} {Ξ» - β†’ (x y : X) (p : x ＝ y) (q : y ＝ z) β†’ x ＝ - }
                                           (Ξ» z r x y p q β†’ p βˆ™ q βˆ™ r)
                                           (Ξ» z r x y p q β†’ p βˆ™ (q βˆ™ r))
                                           refl
                                           t
\end{code}

Then of course associativity of path composition follows:

\begin{code}

assoc-bis : {X : 𝓀 Μ‡ } {x y z t : X} (p : x ＝ y) (q : y ＝ z) (r : z ＝ t)
          β†’ (p βˆ™ q) βˆ™ r ＝ p βˆ™ (q βˆ™ r)
assoc-bis {𝓀} {X} {x} {y} p q r = ap (Ξ» - β†’ - x y p q) (ext-assoc r)

left-inverse-bis : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y) β†’ p ⁻¹ βˆ™ p ＝ refl
left-inverse-bis {𝓀} {X} {x} {y} = yoneda-elem-lc (Ξ» x p β†’ p ⁻¹ βˆ™ p) (Ξ» x p β†’ refl) refl y

right-inverse-bis : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y) β†’ refl ＝ p βˆ™ p ⁻¹
right-inverse-bis {𝓀} {X} {x} {y} = yoneda-const (Ξ» x p β†’ p βˆ™ p ⁻¹) y

from-Ξ£-Id : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
          β†’ Οƒ ＝ Ο„
          β†’ Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , yoneda-nat (Οƒ .pr₁) A (prβ‚‚ Οƒ) (pr₁ Ο„) p ＝ prβ‚‚ Ο„
from-Ξ£-Id {𝓀} {π“₯} {X} {A} {x , a} {Ο„} = yoneda-nat (x , yoneda-nat x A a x refl) B (refl , refl) Ο„
 where
   B : (Ο„ : Ξ£ A) β†’ 𝓀 βŠ” π“₯ Μ‡
   B Ο„ = Ξ£ p κž‰ x ＝ pr₁ Ο„ , yoneda-nat x A a (pr₁ Ο„) p ＝ prβ‚‚ Ο„

to-Ξ£-Id : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
          β†’ (Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , yoneda-nat (pr₁ Οƒ) A (prβ‚‚ Οƒ) (pr₁ Ο„) p ＝ prβ‚‚ Ο„)
          β†’ Οƒ ＝ Ο„
to-Ξ£-Id {𝓀} {π“₯} {X} {A} {x , a} {y , b} (p , q) = r
 where
  Ξ· : (y : X) β†’ x ＝ y β†’ Ξ£ A
  Ξ· y p = (y , yoneda-nat x A a y p)
  yc : (x , a) ＝ (y , yoneda-nat x A a y p)
  yc = yoneda-const Ξ· y p
  r : (x , a) ＝ (y , b)
  r = yoneda-nat (yoneda-nat x A a y p) (Ξ» b β†’ (x , a) ＝ (y , b)) yc b q

from-Ξ£-Id' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
           β†’ Οƒ ＝ Ο„
           β†’ Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ＝ prβ‚‚ Ο„
from-Ξ£-Id' = from-Ξ£-Id

to-Ξ£-Id' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
         β†’ (Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ＝ prβ‚‚ Ο„)
         β†’ Οƒ ＝ Ο„
to-Ξ£-Id' = to-Ξ£-Id

NatΞ£-lc' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } (ΞΆ : Nat A B)
         β†’ ((x : X) β†’ left-cancellable(ΞΆ x)) β†’ left-cancellable(NatΞ£ ΞΆ)
NatΞ£-lc' {𝓀} {π“₯} {𝓦} {X} {A} {B} ΞΆ ΞΆ-lc {(x , a)} {(y , b)} pq = g
  where
    p : x ＝ y
    p = pr₁ (from-Ξ£-Id pq)
    Ξ· : Nat (Id x) B
    Ξ· = yoneda-nat x B (ΞΆ x a)
    q : η y p ＝ ΢ y b
    q = prβ‚‚ (from-Ξ£-Id pq)
    ΞΈ : Nat (Id x) A
    ΞΈ = yoneda-nat x A a
    Ξ·' : Nat (Id x) B
    Ξ·' y p = ΞΆ y (ΞΈ y p)
    r : Ξ·' β‰ˆ Ξ·
    r = yoneda-elem-lc Ξ·' Ξ· refl
    r' : ΢ y (θ y p) ＝ η y p
    r' = r y p
    s : ΢ y (θ y p) ＝ ΢ y b
    s = r' βˆ™ q
    t : θ y p ＝ b
    t = ΞΆ-lc y s
    g : x , a ＝ y , b
    g = to-Ξ£-Id (p , t)

yoneda-equivalence-Ξ£ : FunExt
                     β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                     β†’ Ξ£ A ≃ (Ξ£ x κž‰ X , Nat (Id x) A)
yoneda-equivalence-Ξ£ fe A = Ξ£-cong (Ξ» x β†’ yoneda-equivalence fe x A)


nats-are-uniquely-transports : FunExt
                             β†’ {X : 𝓀 Μ‡ } (x : X) (A : X β†’ π“₯ Μ‡ ) (Ξ· : Nat (Id x) A)
                             β†’ βˆƒ! a κž‰ A x , (Ξ» y p β†’ transport A p a) ＝ Ξ·
nats-are-uniquely-transports fe x A = equivs-are-vv-equivs (yoneda-nat x A) (yoneda-nat-is-equiv fe x A)

adj-obs : FunExt
        β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (g : Y β†’ X) (x : X)
          (Ξ· : (y : Y) β†’ f x ＝ y β†’ g y ＝ x)
        β†’ βˆƒ! q κž‰ g (f x) ＝ x , (Ξ» y p β†’ transport (Ξ» - β†’ g - ＝ x) p q) ＝ Ξ·
adj-obs fe f g x = nats-are-uniquely-transports fe (f x) (Ξ» y β†’ g y ＝ x)

\end{code}

We need this elsewhere:

\begin{code}

idtoeq-bis : (X : 𝓀 Μ‡ ) β†’ Nat (X ＝_) (X ≃_)
idtoeq-bis X = yoneda-nat X (X ≃_) (≃-refl X)

Idtofun' : (X : 𝓀 Μ‡ ) β†’ Nat (Id X) (Ξ» Y β†’ X β†’ Y)
Idtofun' X = yoneda-nat X (Ξ» Y β†’ X β†’ Y) id

idtofun-agree' : (X : 𝓀 Μ‡ ) β†’ idtofun X β‰ˆ Idtofun' X
idtofun-agree' X = yoneda-elem-lc (idtofun X) (Idtofun' X) refl

\end{code}