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-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 -∃!

```