Martin Escardo, 7 May 2015. This is a literate Agda file.

Updated 2015, 2016, 2017 with promises made in 12 May 2015, and a few
other minor things (Agda code and remarks), with precise dates given
at the update points.

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 function
extensionality, 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. 

\begin{code}

{-# OPTIONS --without-K --safe #-}

module yoneda where

open import NonStandardUniverseNotation

\end{code}

We let U, V, W range over universes.

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 Path {U : Universe} {X : U ̇} : X  X  U ̇ where
  idp : (x : X)  Path x x 

\end{code}

The type x ≡ y is the hom type of paths from x to y, which is itself
another ω-groupoid for every x,y:X. Traditional synonyms are the
following:

\begin{code}

Id Hom _≡_ :  {U} {X : U ̇}  X  X  U ̇
Id  = Path
Hom = Path
_≡_ = Path

refl :  {U} {X : U ̇} {x : X}  Id x x
refl {U} {X} {x} = idp x

\end{code}

We use all these notations in the following development, except 'refl'
and 'Path' at this time.

A "presheaf" on an ω-groupoid X is a function X → V into a universe V.
It is automatically functorial in the synthetic approach (see the HoTT
book). But (perhaps surprisingly) this is not needed here.

Nat A B is the type of natural transformations of presheaves on the
ω-groupoid X.  The automatic 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 :  {U V W} {X : U ̇}  (X  V ̇)  (X  W ̇)  U  V  W ̇
Nat A B =  x  A x  B x

\end{code}

To avoid function extensionality, we work with the following notions of
pointwise equality:

\begin{code}

Π :  {U V} {X : U ̇}  (X  V ̇)  U  V ̇
Π A =  x  A x

_∼_ :  {U V} {X : U ̇} {A : X  V ̇}  Π A  Π A  U  V ̇
f  g =  x  f x  g x

_≈_ :  {U V} {X : U ̇} {x : X} {A : X  V ̇}  Nat (Hom x) A  Nat (Hom x) A  U  V ̇
η  θ =  y  η y  θ y

\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 :  {U V} {X : U ̇} {x : X} (A : X  V ̇)
            Nat (Hom x) A  A x
yoneda-elem {U} {V} {X} {x} A η = η x (idp x)

\end{code}

The first use of pattern matching on the identity path (out of two) is
to define the (based) recursion principle Id-rec of the identity type
former.

Then the inverse of yoneda-elem amounts to Id-rec:

\begin{code}

Id-rec :  {U V} {X : U ̇} {x : X} (A : X  V ̇)  A x  (y : X)  x  y  A y
Id-rec _ a _ (idp x) = a

yoneda-nat :  {U V} {X : U ̇} {x : X} (A : X  V ̇)  A x  Nat (Hom x) A 
yoneda-nat = Id-rec

\end{code}

And this is the second and last use of pattern matching on identity
paths in this file:

\begin{code}

yoneda-lemma :  {U V} {X : U ̇} {x : X} {A : X  V ̇} (η : Nat (Hom x) A)
             yoneda-nat A (yoneda-elem A η)  η 
yoneda-lemma {U} {V} {X} {.x} {A} η x (idp .x) = idp (yoneda-elem A η)

\end{code}

We could use funext (twice) to get η ≡ yoneda-nat A (yoneda-elem A η).
But we deliberately work in plain MLTT, and in fact in a very spartan
subset of it as explained in the introduction.

The other way round is trivial (it holds definitionally), and is the
computation rule for the Yoneda Construction:

\begin{code}

yoneda-computation :  {U V} {X : U ̇} {x : X} {A : X  V ̇} (a : A x) 
                    yoneda-elem A (yoneda-nat A a)  a
yoneda-computation = idp 

\end{code}

The following is the HoTT synonym of yoneda-nat, with the arguments
permuted:

\begin{code}

transport :  {U V} {X : U ̇} (A : X  V ̇) {x y : X}  x  y  A x  A y
transport {U} {V} {X} A {x} {y} p a = yoneda-nat {U} {V} {X} {x} A a y p

\end{code}

The essence of the Yoneda Lemma is then that every natural
transformation from Hom x to a presheaf A is a transport, or,
equivalently, that every such natural transformation is recursively
defined.

\begin{code}

transport-lemma :  {U V} {X : U ̇} {x : X} {A : X  V ̇} (η : Nat (Hom x) A) (y : X) (p : x  y)
                 transport A p (η x (idp x))  η y p
transport-lemma = yoneda-lemma

Id-rec-lemma :  {U V} {X : U ̇} {x : X} {A : X  V ̇} (η : Nat (Hom x) A) (y : X) (p : x  y)
              Id-rec A (η x (idp x)) y p  η y p
Id-rec-lemma = yoneda-lemma

\end{code}

There are a number of special cases of interest.

Path composition, inversion and application are defined from yoneda-nat
(that is, from based path recursion or transport):

\begin{code}

source :  {U} {X : U ̇} {x y : X}  x  y  X
source {U} {X} {x} p = x

target :  {U} {X : U ̇} {x y : X}  x  y  X
target {U} {X} {x} {y} p = y

_∙_ :  {U} {X : U ̇} {x y z : X}  x  y  y  z  x  z
p  q = yoneda-nat (Id (source p)) p (target q) q

Id⁻¹  :  {U} {X : U ̇}  X  X  U ̇
Id⁻¹ x y = Id y x

_⁻¹ :  {U} {X : U ̇} {x y : X}  x  y  y  x
p ⁻¹ = yoneda-nat (Id⁻¹ (source p)) (idp (source p)) (target p) p

ap :  {U V} {X : U ̇} {A : V ̇} (f : X  A) {x y : X}  x  y  f x  f y
ap f {x} {y} = yoneda-nat  y  f x  f y) (idp (f x)) y

