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