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.More-FunExt-Consequences where

open import MGS.HAE public
open import MGS.Subsingleton-Theorems public

being-subsingleton-is-subsingleton : dfunext 𝓀 𝓀
                                   β†’  {X : 𝓀 Μ‡ }
                                   β†’ is-subsingleton (is-subsingleton X)

being-subsingleton-is-subsingleton fe {X} i j = c
 where
  l : is-set X
  l = subsingletons-are-sets X i

  a : (x y : X) β†’ i x y = j x y
  a x y = l x y (i x y) (j x y)

  b : (x : X) β†’ i x = j x
  b x = fe (a x)

  c : i = j
  c = fe b

being-center-is-subsingleton : dfunext 𝓀 𝓀
                             β†’ {X : 𝓀 Μ‡ } (c : X)
                             β†’ is-subsingleton (is-center X c)

being-center-is-subsingleton fe {X} c Ο† Ξ³ = k
 where
  i : is-singleton X
  i = c , Ο†

  j : (x : X) β†’ is-subsingleton (c = x)
  j x = singletons-are-sets X i c x

  k : Ο† = Ξ³
  k = fe (Ξ» x β†’ j x (Ο† x) (Ξ³ x))

Ξ -is-set : hfunext 𝓀 π“₯
         β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
         β†’ ((x : X) β†’ is-set (A x)) β†’ is-set (Ξ  A)

Ξ -is-set hfe s f g = b
 where
  a : is-subsingleton (f ∼ g)
  a p q = Ξ³
   where
    h : βˆ€ x β†’  p x = q x
    h x = s x (f x) (g x) (p x) (q x)
    γ : p =  q
    Ξ³ = hfunext-gives-dfunext hfe h

  e : (f = g) ≃ (f ∼ g)
  e = (happly f g , hfe f g)

  b : is-subsingleton (f = g)
  b = equiv-to-subsingleton e a

being-set-is-subsingleton : dfunext 𝓀 𝓀
                          β†’ {X : 𝓀 Μ‡ }
                          β†’ is-subsingleton (is-set X)

being-set-is-subsingleton fe = Ξ -is-subsingleton fe
                                (Ξ» x β†’ Ξ -is-subsingleton fe
                                (Ξ» y β†’ being-subsingleton-is-subsingleton fe))

hlevel-relation-is-subsingleton : dfunext 𝓀 𝓀
                                β†’ (n : β„•) (X : 𝓀 Μ‡ )
                                β†’ is-subsingleton (X is-of-hlevel n)

hlevel-relation-is-subsingleton {𝓀} fe zero X =
 being-singleton-is-subsingleton fe

hlevel-relation-is-subsingleton fe (succ n) X =
 Ξ -is-subsingleton fe
  (Ξ» x β†’ Ξ -is-subsingleton fe
  (Ξ» x' β†’ hlevel-relation-is-subsingleton fe n (x = x')))

●-assoc : dfunext 𝓣 (𝓀 βŠ” 𝓣) β†’ dfunext (𝓀 βŠ” 𝓣) (𝓀 βŠ” 𝓣)
        β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {T : 𝓣 Μ‡ }
          (Ξ± : X ≃ Y) (Ξ² : Y ≃ Z) (Ξ³ : Z ≃ T)
        β†’ Ξ± ● (Ξ² ● Ξ³) = (Ξ± ● Ξ²) ● Ξ³

●-assoc fe fe' (f , a) (g , b) (h , c) = ap (h ∘ g ∘ f ,_) q
 where
  d e : is-equiv (h ∘ g ∘ f)
  d = ∘-is-equiv (∘-is-equiv c b) a
  e = ∘-is-equiv c (∘-is-equiv b a)

  q : d = e
  q = being-equiv-is-subsingleton fe fe' (h ∘ g ∘ f) _ _