\end{code}

We now introduce the usual Agda notation for chains of equalities:

\begin{code}

_≡⟨_⟩_ :  {U} {X : U ̇} (x {y z} : X)  x  y  y  z  x  z
_ ≡⟨ p  q = p  q

_∎ :  {U} {X : U ̇} (x : X)  x  x
_∎ = idp

\end{code}

The function yoneda-elem is left-cancellable in the following sense:

\begin{code}

yoneda-elem-lc :  {U V} {X : U ̇} {x : X} {A : X  V ̇} (η θ : Nat (Hom x) A)             
               yoneda-elem A η  yoneda-elem A θ  η  θ
yoneda-elem-lc {U} {V} {X} {x} {A} η θ q y p =
  η y p                              ≡⟨ (yoneda-lemma η y p)⁻¹ 
  yoneda-nat A (yoneda-elem A η) y p ≡⟨ ap  e  yoneda-nat A e y p) q 
  yoneda-nat A (yoneda-elem A θ) y p ≡⟨ yoneda-lemma θ y p 
  θ y p 

\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 name the yoneda element of η:

\begin{code}

yoneda-nat' :  {U} {X : U ̇} (x {y} : X)  Hom x y  Nat (Hom y) (Hom x)
yoneda-nat' x = yoneda-nat (Hom x)

yoneda-elem' :  {U} {X : U ̇} (x {y} : X)  Nat (Hom y) (Hom x)  Hom x y
yoneda-elem' x = yoneda-elem (Hom x)

yoneda-lemma' :  {U} {X : U ̇} (x {y} : X) (η : Nat (Hom y) (Hom x)) (z : X) (p : y  z)
               (yoneda-elem' x η)  p  η z p
yoneda-lemma' {U} {X} x {y} = yoneda-lemma {U} {U} {X} {y} {Hom x}

yoneda-lemma'' :  {U} {X : U ̇} (x {y} : X) (η : Nat (Hom y) (Hom x)) (z : X) (p : y  z)
               yoneda-nat' x (yoneda-elem' x η) z p  η z p
yoneda-lemma'' {U} {X} x {y} = yoneda-lemma {U} {U} {X} {y} {Hom x}

\end{code}

The above is a generalized version of the main lemma in Hedberg's
Theorem:

\begin{code}

hedberg-lemma :  {U} {X : U ̇} (x : X) (η : Nat (Hom x) (Hom x)) (y : X) (p : x  y)
               (yoneda-elem' x η)  p  η y p
hedberg-lemma x η y p = yoneda-lemma' x η y p

\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' :  {U} {X : U ̇}  X  X  U ̇
Id' x y = Nat (Id y) (Id x)

idp' :  {U} {X : U ̇} (x : X)  Id' x x
idp' x y p = p

_◦_ :  {U V} {X : U ̇} {A B C : X  V ̇}  Nat B C  Nat A B  Nat A C
θ  η = λ y p  θ y (η y p)

_∙'_  :  {U} {X : U ̇} {x y z : X}  Id' x y  Id' y z  Id' x z
_∙'_ = _◦_

-- Cheating (because we chase equivalences):
_⁻¹' :  {U} {X : U ̇} {x y : X}  Id' x y  Id' y x
_⁻¹' {U} {X} {x} {y} η z p = yoneda-nat (Id⁻¹ z) p y (yoneda-elem (Id x) η)

\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 :  {U} {X : U ̇} {x y : X} {p : x  y}  idp x  p  p
idp-left-neutral {U} {X} {x} {y} {p} = yoneda-lemma (idp' x) y p

idp-right-neutral :  {U} {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}

yoneda-const :  {U V} {X : U ̇} {B : V ̇} {x : X} (η : Nat (Hom x)  _  B)) (y : X) (p : x  y)
              yoneda-elem  _  B) η  η y p 
yoneda-const {X} {B} {x} η = yoneda-elem-lc  y p  yoneda-elem _ η) η (idp (yoneda-elem _ η))

\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). We 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}

record Σ {U V : Universe} {X : U ̇} (A : X  V ̇) : U  V ̇ where
 constructor _,_
 field
  pr₁ : X
  pr₂ : A pr₁

open Σ public

_×_ :  {U}  U ̇  U ̇  U ̇
X × Y = Σ \(x : X)  Y

paths-from :  {U} {X : U ̇}  X  U ̇
paths-from x = Σ \y  x  y

is-center-of-contraction :  {U} (X : U ̇)  X  U ̇
is-center-of-contraction X c = (x : X)  c  x

is-contr :  {U}  U ̇  U ̇
is-contr X = Σ \(c : X)  is-center-of-contraction X c

singletons-contractible :  {U} {X : U ̇} {x : X}
                         is-center-of-contraction (paths-from x) (x , idp x)
singletons-contractible {U} {X} {x} (y , p) = yoneda-const η y p
 where
  η : Nat (Hom x)  _  paths-from x)
  η y p = (y , p)

J' :  {U V} {X : U ̇} (x : X) (B' : paths-from x  V ̇)  B' (x , idp x)   w  B' w
J' x B' b w = yoneda-nat B' b w (singletons-contractible w)

\end{code}

Finally, based path induction then reduces to J' in the obvious way:

\begin{code}

uncurry :  {U V} {X : U ̇} {x : X}  ((y : X)  x  y  V ̇)  (paths-from x  V ̇)
uncurry B (y , p) = B y p

J :  {U V} {X : U ̇} (x : X) (B : (y : X)  x  y  V ̇)
   B x (idp x)  (y : X) (p : x  y)  B y p
