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.Unique-Existence where

open import MGS.Subsingleton-Theorems public

βˆƒ! : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
βˆƒ! A = is-singleton (Ξ£ A)

-βˆƒ! : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
-βˆƒ! X Y = βˆƒ! Y

syntax -βˆƒ! A (Ξ» x β†’ b) = βˆƒ! x κž‰ A , b

βˆƒ!-is-subsingleton : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                   β†’ dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
                   β†’ is-subsingleton (βˆƒ! A)

βˆƒ!-is-subsingleton A fe = being-singleton-is-subsingleton fe

unique-existence-gives-weak-unique-existence : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )

  β†’ (βˆƒ! x κž‰ X , A x)
  β†’ (Ξ£ x κž‰ X , A x) Γ— ((x y : X) β†’ A x β†’ A y β†’ x ＝ y)

unique-existence-gives-weak-unique-existence A s = center (Ξ£ A) s , u
 where
  u : βˆ€ x y β†’ A x β†’ A y β†’ x ＝ y
  u x y a b = ap pr₁ (singletons-are-subsingletons (Ξ£ A) s (x , a) (y , b))

weak-unique-existence-gives-unique-existence-sometimes : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) β†’

    ((x : X) β†’ is-subsingleton (A x))

  β†’ ((Ξ£ x κž‰ X , A x) Γ— ((x y : X) β†’ A x β†’ A y β†’ x ＝ y))
  β†’ (βˆƒ! x κž‰ X , A x)

weak-unique-existence-gives-unique-existence-sometimes A i ((x , a) , u) = (x , a) , Ο†
 where
  Ο† : (Οƒ : Ξ£ A) β†’ x , a ＝ Οƒ
  Ο† (y , b) = to-subtype-＝ i (u x y a b)

β„•-is-nno : hfunext 𝓀₀ 𝓀
         β†’ (Y : 𝓀 Μ‡ ) (yβ‚€ : Y) (g : Y β†’ Y)
         β†’ βˆƒ! h κž‰ (β„• β†’ Y), (h 0 ＝ yβ‚€) Γ— (h ∘ succ ＝ g ∘ h)

