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.Solved-Exercises where

open import MGS.Equivalences public

subsingleton-criterion : {X : 𝓀 Μ‡ }
                       β†’ (X β†’ is-singleton X)
                       β†’ is-subsingleton X

subsingleton-criterion' : {X : 𝓀 Μ‡ }
                        β†’ (X β†’ is-subsingleton X)
                        β†’ is-subsingleton X

retract-of-subsingleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                        β†’ Y ◁ X β†’ is-subsingleton X β†’ is-subsingleton Y

left-cancellable : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
left-cancellable f = {x x' : domain f} β†’ f x ＝ f x' β†’ x ＝ x'

lc-maps-reflect-subsingletons : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                              β†’ left-cancellable f
                              β†’ is-subsingleton Y
                              β†’ is-subsingleton X

has-retraction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
has-retraction s = Ξ£ r κž‰ (codomain s β†’ domain s), r ∘ s ∼ id

sections-are-lc : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (s : X β†’ A)
                β†’ has-retraction s β†’ left-cancellable s

equivs-have-retractions : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                        β†’ is-equiv f β†’ has-retraction f

equivs-have-sections : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                     β†’ is-equiv f β†’ has-section f

equivs-are-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
              β†’ is-equiv f β†’ left-cancellable f

equiv-to-subsingleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ X ≃ Y
                      β†’ is-subsingleton Y
                      β†’ is-subsingleton X

comp-inverses : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                (f : X β†’ Y) (g : Y β†’ Z)
                (i : is-equiv f) (j : is-equiv g)
                (f' : Y β†’ X) (g' : Z β†’ Y)
              β†’ f' ∼ inverse f i
              β†’ g' ∼ inverse g j
              β†’ f' ∘ g' ∼ inverse (g ∘ f) (∘-is-equiv j i)

equiv-to-set : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
             β†’ X ≃ Y
             β†’ is-set Y
             β†’ is-set X

sections-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
                        β†’ has-retraction f
                        β†’ g ∼ f
                        β†’ has-retraction g

retractions-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
                           β†’ has-section f
                           β†’ g ∼ f
                           β†’ has-section g

is-joyal-equiv : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-joyal-equiv f = has-section f Γ— has-retraction f

one-inverse : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
              (f : X β†’ Y) (r s : Y β†’ X)
            β†’ (r ∘ f ∼ id)
            β†’ (f ∘ s ∼ id)
            β†’ r ∼ s

joyal-equivs-are-invertible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                            β†’ is-joyal-equiv f β†’ invertible f

joyal-equivs-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                        β†’ is-joyal-equiv f β†’ is-equiv f

invertibles-are-joyal-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                             β†’ invertible f β†’ is-joyal-equiv f

equivs-are-joyal-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                        β†’ is-equiv f β†’ is-joyal-equiv f

equivs-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f g : X β†’ Y}
                      β†’ is-equiv f
                      β†’ g ∼ f
                      β†’ is-equiv g

equiv-to-singleton' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    β†’ X ≃ Y β†’ is-singleton X β†’ is-singleton Y

subtypes-of-sets-are-sets' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (m : X β†’ Y)
                          β†’ left-cancellable m β†’ is-set Y β†’ is-set X

pr₁-lc : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
       β†’ ((x : X) β†’ is-subsingleton (A x))
       β†’ left-cancellable (Ξ» (t : Ξ£ A) β†’ pr₁ t)

subsets-of-sets-are-sets : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
                         β†’ is-set X
                         β†’ ((x : X) β†’ is-subsingleton (A x))
                         β†’ is-set (Ξ£ x κž‰ X , A x)

to-subtype-＝ : {X : 𝓦 Μ‡ } {A : X β†’ π“₯ Μ‡ }
               {x y : X} {a : A x} {b : A y}
             β†’ ((x : X) β†’ is-subsingleton (A x))
             β†’ x ＝ y
             β†’ (x , a) ＝ (y , b)