J x B b y p = J' 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 :  {U V} {X : U ̇} {x : X} {B : (y : X)  x  y  V ̇} (b : B x (idp x))
               J x B b x (idp x)  b
J-computation = idp
  
\end{code}

J constructed in this way has the following normal form reported by Agda:

  λ {U} {V} {X} x B b y p →
    Id-rec b
    (Id-rec
     (Id-rec (idp (Id-rec (x , idp x) p))
      (yoneda-lemma (λ y p → x , idp x) y p))
     (Id-rec (idp (Id-rec (x , idp x) p))
      (yoneda-lemma (λ y p → y , p) y p)))

Some generalities now (15th Nov 2017). Everything that follows is
proved from the Yoneda machinery rather than J, for the sake of
illustration.

\begin{code}

⁻¹-involutive :  {U} {X : U ̇} {x y : X} (p : x  y)  (p ⁻¹)⁻¹  p
⁻¹-involutive {U} {X} {x} {y} = yoneda-elem-lc  x p  (p ⁻¹)⁻¹)  x p  p) (idp(idp x)) y

⁻¹-contravariant :  {U} {X : U ̇} {x y : X} (p : x  y) {z : X} (q : y  z)
                 q ⁻¹  p ⁻¹  (p  q)⁻¹
⁻¹-contravariant {U} {X} {x} {y} p {z} = yoneda-elem-lc  z q  q ⁻¹  p ⁻¹)
                                                        z q  (p  q) ⁻¹)
                                                       idp-left-neutral
                                                       z 

left-inverse :  {U} {X : U ̇} {x y : X} (p : x  y)  p ⁻¹  p  idp y
left-inverse {U} {X} {x} {y} = yoneda-elem-lc  x p  p ⁻¹  p)  x p  idp x) (idp(idp x)) y

right-inverse :  {U} {X : U ̇} {x y : X} (p : x  y)  idp x  p  p ⁻¹
right-inverse {U} {X} {x} {y} = yoneda-const  x p  p  p ⁻¹) y

\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 :  {U} {X : U ̇} {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 {U} {X} {z} {t} = yoneda-elem-lc  z r x y p q  p  q  r)
                                            z r x y p q  p  (q  r))
                                           (idp  x y p q  p  q))
                                           t 
\end{code}

Then of course associativity of path composition follows:

\begin{code}

assoc :  {U} {X : U ̇} {x y z t : X} (p : x  y) (q : y  z) (r : z  t)
       (p  q)  r  p  (q  r)
assoc {U} {X} {x} {y} p q r = ap  f  f x y p q) (ext-assoc r) 

cancel-left :  {U} {X : U ̇} {x y z : X} {p : x  y} {q r : y  z}
             p  q  p  r  q  r
cancel-left {U} {X} {x} {y} {z} {p} {q} {r} s = 
       q              ≡⟨ idp-left-neutral ⁻¹ 
       idp y  q      ≡⟨ ap  t  t  q) ((left-inverse p)⁻¹) 
       (p ⁻¹  p)  q ≡⟨ assoc (p ⁻¹) p q 
       p ⁻¹  (p  q) ≡⟨ ap  t  p ⁻¹  t) s 
       p ⁻¹  (p  r) ≡⟨ (assoc (p ⁻¹) p r)⁻¹ 
       (p ⁻¹  p)  r ≡⟨ ap  t  t  r) (left-inverse p) 
       idp y  r      ≡⟨ idp-left-neutral 
       r 
\end{code}

Added 12 May 2015:

Contractibility also arises as follows with the Yoneda Lemma.
(see https://en.wikipedia.org/wiki/Representable_functor)

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.

   Example. An interesting instance of this is the case where X is U ̇,
   B:U ̇ and A(C)=(B≃C), in which we get that A is representable iff the
   type Σ(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 = (Π(B : U ̇), contractible(Σ(C:U ̇), B≃C)).

   We don't develop this example in this version of these Agda notes.

The Agda development of this has been added 5 Nov 2015 and 17 Nov 2017:

\begin{code}

from-Σ-Id :  {U V} {X : U ̇} (A : X  V ̇) {σ τ : Σ A}
           σ  τ
           Σ \(p : pr₁ σ  pr₁ τ)  yoneda-nat A (pr₂ σ) (pr₁ τ) p  pr₂ τ
from-Σ-Id {U} {V} {X} A {x , a} {τ} p = yoneda-nat B (idp x , idp a) τ p
 where
   B : (τ : Σ A)  U  V ̇
   B τ = Σ \(p : x  pr₁ τ)  yoneda-nat A a (pr₁ τ) p  pr₂ τ

to-Σ-Id :  {U V} {X : U ̇} (A : X  V ̇) {σ τ : Σ A}
           (Σ \(p : pr₁ σ  pr₁ τ)  yoneda-nat A (pr₂ σ) (pr₁ τ) p  pr₂ τ)
           σ  τ
to-Σ-Id {U} {X} A {x , a} {y , b} (p , q) = r
 where
  η : Nat (Hom x)  _  Σ A)
  η y p = (y , yoneda-nat A a y p)
  yc : (x , a)  (y , yoneda-nat A a y p)
  yc = yoneda-const η y p
  r : (x , a)  (y , b)
  r = yoneda-nat  b  (x , a)  (y , b)) yc b q

is-universal-element :  {U V} {X : U ̇} (A : X  V ̇)  Σ A  U  V ̇
is-universal-element A (x , a) =  y (b : A y)  Σ \(p : x  y)  yoneda-nat A a y p  b

ue-is-cc :  {U V} {X : U ̇} {A : X  V ̇}
          (σ : Σ A)  is-universal-element A σ  is-center-of-contraction (Σ A) σ
