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-Equivalence-Induction where

open import MGS-Univalence public
open import MGS-Solved-Exercises public

equiv-singleton-lemma : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X)
                        (f : (y : X) β†’ x ≑ y β†’ A y)
                      β†’ ((y : X) β†’ is-equiv (f y))
                      β†’ is-singleton (Ξ£ A)

equiv-singleton-lemma {𝓀} {π“₯} {X} {A} x f i = Ξ³
 where
  abstract
   e : (y : X) β†’ (x ≑ y) ≃ A y
   e y = (f y , i y)

   d : singleton-type' x ≃ Ξ£ A
   d = Ξ£-cong e

   Ξ³ : is-singleton (Ξ£ A)
   Ξ³ = equiv-to-singleton (≃-sym d) (singleton-types'-are-singletons X x)

singleton-equiv-lemma : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (x : X)
                        (f : (y : X) β†’ x ≑ y β†’ A y)
                      β†’ is-singleton (Ξ£ A)
                      β†’ (y : X) β†’ is-equiv (f y)

singleton-equiv-lemma {𝓀} {π“₯} {X} {A} x f i = Ξ³
 where
  abstract
   g : singleton-type' x β†’ Ξ£ A
   g = NatΞ£ f

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

   Ξ³ : (y : X) β†’ is-equiv (f y)
   Ξ³ = NatΞ£-equiv-gives-fiberwise-equiv f e

univalenceβ‡’ : is-univalent 𝓀
            β†’ (X : 𝓀 Μ‡ ) β†’ is-singleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)

univalence⇒ ua X = equiv-singleton-lemma X (Id→Eq X) (ua X)

β‡’univalence : ((X : 𝓀 Μ‡ ) β†’ is-singleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y))
            β†’ is-univalent 𝓀

⇒univalence i X = singleton-equiv-lemma X (Id→Eq X) (i X)

univalenceβ†’ : is-univalent 𝓀
            β†’ (X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)

univalence→ ua X = singletons-are-subsingletons
                    (Ξ£ (X ≃_)) (univalenceβ‡’ ua X)

β†’univalence : ((X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y))
            β†’ is-univalent 𝓀

β†’univalence i = β‡’univalence (Ξ» X β†’ pointed-subsingletons-are-singletons
                                    (Ξ£ (X ≃_)) (X , id-≃ X) (i X))

