Agda UALib ↑

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository


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

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))

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))