ue-is-cc {U} {V} {X} {A} (x , a) u (y , b) = to-Σ-Id A ((u y) b)

cc-is-ue :  {U V} {X : U ̇} (A : X  V ̇) 
          (σ : Σ A)  is-center-of-contraction (Σ A) σ  is-universal-element A σ
cc-is-ue A (x , a) φ y b = from-Σ-Id A {x , a} {y , b} (φ(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 {U} {X} {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:

\begin{code}

id :  {U} {X : U ̇}  X  X
id x = x

_∘_ :  {U V W} {X : U ̇} {Y : V ̇} {Z : W ̇}  (Y  Z)  (X  Y)  X  Z
(g  f) x = g(f x)

has-section :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
has-section r = Σ \s  r  s  id

has-retraction :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
has-retraction s = Σ \r  r  s  id

is-equiv :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
is-equiv f = has-section f × has-retraction f 

_≃_ :  {U V}  U ̇  V ̇  U  V ̇
X  Y = Σ \(f : X  Y)  is-equiv f

ideq :  {U} (X : U ̇)  X  X
ideq X = id , ((id , idp) , (id , idp))

Eq :  {U V}  U ̇  V ̇  U  V ̇
Eq = _≃_

universality-section :  {U V} {X : U ̇} {A : X  V ̇} (x : X) (a : A x)
                      is-universal-element A (x , a)  (y : X)  has-section(yoneda-nat A a y) 
universality-section {U} {V} {X} {A} x a u y = s y , φ y
 where
  s : Nat A (Hom x)
  s y b = pr₁ (u y b) 
  φ : (y : X) (b : A y)  yoneda-nat A a y (s y b)  b 
  φ y b = pr₂ (u y b)

\end{code}

Actually, it suffices to just give the section, as shown next
(https://github.com/HoTT/book/issues/718#issuecomment-65378867):

\begin{code}

idemp-is-id :  {U} {X : U ̇} {x : X} (η : Nat (Hom x) (Hom x)) (y : X) (p : x  y)
            η y (η y p)  η y p  η y p  p
idemp-is-id {U} {X} {x} η y p idemp = cancel-left (
        η x (idp x)  η y p ≡⟨ hedberg-lemma x η y (η y p) 
        η y (η y p)         ≡⟨ idemp 
        η y p               ≡⟨ (hedberg-lemma x η y p)⁻¹ 
        η x (idp x)  p    )

natural-section-is-equiv :  {U V} {X : U ̇} {A : X  V ̇}
                           (x : X) (r : Nat (Hom x) A)
                         ((y : X)  has-section(r y)) 
                         ((y : X)  is-equiv(r y))
natural-section-is-equiv {U} {V} {X} {A} x r hass = λ y  (hass y , hasr y)
 where
  s : Nat A (Hom x)
  s y = pr₁ (hass y)
  rs : {y : X} (a : A y)  r y (s y a)  a
  rs {y} = pr₂ (hass y)
  η : (y : X)  x  y  x  y
  η y p = s y (r y p)
  idemp : (y : X) (p : x  y)  η y (η y p)  η y p
  idemp y p = ap (s y) (rs (r y p))
  η-is-id : (y : X) (p : x  y)  η y p  p
  η-is-id y p = idemp-is-id η y p (idemp y p)
  hasr : (y : X)  has-retraction(r y)
  hasr y = s y , η-is-id y

\end{code}

We are interested in this corollary:

\begin{code}

universality-equiv :  {U V} {X : U ̇} {A : X  V ̇} (x : X) (a : A x)
                    is-universal-element A (x , a)
                    (y : X)  is-equiv(yoneda-nat A a y)
universality-equiv {U} {V} {X} {A} x a u = natural-section-is-equiv x (yoneda-nat A a)
                                                                      (universality-section x a u)
\end{code}

The converse is trivial:

\begin{code}

section-universality :  {U V} {X : U ̇} {A : X  V ̇} (x : X) (a : A x)
                      ((y : X)  has-section(yoneda-nat A a y))
                      is-universal-element A (x , a)
section-universality x a φ y b = pr₁(φ y) b , pr₂(φ y) b

equiv-universality :  {U V} {X : U ̇} {A : X  V ̇} (x : X) (a : A x)
                    ((y : X)  is-equiv(yoneda-nat A a y))
                    is-universal-element A (x , a)
equiv-universality x a φ = section-universality x a  y  pr₁ (φ y))

\end{code}

Next we show that a presheaf A is representable iff Σ A is contractible.

\begin{code}

_≊_ :  {U V} {X : U ̇}  (X  V ̇)  (X  V ̇)  U  V ̇
A  B = Σ \(η : Nat A B)   x  is-equiv(η x)

is-representable :  {U} {X : U ̇}  (X  U ̇)  U ̇
is-representable A = Σ \x  Id x  A

contr-is-repr :  {U} {X : U ̇} {A : X  U ̇}  is-contr (Σ A)  is-representable A 
contr-is-repr {U} {X} {A} ((x , a) , cc) = g
 where
  g : Σ \(x : X)  Id x  A
  g = x , (yoneda-nat A a , universality-equiv x a (cc-is-ue A (x , a) cc))

equiv-closed-under-∼ :  {U} {X Y : U ̇} (f g : X  Y)  is-equiv f   g  f   is-equiv g
equiv-closed-under-∼ {U} {X} {Y} f g ((s , fs) , (r , rf)) peq = ((s , gs) , (r , rg))
 where
  gs : (y : Y)  g(s y)  y
  gs y = g (s y) ≡⟨ peq (s y)  f (s y) ≡⟨ fs y  y 
  rg : (x : X)  r(g x)  x
  rg x = r (g x) ≡⟨ ap r (peq x)  r (f x) ≡⟨ rf x  x 

is-repr→is-equiv-yoneda :  {U} {X : U ̇} {A : X  U ̇} (x : X) (η : Nat (Id x) A) (y : X) 
                         is-equiv (η y)  is-equiv (yoneda-nat A (yoneda-elem A η) y)
is-repr→is-equiv-yoneda {U} {X} {A} x η y ise =
  equiv-closed-under-∼ (η y) (yoneda-nat A (yoneda-elem A η) y) ise (yoneda-lemma η y)

repr-is-contr :  {U} {X : U ̇} {A : X  U ̇}  is-representable A  is-contr (Σ A)
repr-is-contr {U} {X} {A} (x , (η , φ)) = g
 where
  σ : Σ A
  σ = x , yoneda-elem A η
  is-ue-σ : is-universal-element A σ
  is-ue-σ = equiv-universality x (yoneda-elem A η)  y  is-repr→is-equiv-yoneda x η y (φ y))
  g : Σ \(σ : Σ A)  is-center-of-contraction (Σ A) σ
  g = σ , ue-is-cc σ is-ue-σ

\end{code}

Here are some further consequences:

\begin{code}

paths-from-contractible :  {U} {X : U ̇} (x : X)  is-contr(paths-from x)
paths-from-contractible x = ((x , idp x) , singletons-contractible)

paths-to :  {U} {X : U ̇}  X  U ̇
paths-to x = Σ \y  y  x

rc-is-c :  {U} {X Y : U ̇} (r : X  Y)  has-section r  is-contr X  is-contr Y
rc-is-c {U} {X} {Y} r (s , rs) (x , i) = r x , λ y  r x ≡⟨ ap r (i (s y))  r (s y) ≡⟨ rs y  y 

pt-pf-equiv :  {U} {X : U ̇} (x : X)  Σ \(f : paths-from x  paths-to x)  is-equiv f
pt-pf-equiv {U} {X} x = f , ((g , fg) , (g , gf))
 where
  f : paths-from x  paths-to x
  f (y , p) = y , (p ⁻¹) 
  g : paths-to x  paths-from x
  g (y , p) = y , (p ⁻¹) 
  fg : f  g  id
  fg (y , p) = ap  p  y , p) (⁻¹-involutive p)
  gf : g  f  id
  gf (y , p) = ap  p  y , p) (⁻¹-involutive p)
  
