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  ≡ y₀) × (h ∘ succ ≡ g ∘ h)

ℕ-is-nno {𝓤} hfe Y y₀ g = γ
 where

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

  lemma₀ : (h : ℕ → Y) → ((h  ≡ y₀) × (h ∘ succ ∼ g ∘ h)) ◁ (h ∼ ℕ-iteration Y y₀ g)
  lemma₀ h = r , s , η
   where
    s : (h  ≡ y₀) × (h ∘ succ ∼ g ∘ h) → h ∼ ℕ-iteration Y y₀ g
    s (p , K)  = 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  , (λ 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  ≡ 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  ≡ y₀) × (h ∘ succ ≡ g ∘ h) ◁⟨ i h      ⟩
                 (h  ≡ 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  ≡ y₀) × (h ∘ succ ≡ g ∘ h))
         ◁ (Σ h ꞉ (ℕ → Y), h ≡ ℕ-iteration Y y₀ g)

  lemma₂ = Σ-retract lemma₁

  γ : is-singleton (Σ h ꞉ (ℕ → Y), (h  ≡ 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  ≡ 𝟘)
               × (Fin ∘ succ ≡ λ n → Fin n + 𝟙)

 fin = ℕ-is-nno hfe (𝓤₀ ̇ ) 𝟘 (_+ 𝟙)

 Fin : ℕ → 𝓤₀ ̇
 Fin = pr₁ (center _ fin)

 Fin-equation₀ : Fin  ≡ 𝟘
 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  ≡ 𝟘 + 𝟙
 Fin-equation₁ = refl _

 Fin-equation₂ : Fin  ≡ (𝟘 + 𝟙) + 𝟙
 Fin-equation₂ = refl _

 Fin-equation₃ : Fin  ≡ ((𝟘 + 𝟙) + 𝟙) + 𝟙
 Fin-equation₃ = refl _

infixr -1 -∃!