𝔾-≃ : is-univalent 𝓀
    β†’ (X : 𝓀 Μ‡ ) (A : (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y) β†’ π“₯ Μ‡ )
    β†’ A (X , id-≃ X) β†’ (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A (Y , e)

𝔾-≃ {𝓀} ua X A a Y e = transport A p a
 where
  t : Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y
  t = (X , id-≃ X)

  p : t ≑ (Y , e)
  p = univalenceβ†’ {𝓀} ua X t (Y , e)

𝔾-≃-equation : (ua : is-univalent 𝓀)
             β†’ (X : 𝓀 Μ‡ ) (A : (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y) β†’ π“₯ Μ‡ ) (a : A (X , id-≃ X))
             β†’ 𝔾-≃ ua X A a X (id-≃ X) ≑ a

𝔾-≃-equation {𝓀} {π“₯} ua X A a =

  𝔾-≃ ua X A a X (id-≃ X) β‰‘βŸ¨ refl _                       ⟩
  transport A p a         β‰‘βŸ¨ ap (Ξ» - β†’ transport A - a) q ⟩
  transport A (refl t) a  β‰‘βŸ¨ refl _                       ⟩
  a                       ∎

 where
  t : Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y
  t = (X , id-≃ X)

  p : t ≑ t
  p = univalenceβ†’ {𝓀} ua X t t

  q : p ≑ refl t
  q = subsingletons-are-sets (Ξ£ Y κž‰ 𝓀 Μ‡ , X ≃ Y)
       (univalenceβ†’ {𝓀} ua X) t t p (refl t)

ℍ-≃ : is-univalent 𝓀
    β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
    β†’ A X (id-≃ X) β†’ (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A Y e

ℍ-≃ ua X A = 𝔾-≃ ua X (Ξ£-induction A)

ℍ-≃-equation : (ua : is-univalent 𝓀)
             β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) (a : A X  (id-≃ X))
             β†’ ℍ-≃ ua X A a X (id-≃ X) ≑ a

ℍ-≃-equation ua X A = 𝔾-≃-equation ua X (Ξ£-induction A)

𝕁-≃ : is-univalent 𝓀
    β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
    β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X))
    β†’ (X Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A X Y e

𝕁-≃ ua A Ο† X = ℍ-≃ ua X (A X) (Ο† X)

𝕁-≃-equation : (ua : is-univalent 𝓀)
             β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
             β†’ (Ο† : (X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X))
             β†’ (X : 𝓀 Μ‡ ) β†’ 𝕁-≃ ua A Ο† X X (id-≃ X) ≑ Ο† X

𝕁-≃-equation ua A Ο† X = ℍ-≃-equation ua X (A X) (Ο† X)

ℍ-equiv : is-univalent 𝓀
        β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
        β†’ A X (𝑖𝑑 X) β†’ (Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A Y f

ℍ-equiv {𝓀} {π“₯} ua X A a Y f i = Ξ³ (f , i)
 where
  B : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡
  B Y (f , i) = A Y f

  b : B X (id-≃ X)
  b = a

  Ξ³ : (e : X ≃ Y) β†’ B Y e
  Ξ³ = ℍ-≃ ua X B b Y

𝕁-equiv : is-univalent 𝓀
        β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
        β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (𝑖𝑑 X))
        β†’ (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A X Y f

𝕁-equiv ua A Ο† X = ℍ-equiv ua X (A X) (Ο† X)

𝕁-invertible : is-univalent 𝓀
             β†’ (A : (X Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
             β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (𝑖𝑑 X))
             β†’ (X Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ invertible f β†’ A X Y f

𝕁-invertible ua A Ο† X Y f i = 𝕁-equiv ua A Ο† X Y f (invertibles-are-equivs f i)

automatic-equiv-functoriality :

      (F : 𝓀 Μ‡ β†’ 𝓀 Μ‡ )
      (𝓕 : {X Y : 𝓀 Μ‡ }  β†’ (X β†’ Y) β†’ F X β†’ F Y)
      (𝓕-id : {X : 𝓀 Μ‡ } β†’ 𝓕 (𝑖𝑑 X) ≑ 𝑖𝑑 (F X))
      {X Y Z : 𝓀 Μ‡ }
      (f : X β†’ Y)
      (g : Y β†’ Z)

    β†’ is-univalent 𝓀 β†’ is-equiv f + is-equiv g β†’ 𝓕 (g ∘ f) ≑ 𝓕 g ∘ 𝓕 f

automatic-equiv-functoriality {𝓀} F 𝓕 𝓕-id {X} {Y} {Z} f g ua = Ξ³
  where
   Ξ³ :  is-equiv f + is-equiv g β†’ 𝓕 (g ∘ f) ≑ 𝓕 g ∘ 𝓕 f
   Ξ³ (inl i) = ℍ-equiv ua X A a Y f i g
    where
     A : (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ 𝓀 Μ‡
     A Y f = (g : Y β†’ Z) β†’ 𝓕 (g ∘ f) ≑ 𝓕 g ∘ 𝓕 f

     a : (g : X β†’ Z) β†’ 𝓕 g ≑ 𝓕 g ∘ 𝓕 id
     a g = ap (𝓕 g ∘_) (𝓕-id ⁻¹)

   Ξ³ (inr j) = ℍ-equiv ua Y B b Z g j f
    where
     B : (Z : 𝓀 Μ‡ ) β†’ (Y β†’ Z) β†’ 𝓀 Μ‡
     B Z g = (f : X β†’ Y) β†’ 𝓕 (g ∘ f) ≑ 𝓕 g ∘ 𝓕 f

     b : (f : X β†’ Y) β†’ 𝓕 f ≑ 𝓕 (𝑖𝑑 Y) ∘ 𝓕 f
     b f = ap (_∘ 𝓕 f) (𝓕-id ⁻¹)

Ξ£-change-of-variable' : is-univalent 𝓀
                      β†’ {X : 𝓀 Μ‡ } {Y : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (f : X β†’ Y)
                      β†’ (i : is-equiv f)
                      β†’ (Ξ£ x κž‰ X , A x) ≑ (Ξ£ y κž‰ Y , A (inverse f i y))

Ξ£-change-of-variable' {𝓀} {π“₯} ua {X} {Y} A f i = ℍ-≃ ua X B b Y (f , i)
 where
   B : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’  (𝓀 βŠ” π“₯)⁺ Μ‡
   B Y (f , i) = Ξ£ A ≑ (Ξ£ (A ∘ inverse f i))

   b : B X (id-≃ X)
   b = refl (Ξ£ A)

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

Ξ£-change-of-variable'' ua A f i = Ξ£-change-of-variable' ua A
                                  (inverse f i)
                                  (inverses-are-equivs f i)

transport-map-along-≑ : {X Y Z : 𝓀 Μ‡ }
                        (p : X ≑ Y) (g : X β†’ Z)
                      β†’ transport (Ξ» - β†’ - β†’ Z) p g
                      ≑ g ∘ Idβ†’fun (p ⁻¹)

transport-map-along-≑ (refl X) = refl

transport-map-along-≃ : (ua : is-univalent 𝓀) {X Y Z : 𝓀 Μ‡ }
                        (e : X ≃ Y) (g : X β†’ Z)
                      → transport (λ - → - → Z) (Eq→Id ua X Y e) g
                      ≑ g ∘ ⌜ ≃-sym e ⌝

transport-map-along-≃ {𝓀} ua {X} {Y} {Z} = 𝕁-≃ ua A a X Y
 where
  A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ 𝓀 Μ‡
  A X Y e = (g : X → Z) → transport (λ - → - → Z) (Eq→Id ua X Y e) g
                        ≑ g ∘ ⌜ ≃-sym e ⌝
  a : (X : 𝓀 Μ‡ ) β†’ A X X (id-≃ X)
  a X g = transport (Ξ» - β†’ - β†’ Z) (Eqβ†’Id ua X X (id-≃ X)) g β‰‘βŸ¨ q      ⟩
          transport (Ξ» - β†’ - β†’ Z) (refl X) g                β‰‘βŸ¨ refl _ ⟩
          g                                                 ∎
    where
     p : Eqβ†’Id ua X X (id-≃ X) ≑ refl X
     p = inverses-are-retractions (Id→Eq X X) (ua X X) (refl X)

     q = ap (Ξ» - β†’ transport (Ξ» - β†’ - β†’ Z) - g) p