paths-to-contractible :  {U} {X : U ̇} (x : X)  is-contr(paths-to x)
paths-to-contractible x = rc-is-c (pr₁(pt-pf-equiv x))
                                  (pr₁(pr₂((pt-pf-equiv x))))
                                  (paths-from-contractible x)

is-prop :  {U}  U ̇  U ̇
is-prop X = (x y : X)  x  y

pcubp :  {U} (X Y : U ̇)  is-prop X  is-prop Y  is-prop(X × Y)
pcubp X Y i j (x , y) (x' , y') = to-Σ-Id  _  Y) 
                                          (i x x' , j (yoneda-nat  _  Y) y x' (i x x')) y')

c-is-p :  {U} {X : U ̇}  is-contr X  is-prop X
c-is-p {U} {X} (c , φ) x y = x ≡⟨ (φ x) ⁻¹  c ≡⟨ φ y  y 

ic-is-p :  {U} {X : U ̇}  (X  is-contr X)  is-prop X
ic-is-p {U} {X} φ x = c-is-p (φ x) x

is-embedding :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
is-embedding f =  y  is-prop(Σ \x  y  f x)

is-embedding' :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
is-embedding' f =  x x'  is-equiv (ap f {x} {x'})

embedding-embedding' :  {U V} {X : U ̇} {Y : V ̇} (f : X  Y)  is-embedding f  is-embedding' f
embedding-embedding' {U} {V} {X} f ise = g
 where
  c : (x : X)  is-contr(Σ \(x' : X)  f x  f x')
  c x = (x , idp (f x)) , ise (f x) (x , idp (f x))
  g : (x x' : X)  is-equiv(ap f {x} {x'})
  g x = universality-equiv x (idp (f x)) (cc-is-ue  x'  f x  f x') (pr₁ (c x)) (pr₂ (c x))) 

embedding'-embedding :  {U V} {X : U ̇} {Y : V ̇} (f : X  Y)  is-embedding' f  is-embedding f
embedding'-embedding {U} {V} {X} {Y} f ise = g
 where
  e : (x x' : X)  is-center-of-contraction (Σ \(x' : X)  f x  f x') (x , idp (f x))
  e x x' = ue-is-cc (x , idp (f x)) (equiv-universality x (idp (f x)) (ise x))
  h : (x : X)  is-prop (Σ \(x' : X)  f x  f x')
  h x σ τ = σ ≡⟨ (e x (pr₁ σ) σ)⁻¹  (x , idp (f x)) ≡⟨ e x (pr₁ τ) τ  τ   
  g : (y : Y)  is-prop (Σ \(x' : X)  y  f x')
  g y (x , p) = transport  y  is-prop (Σ \(x' : X)  y  f x')) (p ⁻¹) (h x) (x , p)

\end{code}

9th Jun 2016:

Then it also follows that Id : X → (X → U ̇) is an embedding (the
Yoneda-embedding). In fact, the Id-fiber of A:X→U ̇ says that
A is representable, which is equivalent to the contractibility of ΣA,
which is a proposition. (Hence the injective types are the retracts of
the exponential powers of the universe.)

This works as follows in outline:

If A : X → U ̇ then the Id-fiber of A is Σ \(x : X) → Id x ≡ A.

If (x : X , p : Id x = A) is in the fiber, then

   ap Σ p : Σ (Id x) = Σ A,

and hence, being equal to a contractible type, Σ A is
contractible.

Next we have (*)

 A x ≃ Nat (Id x) A             (yoneda)
     = (y : Y) → Id x y → A y   (definition)
     ≃ (y : Y) → Id x y ≃ A y   (because Σ A is contractible (Yoneda corollary))
     ≃ (y : Y) → Id x y ≡ A y   (by univalence)
     ≃ Id x ≡ A                 (by function extensionality)

Hence the type Σ \(x : X) → Id x ≡ A y is contractible, because Σ A is
contractible, which shows that Id : X → (X → U) is an embedding.

2017:

This relies on univalence. But less than that suffices
(https://groups.google.com/forum/#!topic/homotopytypetheory/bKti7krHM-c)

First, Evan Cavallo showed that it is enough to assume funext and that
the canonical map X ≡ Y → X ≃ Y is an embedding. Then, using this idea
and the above proof outline, we further generalized this to assume
that the canonical map X ≡ Y → (X → Y) is left-cancellable (which is
much weaker than assuming that it is an embedding).

This is what we record next (9th December 2017), using the original
idea (*) in the weakened form discussed above.

We have already defined is-embedding, and the next definition is
equivalent, although we don't need to pause to show this.

\begin{code}

is-Embedding :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
is-Embedding f =  y  is-prop(Σ \x  f x  y)

left-cancellable :  {U V} {X : U ̇} {Y : V ̇}  (X  Y)  U  V ̇
left-cancellable f =  x x'  f x  f x'  x  x'

lcccomp :  {U V W} {X : U ̇} {Y : V ̇} {Z : W ̇} (f : X  Y) (g : Y  Z)
         left-cancellable f  left-cancellable g  left-cancellable (g  f)
lcccomp f g lcf lcg x x' = lcf x x'  lcg (f x) (f x')

\end{code}

If the codomain of a left-cancellable function is a proposition, so is
its domain. 

\begin{code}

lcmtpip :  {U V} {X : U ̇} {Y : V ̇} (f : X  Y)  left-cancellable f  is-prop Y  is-prop X
lcmtpip f lc i x x' = lc x x' (i (f x) (f x'))

\end{code}

We next consider sums and products of families of left-cancellable
maps, which again give left-cancellable maps.

\begin{code}

NatΣ :  {U V W} {X : U ̇} {A : X  V ̇} {B : X  W ̇}  Nat A B  Σ A  Σ B
NatΣ ζ (x , a) = (x , ζ x a)

NatΣ-lc :  {U V W} (X : U ̇) (A : X  V ̇) (B : X  W ̇) (ζ : 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 B pq)
    η : Nat (Hom x) B
    η = yoneda-nat B (ζ x a)
    q : η y p  ζ y b
    q = pr₂ (from-Σ-Id B pq)
    θ : Nat (Hom x) A
    θ = yoneda-nat A a
    η' : Nat (Hom x) B
    η' y p = ζ y (θ y p)
    r : η'  η
    r = yoneda-elem-lc η' η (idp (ζ x a)) 
    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 (θ y p) b s
    g : x , a  y , b
    g = to-Σ-Id A (p , t)

NatΠ :  {U V W} {X : U ̇} {A : X  V ̇} {B : X  W ̇}  Nat A B  Π A  Π B
NatΠ f g x = f x (g x) -- (S combinator from combinatory logic!)

happly :  {U V} {X : U ̇} {A : X  V ̇} (f g : Π A)  f  g  f  g
happly f g p x = ap  h  h x) p

NatΠ-lc :  {U V W} {X : U ̇} {A : X  V ̇} {B : X  W ̇} (f : Nat A B)
     ((x : X)  left-cancellable(f x))
     (g g' : Π A)  NatΠ f g  NatΠ f g'  g  g'
NatΠ-lc f flc g g' p x = flc x (g x) (g' x) (q x)
 where
   q :  x  f x (g x)  f x (g' x)
   q = happly (NatΠ f g) (NatΠ f g') p

\end{code}

Any section is left-cancellable, of course:

\begin{code}

section-lc :  {U V} {X : U ̇} {A : V ̇} (s : X  A)  has-retraction s  left-cancellable s
section-lc {U} {V} {X} {Y} s (r , rs) x y p = (rs x)⁻¹  ap r p  rs y

\end{code}

The function-extensionality principle in its univalent mathematics manifestation:

\begin{code}

FunExt :  U V  U   V  ̇
FunExt U V = {X : U ̇} {A : X  V ̇} (f g : Π A)  is-equiv (happly f g)

≃-funext :  U V  FunExt U V  {X : U ̇} {A : X  V ̇} (f g : Π A)
          (f  g)  ((x : X)  f x  g x)
≃-funext U V fe f g = happly f g , fe f g

funext :  {U V} (fe : FunExt U V) {X : U ̇} {A : X  V ̇} (f g : Π A) 
       ((x : X)  f x  g x)  f  g
funext fe f g = pr₁(pr₁(fe f g))

happly-funext :  {U V} {X : U ̇} {A : X  V ̇}
                (fe : FunExt U V) (f g : Π A) (h : f  g)
               happly f g (funext fe f g h)  h
happly-funext fe f g = pr₂(pr₁(fe f g))

happly-lc :  {U V} {X : U ̇} {A : X  V ̇} (fe : FunExt U V) (f g : Π A) 
          left-cancellable(happly f g)
happly-lc fe f g = section-lc (happly f g) ((pr₂ (fe f g)))

eqtofun :  {U V} (X : U ̇)  Nat (Eq X)  (Y : V ̇)  X  Y)
eqtofun X Y (f , _) = f

idtoeq :  {U} (X : U ̇)  Nat (Id X) (Eq X)
idtoeq X = yoneda-nat (Eq X) (ideq X)

idtofun :  {U} (X : U ̇)  Nat (Id X)  Y  X  Y)
idtofun X Y p = eqtofun X Y (idtoeq X Y p)

idtofun' :  {U} (X : U ̇)  Nat (Id X)  Y  X  Y)
idtofun' X = yoneda-nat  Y  X  Y) id

idtofun-agree :  {U} (X : U ̇)  idtofun X  idtofun' X
idtofun-agree X = yoneda-elem-lc (idtofun X) (idtofun' X) (idp id)

idtofun-is-equiv :  {U} (X Y : U ̇) (p : X  Y)  is-equiv(idtofun X Y p)
idtofun-is-equiv X Y p = pr₂(idtoeq X Y p)

\end{code}

Id : X → (X → U) is left-cancellable:

\begin{code}

Id-lc :  {U} {X : U ̇}  left-cancellable (Id {U} {X})
Id-lc {U} {X} x y p = idtofun (Id y y) (Id x y) (happly (Id y) (Id x) (p ⁻¹) y) (idp y)

\end{code}

The Id Embedding Lemma. The idea is to show that the type 
T := Σ \(x : X) → Id x ≡ A is a proposition by showing that there is a
left-cancellable map from it to a proposition, namely the contractible
type Σ A.

\begin{code}

Id-Embedding-Lemma :  {U}  FunExt U U  FunExt U (U )  {X : U ̇}
                   ((x y : X) (A : X  U ̇)  left-cancellable (idtofun (Id x y) (A y))) 
                   is-Embedding(Id {U} {X})
Id-Embedding-Lemma {U} fe fe' {X} iflc A (x₀ , p₀) = h (x₀ , p₀)
 where
  T = Σ \(x : X)  Id x  A
  q : Σ (Id x₀)  Σ A
  q = ap Σ p₀
  c : is-contr(Σ A)
  c = yoneda-nat is-contr (paths-from-contractible x₀) (Σ A) q
  f₀ : (x : X)  Id x  A  (y : X)  Id x y  A y
  f₀ x = happly (Id x) A
  f₁ : (x : X)  ((y : X)  Id x y  A y)  (y : X)  Id x y  A y
  f₁ x = NatΠ  y  idtofun (Id x y) (A y))
  f₂ : (x : X)  Nat (Id x) A  A x
  f₂ x = yoneda-elem A
  f : (x : X)  Id x  A  A x
  f x = f₂ x  f₁ x  f₀ x
  f₀-lc : (x : X)  left-cancellable(f₀ x)
  f₀-lc x = happly-lc fe' (Id x) A
  f₁-lc : (x : X)  left-cancellable(f₁ x)
  f₁-lc x = g
    where
      l :  φ φ'  f₁ x φ  f₁ x φ'  (x : X)  φ x  φ' x
      l = NatΠ-lc  y  idtofun (Id x y) (A y))  y  iflc x y A)
      g :  φ φ'  f₁ x φ  f₁ x φ'  φ  φ'
      g φ φ' p = funext fe' φ φ' (l φ φ' p)
  f₂-lc : (x : X)  left-cancellable(f₂ x)
  f₂-lc x η η' p = funext fe η η'  y  funext fe (η y) (η' y) (l y))
    where
      l : η  η'
      l = yoneda-elem-lc η η' p
  f-lc : (x : X)  left-cancellable(f x)
  f-lc x = lcccomp (f₀ x) (f₂ x  f₁ x) (f₀-lc x) (lcccomp (f₁ x) (f₂ x) (f₁-lc x) (f₂-lc x))
  g : T  Σ A
  g = NatΣ f 
  g-lc : left-cancellable g
  g-lc = NatΣ-lc X  x  Id x  A) A f f-lc 
  h : is-prop T
  h = lcmtpip g g-lc (c-is-p c)

\end{code}

The definition of a univalent universe and basic consequences:

\begin{code}

is-univalent :  U  U  ̇
is-univalent U = (X Y : U ̇)  is-equiv(idtoeq X Y)

eqtoid :  {U}  is-univalent U  (X Y : U ̇)  X  Y  X  Y 
eqtoid ua X Y = pr₁(pr₁(ua X Y))

idtoeq-eqtoid :  {U} (ua : is-univalent U)
               (X Y : U ̇) (e : X  Y)  idtoeq X Y (eqtoid ua X Y e)  e
idtoeq-eqtoid ua X Y = pr₂(pr₁(ua X Y))

is-univalent-≃ :  {U}  is-univalent U  (X Y : U ̇)  (X  Y)  (X  Y)
is-univalent-≃ ua X Y = idtoeq X Y , ua X Y

is-univalent-idtoeq-lc :  {U}  is-univalent U  (X Y : U ̇)  left-cancellable(idtoeq X Y)
is-univalent-idtoeq-lc ua X Y = section-lc (idtoeq X Y) (pr₂ (ua X Y))

\end{code}

The funext map is left-cancellable:

\begin{code}

funext-lc :  {U V} {X : U ̇} {A : X  V ̇} (fe : FunExt U V) 
          (f g : Π A)  left-cancellable(funext fe f g)
funext-lc fe f g = section-lc (funext fe f g) (happly f g , happly-funext fe f g)

\end{code}

The fact that idtofun is an equivalence is a proposition, assuming
function extensionality:

\begin{code}

jip' :  {U} (fe : FunExt U U) (X Y : U ̇) (p : X  Y)  is-prop(is-equiv(idtofun X Y p))
jip' {U} fe X = J X B go -- Only use of J in this file (can we get rid of it?)
 where
   B : (Y : U ̇)  X  Y  U ̇
   B Y p = is-prop(is-equiv(idtofun X Y p))
   A = Σ \(f : X  X)  f  id
   a : is-prop A
   a = c-is-p (paths-to-contractible id)
   A' = Σ \(f : X  X)  f  id
   η : (f : X  X)  f  id  f  id
   η f = funext fe f id
   η-lc : (f : X  X)  left-cancellable(η f)
   η-lc f = funext-lc fe f id
   h : A'  A
   h = NatΣ η
   h-lc : left-cancellable h
   h-lc = NatΣ-lc (X  X)  f  f  id)  f  f  id) η η-lc
   b : is-prop A'
   b = lcmtpip h h-lc a
   go : is-prop(A' × A')
   go = pcubp A' A' b b

\end{code}

Equivalences are propositions, assuming univalence (and function
extensionality) (but also without the univalence assumption, although
we don't bother):

\begin{code}

jip :  {U}  is-univalent U  FunExt U U  {X Y : U ̇} 
    (f : X  Y)  is-prop(is-equiv f) 
jip {U} ua fe {X} {Y} f ije = h ije
  where
    e : X  Y
    e = (f , ije)
    p : X  Y
    p = eqtoid ua X Y e
    f' : X  Y
    f' = idtofun X Y p
    h' : is-prop(is-equiv f')
    h' = jip' fe X Y p
    ije' : is-equiv f'
    ije' = idtofun-is-equiv X Y p
    e' : X  Y
    e' = f' , ije'
    q : e'  e
    q = idtoeq-eqtoid ua X Y e
    q₁ : f'  f
    q₁ = ap pr₁ q
    h : is-prop(is-equiv f)
    h = yoneda-nat  f  is-prop(is-equiv f)) h' f q₁

\end{code}

The map eqtofun is left-cancellable assuming univalence (and function
extensionality, which is a consequence of univalence, but we don't
bother):

\begin{code}

eqtofun-lc :  {U}  is-univalent U  FunExt U U 
            (X Y : U ̇)  left-cancellable(eqtofun X Y)
eqtofun-lc ua fe X Y (f , jef) (g , jeg) p = go
 where
  q : yoneda-nat is-equiv jef g p  jeg
  q = jip ua fe g (yoneda-nat is-equiv jef g p) jeg
  go : f , jef  g , jeg
  go = to-Σ-Id is-equiv (p , q)
  
\end{code}

The map idtofun is left-cancellable assuming univalence (and funext):

\begin{code}

is-univalent-idtofun-lc :  {U}  is-univalent U  FunExt U U  (X Y : U ̇) 
                        left-cancellable(idtofun X Y)
is-univalent-idtofun-lc  ua fe X Y = 
   lcccomp (idtoeq X Y) (eqtofun X Y) (is-univalent-idtoeq-lc ua X Y) (eqtofun-lc ua fe X Y)

\end{code}

Univalence implies that the function Id_X : X → (X → U) is an embedding.
  
\begin{code}

UA-Id-embedding-Theorem :  {U}  is-univalent U  FunExt U U  FunExt U (U ) 
                        {X : U ̇}  is-Embedding(Id {U} {X})
UA-Id-embedding-Theorem {U} ua fe fe' {X} = Id-Embedding-Lemma fe fe' 
                                             x y a  is-univalent-idtofun-lc ua fe (Id x y) (a y))

