Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.Yoneda where

open import MGS.Unique-Existence public
open import MGS.Embeddings public

𝓨 : {X : 𝓀 Μ‡ } β†’ X β†’ (X β†’ 𝓀 Μ‡ )
𝓨 {𝓀} {X} = Id X

π‘Œ : (X : 𝓀 Μ‡ ) β†’ X β†’ (X β†’ 𝓀 Μ‡ )
π‘Œ {𝓀} X = 𝓨 {𝓀} {X}

transport-lemma : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
                β†’ (Ο„ : Nat (𝓨 x) A)
                β†’ (y : X) (p : x ＝ y) β†’ Ο„ y p ＝ transport A p (Ο„ x (refl x))

transport-lemma A x Ο„ x (refl x) = refl (Ο„ x (refl x))

𝓔 : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X) β†’ Nat (𝓨 x) A β†’ A x
𝓔 A x Ο„ = Ο„ x (refl x)

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

yoneda-Ξ· : dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 π“₯
         β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
         β†’ 𝓝 A x ∘ 𝓔 A x ∼ id

yoneda-Ξ· fe fe' A x = Ξ³
 where
  Ξ³ : (Ο„ : Nat (𝓨 x) A) β†’ (Ξ» y p β†’ transport A p (Ο„ x (refl x))) ＝ Ο„
  Ξ³ Ο„ = fe (Ξ» y β†’ fe' (Ξ» p β†’ (transport-lemma A x Ο„ y p)⁻¹))

yoneda-Ξ΅ : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
         β†’ 𝓔 A x ∘ 𝓝 A x ∼ id

yoneda-Ξ΅ A x = Ξ³
 where
  Ξ³ : (a : A x) β†’ transport A (refl x) a ＝ a
  Ξ³ = refl

is-fiberwise-equiv : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
is-fiberwise-equiv Ο„ = βˆ€ x β†’ is-equiv (Ο„ x)

𝓔-is-equiv : dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 π“₯
           β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
           β†’ is-fiberwise-equiv (𝓔 A)

𝓔-is-equiv fe fe' A x = invertibles-are-equivs (𝓔 A x )
                         (𝓝 A x , yoneda-Ξ· fe fe' A x , yoneda-Ξ΅ A x)

𝓝-is-equiv : dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 π“₯
           β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
           β†’ is-fiberwise-equiv (𝓝 A)

𝓝-is-equiv fe fe' A x = invertibles-are-equivs (𝓝 A x)
                         (𝓔 A x , yoneda-Ξ΅ A x , yoneda-Ξ· fe fe' A x)

Yoneda-Lemma : dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 π“₯
             β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
             β†’ Nat (𝓨 x) A ≃ A x

Yoneda-Lemma fe fe' A x = 𝓔 A x , 𝓔-is-equiv fe fe' A x

retract-universal-lemma : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
                        β†’ ((y : X) β†’ A y ◁ (x ＝ y))
                        β†’ βˆƒ! A

retract-universal-lemma A x ρ = i
 where
  Οƒ : Ξ£ A ◁ singleton-type' x
  Οƒ = Ξ£-retract ρ

  i : βˆƒ! A
  i = retract-of-singleton Οƒ (singleton-types'-are-singletons (domain A) x)

fiberwise-equiv-universal : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                            (x : X) (Ο„ : Nat (𝓨 x) A)
                          β†’ is-fiberwise-equiv Ο„
                          β†’ βˆƒ! A

fiberwise-equiv-universal A x Ο„ e = retract-universal-lemma A x ρ
 where
  ρ : βˆ€ y β†’ A y ◁ (x ＝ y)
  ρ y = ≃-gives-β–· ((Ο„ y) , e y)

universal-fiberwise-equiv : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                          β†’ βˆƒ! A
                          β†’ (x : X) (Ο„ : Nat (𝓨 x) A) β†’ is-fiberwise-equiv Ο„

universal-fiberwise-equiv {𝓀} {π“₯} {X} A u x Ο„ = Ξ³
 where
  g : singleton-type' x β†’ Ξ£ A
  g = NatΞ£ Ο„

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

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

hfunextβ†’ : hfunext 𝓀 π“₯
         β†’ ((X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (f : Ξ  A) β†’ βˆƒ! g κž‰ Ξ  A , f ∼ g)

hfunextβ†’ hfe X A f = fiberwise-equiv-universal (f ∼_) f (happly f) (hfe f)

β†’hfunext : ((X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (f : Ξ  A) β†’ βˆƒ! g κž‰ Ξ  A , f ∼ g)
         β†’ hfunext 𝓀 π“₯

β†’hfunext Ο† {X} {A} f = universal-fiberwise-equiv (f ∼_) (Ο† X A f) f (happly f)

fiberwise-equiv-criterion : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                            (x : X)
                          β†’ ((y : X) β†’ A y ◁ (x ＝ y))
                          β†’ (Ο„ : Nat (𝓨 x) A) β†’ is-fiberwise-equiv Ο„

fiberwise-equiv-criterion A x ρ Ο„ = universal-fiberwise-equiv A
                                     (retract-universal-lemma A x ρ) x Ο„

fiberwise-equiv-criterion' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                            (x : X)
                          β†’ ((y : X) β†’ (x ＝ y) ≃ A y)
                          β†’ (Ο„ : Nat (𝓨 x) A) β†’ is-fiberwise-equiv Ο„

fiberwise-equiv-criterion' A x e = fiberwise-equiv-criterion A x
                                    (Ξ» y β†’ ≃-gives-β–· (e y))

_≃̇_ : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
A ≃̇ B = βˆ€ x β†’ A x ≃ B x

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

representable-universal : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                        β†’ is-representable A
                        β†’ βˆƒ! A

representable-universal A (x , e) = retract-universal-lemma A x
                                     (Ξ» x β†’ ≃-gives-β–· (e x))

universal-representable : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                        β†’ βˆƒ! A
                        β†’ is-representable A

universal-representable {𝓀} {π“₯} {X} {A} ((x , a) , p) = x , Ο†
 where
  e : is-fiberwise-equiv (𝓝 A x a)
  e = universal-fiberwise-equiv A ((x , a) , p) x (𝓝 A x a)

  Ο† : (y : X) β†’ (x ＝ y) ≃ A y
  Ο† y = (𝓝 A x a y , e y)

fiberwise-retractions-are-equivs : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (x : X)
                                 β†’ (Ο„ : Nat (𝓨 x) A)
                                 β†’ ((y : X) β†’ has-section (Ο„ y))
                                 β†’ is-fiberwise-equiv Ο„

fiberwise-retractions-are-equivs {𝓀} {π“₯} {X} A x Ο„ s = Ξ³
 where
  ρ : (y : X) β†’ A y ◁ (x ＝ y)
  ρ y = Ο„ y , s y

  i : βˆƒ! A
  i = retract-universal-lemma A x ρ

  Ξ³ : is-fiberwise-equiv Ο„
  Ξ³ = universal-fiberwise-equiv A i x Ο„

fiberwise-◁-gives-≃ : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (x : X)
                    β†’ ((y : X) β†’ A y ◁ (x ＝ y))
                    β†’ ((y : X) β†’ A y ≃ (x ＝ y))

fiberwise-◁-gives-≃ X A x ρ = Ξ³
 where
  f : (y : X) β†’ (x ＝ y) β†’ A y
  f y = retraction (ρ y)

  e : is-fiberwise-equiv f
  e = fiberwise-retractions-are-equivs A x f (Ξ» y β†’ retraction-has-section (ρ y))

  Ξ³ : (y : X) β†’ A y ≃ (x ＝ y)
  Ξ³ y = ≃-sym (f y , e y)

embedding-criterion' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                     β†’ ((x x' : X) β†’ (f x ＝ f x') ◁ (x ＝ x'))
                     β†’ is-embedding f

embedding-criterion' f ρ = embedding-criterion f
                            (Ξ» x β†’ fiberwise-◁-gives-≃ (domain f)
                                    (Ξ» - β†’ f x ＝ f -) x (ρ x))

being-fiberwise-equiv-is-subsingleton : global-dfunext
                                      β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
                                      β†’ (Ο„ : Nat A B)
                                      β†’ is-subsingleton (is-fiberwise-equiv Ο„)

being-fiberwise-equiv-is-subsingleton fe Ο„ =
 Ξ -is-subsingleton fe (Ξ» y β†’ being-equiv-is-subsingleton fe fe (Ο„ y))

being-representable-is-subsingleton : global-dfunext
                                    β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                                    β†’ is-subsingleton (is-representable A)

being-representable-is-subsingleton fe {X} A rβ‚€ r₁ = Ξ³
 where
  u : βˆƒ! A
  u = representable-universal A rβ‚€

  i : (x : X) (Ο„ : Nat (𝓨 x) A) β†’ is-singleton (is-fiberwise-equiv Ο„)
  i x Ο„ = pointed-subsingletons-are-singletons
           (is-fiberwise-equiv Ο„)
           (universal-fiberwise-equiv A u x Ο„)
           (being-fiberwise-equiv-is-subsingleton fe Ο„)

  Ξ΅ : (x : X) β†’ (𝓨 x ≃̇ A) ≃ A x
  Ξ΅ x = ((y : X) β†’ 𝓨 x y ≃ A y)                       β‰ƒβŸ¨ Ξ Ξ£-distr-≃ ⟩
        (Ξ£ Ο„ κž‰ Nat (𝓨 x) A , is-fiberwise-equiv Ο„)    β‰ƒβŸ¨ pr₁-≃ (i x) ⟩
        Nat (𝓨 x) A                                   β‰ƒβŸ¨ Yoneda-Lemma fe fe A x ⟩
        A x                                           β– 

  Ξ΄ : is-representable A ≃ Ξ£ A
  Ξ΄ = Ξ£-cong Ξ΅

  v : is-singleton (is-representable A)
  v = equiv-to-singleton Ξ΄ u

  Ξ³ : rβ‚€ ＝ r₁
  Ξ³ = singletons-are-subsingletons (is-representable A) v rβ‚€ r₁

𝓨-is-embedding : Univalence β†’ (X : 𝓀 Μ‡ ) β†’ is-embedding (π‘Œ X)
𝓨-is-embedding {𝓀} ua X A = Ξ³
 where
  hfe : global-hfunext
  hfe = univalence-gives-global-hfunext ua

  dfe : global-dfunext
  dfe = univalence-gives-global-dfunext ua

  p = Ξ» x β†’ (𝓨 x ＝ A)                 β‰ƒβŸ¨ i  x ⟩
            ((y : X) β†’ 𝓨 x y ＝ A y)   β‰ƒβŸ¨ ii x ⟩
            ((y : X) β†’ 𝓨 x y ≃ A y)   β– 
    where
     i  = Ξ» x β†’ (happly (𝓨 x) A , hfe (𝓨 x) A)
     ii = Ξ» x β†’ Ξ -cong dfe dfe
                 (Ξ» y β†’ univalence-≃ (ua 𝓀)
                         (𝓨 x y) (A y))

  e : fiber 𝓨 A ≃ is-representable A
  e = Ξ£-cong p

  Ξ³ : is-subsingleton (fiber 𝓨 A)
  Ξ³ = equiv-to-subsingleton e (being-representable-is-subsingleton dfe A)

\end{code}