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.