pr₁-equiv : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
          β†’ ((x : X) β†’ is-singleton (A x))
          β†’ is-equiv (Ξ» (t : Ξ£ A) β†’ pr₁ t)

pr₁-≃ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
      β†’ ((x : X) β†’ is-singleton (A x))
      β†’ Ξ£ A ≃ X

pr₁-≃ i = pr₁ , pr₁-equiv i

Ξ Ξ£-distr-≃ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
           β†’ (Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a)
           ≃ (Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x))

Ξ£-assoc : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Z : Ξ£ Y β†’ 𝓦 Μ‡ }
        β†’ Ξ£ Z ≃ (Ξ£ x κž‰ X , Ξ£ y κž‰ Y x , Z (x , y))

⁻¹-≃ : {X : 𝓀 Μ‡ } (x y : X) β†’ (x ＝ y) ≃ (y ＝ x)

singleton-types-≃ : {X : 𝓀 Μ‡ } (x : X) β†’ singleton-type' x ≃ singleton-type x

singletons-≃ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
             β†’ is-singleton X β†’ is-singleton Y β†’ X ≃ Y

maps-of-singletons-are-equivs : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                              β†’ is-singleton X β†’ is-singleton Y β†’ is-equiv f

logically-equivalent-subsingletons-are-equivalent : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
                                                  β†’ is-subsingleton X
                                                  β†’ is-subsingleton Y
                                                  β†’ X ↔ Y
                                                  β†’ X ≃ Y

singletons-are-equivalent : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
                          β†’ is-singleton X
                          β†’ is-singleton Y
                          β†’ X ≃ Y

NatΞ£-fiber-equiv : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (Ο† : Nat A B)
                   (x : X) (b : B x)
                 β†’ fiber (Ο† x) b ≃ fiber (NatΞ£ Ο†) (x , b)

NatΞ£-equiv-gives-fiberwise-equiv : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
                                   (Ο† : Nat A B)
                                 β†’ is-equiv (NatΞ£ Ο†)
                                 β†’ ((x : X) β†’ is-equiv (Ο† x))

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

Γ—-is-singleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ is-singleton X
                  β†’ is-singleton Y
                  β†’ is-singleton (X Γ— Y)

Γ—-is-subsingleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ is-subsingleton X
                  β†’ is-subsingleton Y
                  β†’ is-subsingleton (X Γ— Y)

Γ—-is-subsingleton' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                   β†’ ((Y β†’ is-subsingleton X) Γ— (X β†’ is-subsingleton Y))
                   β†’ is-subsingleton (X Γ— Y)

Γ—-is-subsingleton'-back : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                        β†’ is-subsingleton (X Γ— Y)
                        β†’ (Y β†’ is-subsingleton X) Γ— (X β†’ is-subsingleton Y)

apβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y β†’ Z) {x x' : X} {y y' : Y}
    β†’ x ＝ x' β†’ y ＝ y' β†’ f x y ＝ f x' y'

subsingleton-criterion = sol
 where
  sol : {X : 𝓀 Μ‡ } β†’ (X β†’ is-singleton X) β†’ is-subsingleton X
  sol f x = singletons-are-subsingletons (domain f) (f x) x

subsingleton-criterion' = sol
 where
  sol : {X : 𝓀 Μ‡ } β†’ (X β†’ is-subsingleton X) β†’ is-subsingleton X
  sol f x y = f x x y

retract-of-subsingleton = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ Y ◁ X β†’ is-subsingleton X β†’ is-subsingleton Y
  sol (r , s , Ξ·) i =  subsingleton-criterion
                        (Ξ» x β†’ retract-of-singleton (r , s , Ξ·)
                                (pointed-subsingletons-are-singletons
                                  (codomain s) (s x) i))

lc-maps-reflect-subsingletons = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ left-cancellable f β†’ is-subsingleton Y β†’ is-subsingleton X
  sol f l s x x' = l (s (f x) (f x'))