≃-sym-involutive : dfunext π“₯ (𝓀 βŠ” π“₯) β†’ dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯) β†’
                   {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (Ξ± : X ≃ Y)
                 β†’ ≃-sym (≃-sym Ξ±) = Ξ±

≃-sym-involutive fe fe' (f , a) = to-subtype-=
                                   (being-equiv-is-subsingleton fe fe')
                                   (inversion-involutive f a)

≃-sym-is-equiv : dfunext π“₯ (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
               β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
               β†’ is-equiv (≃-sym {𝓀} {π“₯} {X} {Y})

≃-sym-is-equiv feβ‚€ fe₁ feβ‚‚ = invertibles-are-equivs ≃-sym
                              (≃-sym ,
                               ≃-sym-involutive feβ‚€ feβ‚‚ ,
                               ≃-sym-involutive fe₁ feβ‚‚)

≃-sym-≃ : dfunext π“₯ (𝓀 βŠ” π“₯) β†’ dfunext 𝓀 (𝓀 βŠ” π“₯) β†’ dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
        β†’ (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
        β†’ (X ≃ Y) ≃ (Y ≃ X)

≃-sym-≃ feβ‚€ fe₁ feβ‚‚ X Y = ≃-sym , ≃-sym-is-equiv feβ‚€ fe₁ feβ‚‚

Ξ -cong : dfunext 𝓀 π“₯ β†’ dfunext 𝓀 𝓦
       β†’ {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Y' : X β†’ 𝓦 Μ‡ }
       β†’ ((x : X) β†’ Y x ≃ Y' x) β†’ Ξ  Y ≃ Ξ  Y'

Ξ -cong fe fe' {X} {Y} {Y'} Ο† = invertibility-gives-≃ F (G , GF , FG)
 where
  f : (x : X) β†’ Y x β†’ Y' x
  f x = ⌜ Ο† x ⌝

  e : (x : X) β†’ is-equiv (f x)
  e x = ⌜⌝-is-equiv (Ο† x)

  g : (x : X) β†’ Y' x β†’ Y x
  g x = inverse (f x) (e x)

  fg : (x : X) (y' : Y' x) β†’ f x (g x y') = y'
  fg x = inverses-are-sections (f x) (e x)

  gf : (x : X) (y : Y x) β†’ g x (f x y) = y
  gf x = inverses-are-retractions (f x) (e x)

  F : ((x : X) β†’ Y x) β†’ ((x : X) β†’ Y' x)
  F Ο† x = f x (Ο† x)

  G : ((x : X) β†’ Y' x) β†’ (x : X) β†’ Y x
  G Ξ³ x = g x (Ξ³ x)

  FG : (Ξ³ : ((x : X) β†’ Y' x)) β†’ F (G Ξ³) = Ξ³
  FG Ξ³ = fe' (Ξ» x β†’ fg x (Ξ³ x))

  GF : (Ο† : ((x : X) β†’ Y x)) β†’ G (F Ο†) = Ο†
  GF Ο† = fe (Ξ» x β†’ gf x (Ο† x))

hfunext-≃ : hfunext 𝓀 π“₯
          β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f g : Ξ  A)
          β†’ (f = g) ≃ (f ∼ g)

hfunext-≃ hfe f g = (happly f g , hfe f g)

hfunextβ‚‚-≃ : hfunext 𝓀 (π“₯ βŠ” 𝓦) β†’ hfunext π“₯ 𝓦
           β†’ {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {A : (x : X) β†’ Y x β†’ 𝓦 Μ‡ }
             (f g : (x : X) (y : Y x) β†’ A x y)
           β†’ (f = g) ≃ (βˆ€ x y β†’ f x y = g x y)

hfunextβ‚‚-≃ fe fe' {X} f g =

 (f = g)                  β‰ƒβŸ¨ i ⟩
 (βˆ€ x β†’ f x = g x)        β‰ƒβŸ¨ ii ⟩
 (βˆ€ x y β†’ f x y = g x y)  β– 

 where
  i  = hfunext-≃ fe f g
  ii = Ξ -cong
        (hfunext-gives-dfunext fe)
        (hfunext-gives-dfunext fe)
        (Ξ» x β†’ hfunext-≃ fe' (f x) (g x))

precomp-invertible : dfunext π“₯ 𝓦 β†’ dfunext 𝓀 𝓦
                   β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y)
                   β†’ invertible f
                   β†’ invertible (Ξ» (h : Y β†’ Z) β†’ h ∘ f)

precomp-invertible fe fe' {X} {Y} {Z} f (g , Ξ· , Ξ΅) = (g' , Ξ·' , Ξ΅')
 where
  f' : (Y β†’ Z) β†’ (X β†’ Z)
  f' h = h ∘ f

  g' : (X β†’ Z) β†’ (Y β†’ Z)
  g' k = k ∘ g

  Ξ·' : (h : Y β†’ Z) β†’ g' (f' h) = h
  Ξ·' h = fe (Ξ» y β†’ ap h (Ξ΅ y))

  Ξ΅' : (k : X β†’ Z) β†’ f' (g' k) = k
  Ξ΅' k = fe' (Ξ» x β†’ ap k (Ξ· x))

dprecomp : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ ) (f : X β†’ Y)
         β†’ Ξ  A β†’ Ξ  (A ∘ f)

dprecomp A f = _∘ f

dprecomp-is-equiv : dfunext 𝓀 𝓦
                  β†’ dfunext π“₯ 𝓦
                  β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ ) (f : X β†’ Y)
                  β†’ is-equiv f
                  β†’ is-equiv (dprecomp A f)

dprecomp-is-equiv fe fe' {X} {Y} A f i = invertibles-are-equivs Ο† (ψ , ΟˆΟ† , Ο†Οˆ)
 where
  g = inverse f i
  Ξ· = inverses-are-retractions f i
  Ξ΅ = inverses-are-sections f i

  Ο„ : (x : X) β†’ ap f (Ξ· x) = Ξ΅ (f x)
  Ο„ = half-adjoint-condition f i

  Ο† : Ξ  A β†’ Ξ  (A ∘ f)
  Ο† = dprecomp A f

  ψ : Ξ  (A ∘ f) β†’ Ξ  A
  ψ k y = transport A (Ρ y) (k (g y))

  Ο†Οˆβ‚€ : (k : Ξ  (A ∘ f)) (x : X) β†’ transport A (Ξ΅ (f x)) (k (g (f x))) = k x
  Ο†Οˆβ‚€ k x = transport A (Ξ΅ (f x))   (k (g (f x))) =⟨ a ⟩
            transport A (ap f (η x))(k (g (f x))) =⟨ b ⟩
            transport (A ∘ f) (η x) (k (g (f x))) =⟨ c ⟩
            k x                                   ∎
    where
     a = ap (Ξ» - β†’ transport A - (k (g (f x)))) ((Ο„ x)⁻¹)
     b = (transport-ap A f (η x) (k (g (f x))))⁻¹
     c = apd k (Ξ· x)

  Ο†Οˆ : Ο† ∘ ψ ∼ id
  Ο†Οˆ k = fe (Ο†Οˆβ‚€ k)

  ΟˆΟ†β‚€ : (h : Ξ  A) (y : Y) β†’ transport A (Ξ΅ y) (h (f (g y))) = h y
  ΟˆΟ†β‚€ h y = apd h (Ξ΅ y)

  ΟˆΟ† : ψ ∘ Ο† ∼ id
  ΟˆΟ† h = fe' (ΟˆΟ†β‚€ h)

Ξ -change-of-variable : dfunext 𝓀 𝓦
                     β†’ dfunext π“₯ 𝓦
                     β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ ) (f : X β†’ Y)
                     β†’ is-equiv f
                     β†’ (Ξ  y κž‰ Y , A y) ≃ (Ξ  x κž‰ X , A (f x))

Ξ -change-of-variable fe fe' A f i = dprecomp A f , dprecomp-is-equiv fe fe' A f i

at-most-one-section : dfunext π“₯ 𝓀 β†’ hfunext π“₯ π“₯
                    β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                    β†’ has-retraction f
                    β†’ is-subsingleton (has-section f)

at-most-one-section {π“₯} {𝓀} fe hfe {X} {Y} f (g , gf) (h , fh) = d
 where
  fe' : dfunext π“₯ π“₯
  fe' = hfunext-gives-dfunext hfe

  a : invertible f
  a = joyal-equivs-are-invertible f ((h , fh) , (g , gf))

  b : is-singleton (fiber (Ξ» h β†’  f ∘ h) id)
  b = invertibles-are-equivs (Ξ» h β†’ f ∘ h) (postcomp-invertible fe fe' f a) id

  r : fiber (Ξ» h β†’  f ∘ h) id β†’ has-section f
  r (h , p) = (h , happly (f ∘ h) id p)

  s : has-section f β†’ fiber (Ξ» h β†’ f ∘ h) id
  s (h , Ξ·) = (h , fe' Ξ·)

  rs : (Οƒ : has-section f) β†’ r (s Οƒ) = Οƒ
  rs (h , η) = to-Σ-=' q
   where
    q : happly (f ∘ h) id (inverse (happly (f ∘ h) id) (hfe (f ∘ h) id) η) = η
    q = inverses-are-sections (happly (f ∘ h) id) (hfe (f ∘ h) id) η

  c : is-singleton (has-section f)
  c = retract-of-singleton (r , s , rs) b

  d : (Οƒ : has-section f) β†’ h , fh = Οƒ
  d = singletons-are-subsingletons (has-section f) c (h , fh)

at-most-one-retraction : hfunext 𝓀 𝓀 β†’ dfunext π“₯ 𝓀
                       β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                       β†’ has-section f
                       β†’ is-subsingleton (has-retraction f)

at-most-one-retraction {𝓀} {π“₯} hfe fe' {X} {Y} f (g , fg) (h , hf) = d
 where
  fe : dfunext 𝓀 𝓀
  fe = hfunext-gives-dfunext hfe

  a : invertible f
  a = joyal-equivs-are-invertible f ((g , fg) , (h , hf))

  b : is-singleton (fiber (Ξ» h β†’  h ∘ f) id)
  b = invertibles-are-equivs (Ξ» h β†’ h ∘ f) (precomp-invertible fe' fe f a) id

  r : fiber (Ξ» h β†’  h ∘ f) id β†’ has-retraction f
  r (h , p) = (h , happly (h ∘ f) id p)

  s : has-retraction f β†’ fiber (Ξ» h β†’  h ∘ f) id
  s (h , Ξ·) = (h , fe Ξ·)

  rs : (Οƒ : has-retraction f) β†’ r (s Οƒ) = Οƒ
  rs (h , η) = to-Σ-=' q
   where
    q : happly (h ∘ f) id (inverse (happly (h ∘ f) id) (hfe (h ∘ f) id) η) = η
    q = inverses-are-sections (happly (h ∘ f) id) (hfe (h ∘ f) id) η

  c : is-singleton (has-retraction f)
  c = retract-of-singleton (r , s , rs) b

  d : (ρ : has-retraction f) β†’ h , hf = ρ
  d = singletons-are-subsingletons (has-retraction f) c (h , hf)

being-joyal-equiv-is-subsingleton : hfunext 𝓀 𝓀 β†’ hfunext π“₯ π“₯ β†’ dfunext π“₯ 𝓀
                                  β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                  β†’ (f : X β†’ Y)
                                  β†’ is-subsingleton (is-joyal-equiv f)

being-joyal-equiv-is-subsingleton feβ‚€ fe₁ feβ‚‚ f = Γ—-is-subsingleton'
                                                   (at-most-one-section    feβ‚‚ fe₁ f ,
                                                    at-most-one-retraction feβ‚€ feβ‚‚ f)

being-hae-is-subsingleton : dfunext π“₯ 𝓀 β†’ hfunext π“₯ π“₯ β†’ dfunext 𝓀 (π“₯ βŠ” 𝓀)
                          β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                          β†’ is-subsingleton (is-hae f)

being-hae-is-subsingleton feβ‚€ fe₁ feβ‚‚ {X} {Y} f = subsingleton-criterion' Ξ³
 where
  a = Ξ» g Ξ΅ x
    β†’ ((g (f x) , Ξ΅ (f x)) = (x , refl (f x)))                                   β‰ƒβŸ¨ i  g Ξ΅ x ⟩
      (Ξ£ p κž‰ g (f x) = x , transport (Ξ» - β†’ f - = f x) p (Ξ΅ (f x)) = refl (f x)) β‰ƒβŸ¨ ii g Ξ΅ x ⟩
      (Ξ£ p κž‰ g (f x) = x , ap f p = Ξ΅ (f x))                                     β– 
   where
    i  = Ξ» g Ξ΅ x β†’ Ξ£-=-≃ (g (f x) , Ξ΅ (f x)) (x , refl (f x))
    ii = Ξ» g Ξ΅ x β†’ Ξ£-cong (Ξ» p β†’ transport-ap-≃ f p (Ξ΅ (f x)))

  b = (Ξ£ (g , Ξ΅) κž‰ has-section f , βˆ€ x β†’ (g (f x) , Ξ΅ (f x)) = (x , refl (f x)))         β‰ƒβŸ¨ i ⟩
      (Ξ£ (g , Ξ΅) κž‰ has-section f , βˆ€ x β†’ Ξ£  p κž‰ g (f x) = x , ap f p = Ξ΅ (f x))          β‰ƒβŸ¨ ii ⟩
      (Ξ£ g κž‰ (Y β†’ X) , Ξ£ Ξ΅ κž‰ f ∘ g ∼ id , βˆ€ x β†’ Ξ£  p κž‰ g (f x) = x , ap f p = Ξ΅ (f x))   β‰ƒβŸ¨ iii ⟩
      (Ξ£ g κž‰ (Y β†’ X) , Ξ£ Ξ΅ κž‰ f ∘ g ∼ id , Ξ£ Ξ· κž‰ g ∘ f ∼ id , βˆ€ x β†’ ap f (Ξ· x) = Ξ΅ (f x)) β‰ƒβŸ¨ iv ⟩
      is-hae f                                                                           β– 
   where
    i   = Ξ£-cong (Ξ» (g , Ξ΅) β†’ Ξ -cong feβ‚‚ feβ‚‚ (a g Ξ΅))
    ii  = Ξ£-assoc
    iii = Ξ£-cong (Ξ» g β†’ Ξ£-cong (Ξ» Ξ΅ β†’ Ξ Ξ£-distr-≃))
    iv  = Ξ£-cong (Ξ» g β†’ Ξ£-flip)

  Ξ³ : is-hae f β†’ is-subsingleton (is-hae f)
  Ξ³ (gβ‚€ , Ξ΅β‚€ , Ξ·β‚€ , Ο„β‚€) = i
   where
    c : (x : X) β†’ is-set (fiber f (f x))
    c x = singletons-are-sets (fiber f (f x)) (haes-are-equivs f (gβ‚€ , Ξ΅β‚€ , Ξ·β‚€ , Ο„β‚€) (f x))

    d : ((g , Ξ΅) : has-section f) β†’ is-subsingleton (βˆ€ x β†’ (g (f x) , Ξ΅ (f x)) = (x , refl (f x)))
    d (g , Ξ΅) = Ξ -is-subsingleton feβ‚‚ (Ξ» x β†’ c x (g (f x) , Ξ΅ (f x)) (x , refl (f x)))

    e : is-subsingleton (Ξ£ (g , Ξ΅) κž‰ has-section f , βˆ€ x β†’ (g (f x) , Ξ΅ (f x)) = (x , refl (f x)))
    e = Ξ£-is-subsingleton (at-most-one-section feβ‚€ fe₁ f (gβ‚€ , Ξ΅β‚€)) d

    i : is-subsingleton (is-hae f)
    i = equiv-to-subsingleton (≃-sym b) e

emptiness-is-subsingleton : dfunext 𝓀 𝓀₀ β†’ (X : 𝓀 Μ‡ )
                          β†’ is-subsingleton (is-empty X)

emptiness-is-subsingleton fe X f g = fe (Ξ» x β†’ !𝟘 (f x = g x) (f x))

+-is-subsingleton : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ }
                  β†’ is-subsingleton P
                  β†’ is-subsingleton Q
                  β†’ (P β†’ Q β†’ 𝟘) β†’ is-subsingleton (P + Q)

+-is-subsingleton {𝓀} {π“₯} {P} {Q} i j f = Ξ³
 where
  Ξ³ : (x y : P + Q) β†’ x = y
  Ξ³ (inl p) (inl p') = ap inl (i p p')
  γ (inl p) (inr q)  = !𝟘 (inl p = inr q) (f p q)
  γ (inr q) (inl p)  = !𝟘 (inr q = inl p) (f p q)
  Ξ³ (inr q) (inr q') = ap inr (j q q')

+-is-subsingleton' : dfunext 𝓀 𝓀₀
                   β†’ {P : 𝓀 Μ‡ } β†’ is-subsingleton P β†’ is-subsingleton (P + Β¬ P)

+-is-subsingleton' fe {P} i = +-is-subsingleton i
                               (emptiness-is-subsingleton fe P)
                               (Ξ» p n β†’ n p)

EM-is-subsingleton : dfunext (𝓀 ⁺) 𝓀 β†’ dfunext 𝓀 𝓀 β†’ dfunext 𝓀 𝓀₀
                   β†’ is-subsingleton (EM 𝓀)

EM-is-subsingleton fe⁺ fe feβ‚€ = Ξ -is-subsingleton fe⁺
                                 (Ξ» P β†’ Ξ -is-subsingleton fe
                                         (Ξ» i β†’ +-is-subsingleton' feβ‚€ i))
\end{code}