\end{code}

Streicher's K-axiom:

\begin{code}

is-set :  {U}  U ̇  U ̇
is-set X = {x y : X}  x  y

K :  U  U  ̇
K U = (X : U ̇)  is-set X

\end{code}

Implies that istofun is left-cancellable:

\begin{code}

K-idtofun-lc :  {U}  K (U ) 
             {X : U ̇} (x y : X) (A : X  U ̇)  left-cancellable(idtofun (Id x y) (A y))
K-idtofun-lc {U} k {X} x y A p q r = k (Id (Id x y) (A y))

\end{code}

The K axiom and function extensionality together imply that the
function Id : X → (X → U) is an embedding.

\begin{code}

K-id-embedding-Theorem' :  {U}  K (U )  FunExt U U  FunExt U (U ) 
                        {X : U ̇}  is-Embedding(Id {U} {X})
K-id-embedding-Theorem' {U} k fe fe' {X} = Id-Embedding-Lemma fe fe' (K-idtofun-lc k) 

\end{code}

But actually function extensionality is not needed for this: K alone suffices.

\begin{code}

K-lc-e :  {U V}  {X : U ̇} {Y : V ̇} (f : X  Y)  left-cancellable f  K V  is-Embedding f
K-lc-e {U} {V} {X} {Y} f f-lc k y (x , p) (x' , p') = to-Σ-Id  x  f x  y) (r , q)
 where
   r : x  x'
   r = f-lc x x' (p  (p' ⁻¹))
   q : yoneda-nat  x  f x  y) p x' r  p'
   q = k (Id (f x') y)

K-id-embedding-Theorem :  {U}  K (U )  {X : U ̇}  is-Embedding(Id {U} {X})
K-id-embedding-Theorem {U} k {X} = K-lc-e Id Id-lc k

\end{code}











Here are the needed precedences for the above code to parse correctly:

\begin{code}

infixl 4  _,_
infixl 5  _∘_
infix  4  _∼_
infix  1  _≡_
infix  3  _⁻¹
infixl 2  _∙_
infix  1  _∎
infixr 0  _≡⟨_⟩_ 

\end{code}