--- a/src/CCC.agda	Sun Feb 11 11:25:40 2024 +0900
+++ b/src/CCC.agda	Tue Jul 02 08:34:33 2024 +0900
@@ -285,6 +285,14 @@
      Monik : {a : Obj A} (h : Hom A a Ω)  → Mono A (equalizer (Ker h))
      Monik h = record { isMono = λ f g → monic (Ker h ) } 
 
+--  Nat as iniitla object (1→ ℕ → ℕ)
+--
+--     0     s
+--  1 -→  ℕ --→ ℕ 
+--  |     |h    |h
+--  + --→ A --→ A  
+--     a     f
+
 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          Nat   : Obj A