β„•-is-nno {𝓀} hfe Y yβ‚€ g = Ξ³
 where

  fe : dfunext 𝓀₀ 𝓀
  fe = hfunext-gives-dfunext hfe

  lemmaβ‚€ : (h : β„• β†’ Y) β†’ ((h 0 ＝ yβ‚€) Γ— (h ∘ succ ∼ g ∘ h)) ◁ (h ∼ β„•-iteration Y yβ‚€ g)
  lemmaβ‚€ h = r , s , Ξ·
   where
    s : (h 0 ＝ yβ‚€) Γ— (h ∘ succ ∼ g ∘ h) β†’ h ∼ β„•-iteration Y yβ‚€ g
    s (p , K) 0 = p
    s (p , K) (succ n) = h (succ n)                  ＝⟨ K n ⟩
                         g (h n)                     ＝⟨ ap g (s (p , K) n) ⟩
                         g (β„•-iteration Y yβ‚€ g n)    ＝⟨ refl _ ⟩
                         β„•-iteration Y yβ‚€ g (succ n) ∎

    r : codomain s β†’ domain s
    r H = H 0 , (Ξ» n β†’ h (succ n)                  ＝⟨ H (succ n) ⟩
                       β„•-iteration Y yβ‚€ g (succ n) ＝⟨ refl _ ⟩
                       g (β„•-iteration Y yβ‚€ g n)    ＝⟨ ap g ((H n)⁻¹) ⟩
                       g (h n )                    ∎)

    remark : βˆ€ n H β†’ prβ‚‚ (r H) n ＝ H (succ n) βˆ™ (refl _ βˆ™ ap g ((H n)⁻¹))
    remark n H = refl _

    Ξ· : (z : (h 0 ＝ yβ‚€) Γ— (h ∘ succ ∼ g ∘ h)) β†’ r (s z) ＝ z
    Ξ· (p , K) = q
     where
      v = Ξ» n β†’
       s (p , K) (succ n) βˆ™ (refl _ βˆ™ ap g ((s (p , K) n)⁻¹))                  ＝⟨ refl _ ⟩
       K n βˆ™  ap g (s (p , K) n) βˆ™ (refl _ βˆ™ ap g ((s (p , K) n)⁻¹))           ＝⟨ i   n ⟩
       K n βˆ™  ap g (s (p , K) n) βˆ™  ap g ((s (p , K) n) ⁻¹)                    ＝⟨ ii  n ⟩
       K n βˆ™ (ap g (s (p , K) n) βˆ™  ap g ((s (p , K) n) ⁻¹))                   ＝⟨ iii n ⟩
       K n βˆ™ (ap g (s (p , K) n) βˆ™ (ap g  (s (p , K) n))⁻¹)                    ＝⟨ iv  n ⟩
       K n βˆ™ refl _                                                            ＝⟨ refl _ ⟩
       K n                                                                     ∎
        where
         i   = Ξ» n β†’ ap (K n βˆ™ ap g (s (p , K) n) βˆ™_)
                        (refl-left {_} {_} {_} {_} {ap g ((s (p , K) n)⁻¹)})
         ii  = Ξ» n β†’ βˆ™assoc (K n) (ap g (s (p , K) n)) (ap g ((s (p , K) n)⁻¹))
         iii = Ξ» n β†’ ap (Ξ» - β†’ K n βˆ™ (ap g (s (p , K) n) βˆ™ -)) (ap⁻¹ g (s (p , K) n) ⁻¹)
         iv  = Ξ» n β†’ ap (K n βˆ™_) (⁻¹-rightβˆ™ (ap g (s (p , K) n)))

      q = r (s (p , K))                                                      ＝⟨ refl _ ⟩
          p , (Ξ» n β†’ s (p , K) (succ n) βˆ™ (refl _ βˆ™ ap g ((s (p , K) n)⁻¹))) ＝⟨ vi ⟩
          p , K                                                              ∎
       where
         vi = ap (p ,_) (fe v)

  lemma₁ = Ξ» h β†’ (h 0 ＝ yβ‚€) Γ— (h ∘ succ ＝ g ∘ h) β—βŸ¨ i h ⟩
                 (h 0 ＝ yβ‚€) Γ— (h ∘ succ ∼ g ∘ h) β—βŸ¨ lemmaβ‚€ h ⟩
                 (h ∼ β„•-iteration Y yβ‚€ g)        β—βŸ¨ ii h ⟩
                 (h ＝ β„•-iteration Y yβ‚€ g)        β—€
   where
    i  = Ξ» h β†’ Ξ£-retract (Ξ» _ β†’ ≃-gives-◁ (happly (h ∘ succ) (g ∘ h) , hfe _ _))
    ii = Ξ» h β†’ ≃-gives-β–· (happly h (β„•-iteration Y yβ‚€ g) , hfe _ _)

  lemmaβ‚‚ : (Ξ£ h κž‰ (β„• β†’ Y), (h 0 ＝ yβ‚€) Γ— (h ∘ succ ＝ g ∘ h))
         ◁ (Ξ£ h κž‰ (β„• β†’ Y), h ＝ β„•-iteration Y yβ‚€ g)

  lemmaβ‚‚ = Ξ£-retract lemma₁

  Ξ³ : is-singleton (Ξ£ h κž‰ (β„• β†’ Y), (h 0 ＝ yβ‚€) Γ— (h ∘ succ ＝ g ∘ h))
  Ξ³ = retract-of-singleton lemmaβ‚‚
                           (singleton-types-are-singletons (β„• β†’ Y) (β„•-iteration Y yβ‚€ g))

module finite-types (hfe : hfunext 𝓀₀ 𝓀₁) where

 fin :  βˆƒ! Fin κž‰ (β„• β†’ 𝓀₀ Μ‡ )
               , (Fin 0 ＝ 𝟘)
               Γ— (Fin ∘ succ ＝ Ξ» n β†’ Fin n + πŸ™)

 fin = β„•-is-nno hfe (𝓀₀ Μ‡ ) 𝟘 (_+ πŸ™)

 Fin : β„• β†’ 𝓀₀ Μ‡
 Fin = pr₁ (center _ fin)

 Fin-equationβ‚€ : Fin 0 ＝ 𝟘
 Fin-equationβ‚€ = refl _

 Fin-equation-succ : Fin ∘ succ ＝ Ξ» n β†’ Fin n + πŸ™
 Fin-equation-succ = refl _

 Fin-equation-succ' : (n : β„•) β†’ Fin (succ n) ＝ Fin n + πŸ™
 Fin-equation-succ' n = refl _

 Fin-equation₁ : Fin 1 ＝ 𝟘 + πŸ™
 Fin-equation₁ = refl _

 Fin-equationβ‚‚ : Fin 2 ＝ (𝟘 + πŸ™) + πŸ™
 Fin-equationβ‚‚ = refl _

 Fin-equation₃ : Fin 3 ＝ ((𝟘 + πŸ™) + πŸ™) + πŸ™
 Fin-equation₃ = refl _

infixr -1 -βˆƒ!

\end{code}