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.Subsingleton-Theorems where

open import MGS.FunExt-from-Univalence public

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

Ξ -is-subsingleton fe i f g = fe (Ξ» x β†’ i x (f x) (g x))

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

being-singleton-is-subsingleton fe {X} (x , Ο†) (y , Ξ³) = p
 where
  i : is-subsingleton X
  i = singletons-are-subsingletons X (y , Ξ³)

  s : is-set X
  s = subsingletons-are-sets X i

  a : (z : X) β†’ is-subsingleton ((t : X) β†’ z ＝ t)
  a z = Ξ -is-subsingleton fe (s z)

  b : x ＝ y
  b = Ο† y

  p : (x , Ο†) ＝ (y , Ξ³)
  p = to-subtype-＝ a b

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

being-equiv-is-subsingleton fe fe' f = Ξ -is-subsingleton fe
                                        (Ξ» x β†’ being-singleton-is-subsingleton fe')

subsingletons-are-retracts-of-logically-equivalent-types : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                                         β†’ is-subsingleton X
                                                         β†’ (X ↔ Y)
                                                         β†’ X ◁ Y

subsingletons-are-retracts-of-logically-equivalent-types i (f , g) = g , f , Ξ·
 where
  η : g ∘ f ∼ id
  Ξ· x = i (g (f x)) x

equivalence-property-is-retract-of-invertibility-data : dfunext π“₯ (𝓀 βŠ” π“₯) β†’ dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
                                                      β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                                      β†’ is-equiv f ◁ invertible f

equivalence-property-is-retract-of-invertibility-data fe fe' f =
  subsingletons-are-retracts-of-logically-equivalent-types
   (being-equiv-is-subsingleton fe fe' f) (equivs-are-invertible f , invertibles-are-equivs f)

univalence-is-subsingleton : is-univalent (𝓀 ⁺)
                           β†’ is-subsingleton (is-univalent 𝓀)

univalence-is-subsingleton {𝓀} ua⁺ = subsingleton-criterion' Ξ³
 where
  Ξ³ : is-univalent 𝓀 β†’ is-subsingleton (is-univalent 𝓀)
  Ξ³ ua = i
   where
    dfe₁ : dfunext  𝓀    (𝓀 ⁺)
    dfeβ‚‚ : dfunext (𝓀 ⁺) (𝓀 ⁺)

    dfe₁ = univalence-gives-dfunext' ua ua⁺
    dfeβ‚‚ = univalence-gives-dfunext ua⁺

    i : is-subsingleton (is-univalent 𝓀)
    i = Ξ -is-subsingleton dfeβ‚‚
         (Ξ» X β†’ Ξ -is-subsingleton dfeβ‚‚
         (Ξ» Y β†’ being-equiv-is-subsingleton dfe₁ dfeβ‚‚ (Idβ†’Eq X Y)))

Univalence : 𝓀ω
Univalence = βˆ€ 𝓀 β†’ is-univalent 𝓀

univalence-is-subsingletonΟ‰ : Univalence β†’ is-subsingleton (is-univalent 𝓀)
univalence-is-subsingletonΟ‰ {𝓀} Ξ³ = univalence-is-subsingleton (Ξ³ (𝓀 ⁺))

univalence-is-a-singleton : Univalence β†’ is-singleton (is-univalent 𝓀)
univalence-is-a-singleton {𝓀} Ξ³ = pointed-subsingletons-are-singletons
                                   (is-univalent 𝓀)
                                   (Ξ³ 𝓀)
                                   (univalence-is-subsingletonω γ)

global-dfunext : 𝓀ω
global-dfunext = βˆ€ {𝓀 π“₯} β†’ dfunext 𝓀 π“₯

univalence-gives-global-dfunext : Univalence β†’ global-dfunext
univalence-gives-global-dfunext ua {𝓀} {π“₯} = univalence-gives-dfunext'
                                               (ua 𝓀) (ua (𝓀 βŠ” π“₯))

global-hfunext : 𝓀ω
global-hfunext = βˆ€ {𝓀 π“₯} β†’ hfunext 𝓀 π“₯

univalence-gives-global-hfunext : Univalence β†’ global-hfunext
univalence-gives-global-hfunext ua {𝓀} {π“₯} = univalence-gives-hfunext'
                                               (ua 𝓀) (ua (𝓀 βŠ” π“₯))

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

Ξ -is-subsingleton' fe {X} {A} i = Ξ³
 where
  ρ : ({x : X} β†’ A x) ◁ Ξ  A
  ρ = (Ξ» f {x} β†’ f x) , (Ξ» g x β†’ g {x}) , (Ξ» f β†’ refl (Ξ» {x} β†’ f))

  Ξ³ : is-subsingleton ({x : X} β†’ A x)
  γ = retract-of-subsingleton ρ (Π-is-subsingleton fe i)

vv-and-hfunext-are-subsingletons-lemma  : dfunext (𝓀 ⁺)       (𝓀 βŠ” (π“₯ ⁺))
                                        β†’ dfunext (𝓀 βŠ” (π“₯ ⁺)) (𝓀 βŠ” π“₯)
                                        β†’ dfunext (𝓀 βŠ” π“₯)     (𝓀 βŠ” π“₯)

                                        β†’ is-subsingleton (vvfunext 𝓀 π“₯)
                                        Γ— is-subsingleton (hfunext  𝓀 π“₯)

vv-and-hfunext-are-subsingletons-lemma {𝓀} {π“₯} dfe dfe' dfe'' = Ο† , Ξ³
 where
  Ο† : is-subsingleton (vvfunext 𝓀 π“₯)
  Ο† = Ξ -is-subsingleton' dfe
       (Ξ» X β†’ Ξ -is-subsingleton' dfe'
       (Ξ» A β†’ Ξ -is-subsingleton dfe''
       (Ξ» i β†’ being-singleton-is-subsingleton dfe'')))

  Ξ³ : is-subsingleton (hfunext 𝓀 π“₯)
  Ξ³ = Ξ -is-subsingleton' dfe
       (Ξ» X β†’ Ξ -is-subsingleton' dfe'
       (Ξ» A β†’ Ξ -is-subsingleton dfe''
       (Ξ» f β†’ Ξ -is-subsingleton dfe''
       (Ξ» g β†’ being-equiv-is-subsingleton dfe'' dfe''
               (happly f g)))))

vv-and-hfunext-are-singletons : Univalence
                              β†’ is-singleton (vvfunext 𝓀 π“₯)
                              Γ— is-singleton (hfunext  𝓀 π“₯)

vv-and-hfunext-are-singletons {𝓀} {π“₯} ua =

 f (vv-and-hfunext-are-subsingletons-lemma
     (univalence-gives-dfunext' (ua (𝓀 ⁺))       (ua ((𝓀 ⁺) βŠ” (π“₯ ⁺))))
     (univalence-gives-dfunext' (ua (𝓀 βŠ” (π“₯ ⁺))) (ua (𝓀 βŠ” (π“₯ ⁺))))
     (univalence-gives-dfunext' (ua (𝓀 βŠ” π“₯))     (ua (𝓀 βŠ” π“₯))))

 where
  f : is-subsingleton (vvfunext 𝓀 π“₯) Γ— is-subsingleton (hfunext 𝓀 π“₯)
    β†’ is-singleton (vvfunext 𝓀 π“₯) Γ— is-singleton (hfunext 𝓀 π“₯)

  f (i , j) = pointed-subsingletons-are-singletons (vvfunext 𝓀 π“₯)
                (univalence-gives-vvfunext' (ua 𝓀) (ua (𝓀 βŠ” π“₯))) i ,

              pointed-subsingletons-are-singletons (hfunext 𝓀 π“₯)
                (univalence-gives-hfunext' (ua 𝓀) (ua (𝓀 βŠ” π“₯))) j
\end{code}