sections-are-lc = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (s : X β†’ A)
      β†’ has-retraction s β†’ left-cancellable s
  sol s (r , Ρ) {x} {y} p = x       ＝⟨ (Ρ x)⁻¹ ⟩
                            r (s x) ＝⟨ ap r p ⟩
                            r (s y) ＝⟨ Ρ y ⟩
                            y       ∎

equivs-have-retractions = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ has-retraction f
  sol f e = (inverse f e , inverses-are-retractions f e)

equivs-have-sections = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ has-section f
  sol f e = (inverse f e , inverses-are-sections f e)

equivs-are-lc = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f β†’ left-cancellable f
  sol f e = sections-are-lc f (equivs-have-retractions f e)

equiv-to-subsingleton = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ is-subsingleton Y β†’ is-subsingleton X
  sol (f , i) = lc-maps-reflect-subsingletons f (equivs-are-lc f i)

comp-inverses = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
        (f : X β†’ Y) (g : Y β†’ Z)
        (i : is-equiv f) (j : is-equiv g)
        (f' : Y β†’ X) (g' : Z β†’ Y)
      β†’ f' ∼ inverse f i
      β†’ g' ∼ inverse g j
      β†’ f' ∘ g' ∼ inverse (g ∘ f) (∘-is-equiv j i)
  sol f g i j f' g' h k z =
   f' (g' z)                          ＝⟨ h (g' z) ⟩
   inverse f i (g' z)                 ＝⟨ ap (inverse f i) (k z) ⟩
   inverse f i (inverse g j z)        ＝⟨ inverse-of-∘ f g i j z ⟩
   inverse (g ∘ f) (∘-is-equiv j i) z ∎

equiv-to-set = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ≃ Y β†’ is-set Y β†’ is-set X
  sol e = subtypes-of-sets-are-sets' ⌜ e ⌝ (equivs-are-lc ⌜ e ⌝ (⌜⌝-is-equiv e))

sections-closed-under-∼ = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
      β†’ has-retraction f β†’ g ∼ f β†’ has-retraction g
  sol f g (r , rf) h = (r ,
                        Ξ» x β†’ r (g x) ＝⟨ ap r (h x) ⟩
                              r (f x) ＝⟨ rf x ⟩
                              x       ∎)

retractions-closed-under-∼ = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
      β†’ has-section f β†’ g ∼ f β†’ has-section g
  sol f g (s , fs) h = (s ,
                        Ξ» y β†’ g (s y) ＝⟨ h (s y) ⟩
                              f (s y) ＝⟨ fs y ⟩
                              y ∎)

one-inverse = sol
 where
  sol : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
        (f : X β†’ Y) (r s : Y β†’ X)
      β†’ (r ∘ f ∼ id)
      β†’ (f ∘ s ∼ id)
      β†’ r ∼ s
  sol X Y f r s h k y = r y         ＝⟨ ap r ((k y)⁻¹) ⟩
                        r (f (s y)) ＝⟨ h (s y) ⟩
                        s y         ∎

joyal-equivs-are-invertible = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ is-joyal-equiv f β†’ invertible f
  sol f ((s , Ξ΅) , (r , Ξ·)) = (s , sf , Ξ΅)
   where
    sf = Ξ» (x : domain f) β†’ s (f x)       ＝⟨ (Ξ· (s (f x)))⁻¹ ⟩
                            r (f (s (f x))) ＝⟨ ap r (Ρ (f x)) ⟩
                            r (f x)       ＝⟨ η x ⟩
                            x            ∎

joyal-equivs-are-equivs = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ is-joyal-equiv f β†’ is-equiv f
  sol f j = invertibles-are-equivs f (joyal-equivs-are-invertible f j)

invertibles-are-joyal-equivs = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ invertible f β†’ is-joyal-equiv f
  sol f (g , Ξ· , Ξ΅) = ((g , Ξ΅) , (g , Ξ·))

equivs-are-joyal-equivs = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ is-equiv f β†’ is-joyal-equiv f
  sol f e = invertibles-are-joyal-equivs f (equivs-are-invertible f e)

equivs-closed-under-∼ = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f g : X β†’ Y}
      β†’ is-equiv f β†’ g ∼ f β†’ is-equiv g
  sol {𝓀} {π“₯} {X} {Y} {f} {g} e h = joyal-equivs-are-equivs g
                                      (retractions-closed-under-∼ f g
                                       (equivs-have-sections f e) h ,
                                      sections-closed-under-∼ f g
                                       (equivs-have-retractions f e) h)

equiv-to-singleton' = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ X ≃ Y β†’ is-singleton X β†’ is-singleton Y
  sol e = retract-of-singleton (≃-gives-β–· e)

subtypes-of-sets-are-sets' = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (m : X β†’ Y)
      β†’ left-cancellable m β†’ is-set Y β†’ is-set X
  sol {𝓀} {π“₯} {X} m i h = types-with-wconstant-＝-endomaps-are-sets X c
   where
    f : (x x' : X) β†’ x ＝ x' β†’ x ＝ x'
    f x x' r = i (ap m r)

    ΞΊ : (x x' : X) (r s : x ＝ x') β†’ f x x' r ＝ f x x' s
    ΞΊ x x' r s = ap i (h (m x) (m x') (ap m r) (ap m s))

    c : wconstant-＝-endomaps X
    c x x' = f x x' , ΞΊ x x'

pr₁-lc = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
      β†’ ((x : X) β†’ is-subsingleton (A x))
      β†’ left-cancellable  (Ξ» (t : Ξ£ A) β†’ pr₁ t)
  sol i p = to-Σ-＝ (p , i _ _ _)

subsets-of-sets-are-sets = sol
 where
  sol : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
     β†’ is-set X
     β†’ ((x : X) β†’ is-subsingleton (A x))
     β†’ is-set (Ξ£ x κž‰ X , A x)
  sol X A h p = subtypes-of-sets-are-sets' pr₁ (pr₁-lc p) h

to-subtype-＝ = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
        {x y : X} {a : A x} {b : A y}
      β†’ ((x : X) β†’ is-subsingleton (A x))
      β†’ x ＝ y
      β†’ (x , a) ＝ (y , b)
  sol {𝓀} {π“₯} {X} {A} {x} {y} {a} {b} s p = to-Ξ£-＝ (p , s y (transport A p a) b)

pr₁-equiv = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
      β†’ ((x : X) β†’ is-singleton (A x))
      β†’ is-equiv (Ξ» (t : Ξ£ A) β†’ pr₁ t)
  sol {𝓀} {π“₯} {X} {A} s = invertibles-are-equivs pr₁ (g , Ξ· , Ξ΅)
   where
    g : X β†’ Ξ£ A
    g x = x , pr₁ (s x)

    Ξ΅ : (x : X) β†’ pr₁ (g x) ＝ x
    Ξ΅ x = refl (pr₁ (g x))

    Ξ· : (Οƒ : Ξ£ A) β†’ g (pr₁ Οƒ) ＝ Οƒ
    Ξ· (x , a) = to-subtype-＝ (Ξ» x β†’ singletons-are-subsingletons (A x) (s x)) (Ξ΅ x)

Ξ Ξ£-distr-≃ = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
      β†’ (Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a)
      ≃ (Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x))
  sol {𝓀} {π“₯} {𝓦} {X} {A} {P} = invertibility-gives-≃ Ο† (Ξ³ , Ξ· , Ξ΅)
   where
    Ο† : (Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a)
      β†’ Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x)
    Ο† g = ((Ξ» x β†’ pr₁ (g x)) , Ξ» x β†’ prβ‚‚ (g x))

    Ξ³ : (Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x))
      β†’ Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a
    Ξ³ (f , Ο†) x = f x , Ο† x

    Ξ· : Ξ³ ∘ Ο† ∼ id
    Ξ· = refl

    Ξ΅ : Ο† ∘ Ξ³ ∼ id
    Ξ΅ = refl

Ξ£-assoc = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Z : Ξ£ Y β†’ 𝓦 Μ‡ }
      β†’ Ξ£ Z ≃ (Ξ£ x κž‰ X , Ξ£ y κž‰ Y x , Z (x , y))
  sol {𝓀} {π“₯} {𝓦} {X} {Y} {Z} = invertibility-gives-≃ f (g , refl , refl)
   where
    f : Ξ£ Z β†’ Ξ£ x κž‰ X , Ξ£ y κž‰ Y x , Z (x , y)
    f ((x , y) , z) = (x , (y , z))

    g : (Ξ£ x κž‰ X , Ξ£ y κž‰ Y x , Z (x , y)) β†’ Ξ£ Z
    g (x , (y , z)) = ((x , y) , z)

⁻¹-is-equiv : {X : 𝓀 Μ‡ } (x y : X)
            β†’ is-equiv (Ξ» (p : x ＝ y) β†’ p ⁻¹)
⁻¹-is-equiv x y = invertibles-are-equivs _⁻¹
                   (_⁻¹ , ⁻¹-involutive , ⁻¹-involutive)

⁻¹-≃ = sol
 where
  sol : {X : 𝓀 Μ‡ } (x y : X) β†’ (x ＝ y) ≃ (y ＝ x)
  sol x y = (_⁻¹ , ⁻¹-is-equiv x y)

singleton-types-≃ = sol
 where
  sol : {X : 𝓀 Μ‡ } (x : X) β†’ singleton-type' x ≃ singleton-type x
  sol x = Ξ£-cong (Ξ» y β†’ ⁻¹-≃ x y)

singletons-≃ = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-singleton X β†’ is-singleton Y β†’ X ≃ Y
  sol {𝓀} {π“₯} {X} {Y} i j = invertibility-gives-≃ f (g , Ξ· , Ξ΅)
   where
    f : X β†’ Y
    f x = center Y j

    g : Y β†’ X
    g y = center X i

    Ξ· : (x : X) β†’ g (f x) ＝ x
    Ξ· = centrality X i

    Ξ΅ : (y : Y) β†’ f (g y) ＝ y
    Ξ΅ = centrality Y j

maps-of-singletons-are-equivs = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
      β†’ is-singleton X β†’ is-singleton Y β†’ is-equiv f

  sol {𝓀} {π“₯} {X} {Y} f i j = invertibles-are-equivs f (g , Ξ· , Ξ΅)
   where
    g : Y β†’ X
    g y = center X i

    Ξ· : (x : X) β†’ g (f x) ＝ x
    Ξ· = centrality X i

    Ξ΅ : (y : Y) β†’ f (g y) ＝ y
    Ξ΅ y = singletons-are-subsingletons Y j (f (g y)) y

logically-equivalent-subsingletons-are-equivalent = sol
 where
  sol : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
      β†’ is-subsingleton X β†’ is-subsingleton Y β†’ X ↔ Y β†’ X ≃ Y
  sol  X Y i j (f , g) = invertibility-gives-≃ f
                          (g ,
                           (Ξ» x β†’ i (g (f x)) x) ,
                           (Ξ» y β†’ j (f (g y)) y))

singletons-are-equivalent = sol
 where
  sol : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
      β†’ is-singleton X β†’ is-singleton Y β†’ X ≃ Y
  sol  X Y i j = invertibility-gives-≃ (Ξ» _ β†’ center Y j)
                  ((Ξ» _ β†’ center X i) ,
                   centrality X i ,
                   centrality Y j)

NatΞ£-fiber-equiv = sol
 where
  sol : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (Ο† : Nat A B)
        (x : X) (b : B x)
      β†’ fiber (Ο† x) b ≃ fiber (NatΞ£ Ο†) (x , b)
  sol A B Ο† x b = invertibility-gives-≃ f (g , Ξ΅ , Ξ·)
   where
    f : fiber (Ο† x) b β†’ fiber (NatΞ£ Ο†) (x , b)
    f (a , refl _) = ((x , a) , refl (x , Ο† x a))

    g : fiber (NatΞ£ Ο†) (x , b) β†’ fiber (Ο† x) b
    g ((x , a) , refl _) = (a , refl (Ο† x a))

    Ξ΅ : (w : fiber (Ο† x) b) β†’ g (f w) ＝ w
    Ξ΅ (a , refl _) = refl (a , refl (Ο† x a))

    Ξ· : (t : fiber (NatΞ£ Ο†) (x , b)) β†’ f (g t) ＝ t
    Ξ· ((x , a) , refl _) = refl ((x , a) , refl (NatΞ£ Ο† (x , a)))

NatΞ£-equiv-gives-fiberwise-equiv = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } (Ο† : Nat A B)
      β†’ is-equiv (NatΞ£ Ο†) β†’ ((x : X) β†’ is-equiv (Ο† x))
  sol {𝓀} {π“₯} {𝓦} {X} {A} {B} Ο† e x b = Ξ³
   where
    d : fiber (Ο† x) b ≃ fiber (NatΞ£ Ο†) (x , b)
    d = NatΞ£-fiber-equiv A B Ο† x b

    s : is-singleton (fiber (NatΞ£ Ο†) (x , b))
    s = e (x , b)

    Ξ³ : is-singleton (fiber (Ο† x) b)
    Ξ³ = equiv-to-singleton d s

Ξ£-is-subsingleton = sol
 where
  sol : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
      β†’ is-subsingleton X
      β†’ ((x : X) β†’ is-subsingleton (A x))
      β†’ is-subsingleton (Ξ£ A)
  sol i j (x , _) (y , _) = to-subtype-＝ j (i x y)

Γ—-is-singleton = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-singleton X
      β†’ is-singleton Y
      β†’ is-singleton (X Γ— Y)
  sol (x , Ο†) (y , Ξ³) = (x , y) , Ξ΄
   where
    Ξ΄ : βˆ€ z β†’ x , y ＝ z
    Ξ΄ (x' , y' ) = to-Γ—-＝ (Ο† x' , Ξ³ y')

Γ—-is-subsingleton = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-subsingleton X β†’ is-subsingleton Y β†’ is-subsingleton (X Γ— Y)
  sol i j = Ξ£-is-subsingleton i (Ξ» _ β†’ j)

Γ—-is-subsingleton' = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ ((Y β†’ is-subsingleton X) Γ— (X β†’ is-subsingleton Y))
      β†’ is-subsingleton (X Γ— Y)
  sol {𝓀} {π“₯} {X} {Y} (i , j) = k
   where
    k : is-subsingleton (X Γ— Y)
    k (x , y) (x' , y') = to-Γ—-＝ (i y x x' , j x y y')

Γ—-is-subsingleton'-back = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-subsingleton (X Γ— Y)
      β†’ (Y β†’ is-subsingleton X) Γ— (X β†’ is-subsingleton Y)
  sol {𝓀} {π“₯} {X} {Y} k = i , j
   where
    i : Y β†’ is-subsingleton X
    i y x x' = ap pr₁ (k (x , y) (x' , y))

    j : X β†’ is-subsingleton Y
    j x y y' = ap prβ‚‚ (k (x , y) (x , y'))

apβ‚‚ = sol
 where
  sol : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y β†’ Z) {x x' : X} {y y' : Y}
      β†’ x ＝ x' β†’ y ＝ y' β†’ f x y ＝ f x' y'
  sol f (refl x) (refl y) = refl (f x y)

\end{code}