N ⟶ N, 0 + n = n

• 03 August 2025
• Mathematics,
• Process book,
• Learning

0 + n = n #

and a quest was "show 0 + n = n"

A proof is a path

0 + n = 0 is a path or, ∃ f : Γ ⟶ {0 + n = 0}

0 + n = 0 is a proposition in Prop

Az egyenlőség 0 + n és n között

The identity 0 + n = n is a path (isomorphism) between types.



∀ n : ℕ, 0 + n = n ∈ Ω -- I still struggle with this

∀ n : ℕ, 0 + n = n : Prop ?    une proposition à prouver, un chemin dans la logique constructive!



💡-- how to write in many ways? 🔁 Logique = Prop, zero_add= preuve/fonction

Prop = logique = Ω = geometry ?

Every morphism to Ω is a proof #maybe Geometry = formes des preuves 🌀

(0 ⟶ 0 + n ⟵ n) ⟶ n
s(a) + s(b) = s(a + b)
s(0) + s(1) = s(0 + 1)
Maybe this stuff seems simple, because I see "Oh 0 + 1" what could be easier? But it is maybe so not very simple. -- Inductive structure makes evaluation possible.
an inductive definition: each step built from the previous.
-- What were the previous steps?
I am starting to understand something! I looked in Topoi [Goldblatt] for the diagram of natural numbers. And by drawing the arrows, and reading the explanation, I learnt for example

• m ∘ n = m + n, which is an insight for me! + is composition on the natural numbers.
• N ⟶ N is an infinite collection arrows, of numbers!, and N is a single thing
• drawing / constructing the diagram shows nicely why 0 + n = n is
  • 0 is the id 1_N, so composing an arrow n with it composes to n
    
    

-- I wonder how to write this in Lean4 and proof trees Also how is this geometry = logic? and, how to draw the evaluation arrows for the ∀ statement 0 + n = n? and how to draw this in Peirce graphs?


ChatGPT again says: Diagramming clarifies logic as geometry. 📐➕🌱    *fascinating! *

Also, these cat-diagrams seem like maybe qualitative geometry (I don't yet have the vocabulary), like it doesn't matter which way arrows point to as long as they are not pointing to the same point with exactly overlapping another arrow which would perhaps be identity?
Maybe this is something like what is meant by logic being geometry?


   diagrams are like maps of relationships, not distances

• arrows (morphisms) are directed paths
• composition = gluing paths: if f : A ⟶ B and g : B ⟶ C, then g ∘ f : A ⟶ C
• commutative diagrams are “geometric equalities”
  
  

-- Ohhhhhh, big insight for me 🎉, this is the definition of a category:

inductive ℕ where
  | zero : ℕ
  | succ : ℕ → ℕ

def add : ℕ → ℕ → ℕ
  | .zero, n     => n
  | .succ m, n   => .succ (add m n)

inductive ℕ where
  | zero : ℕ      -- a single thing
  | succ : ℕ → ℕ  -- the infinite arrows / numbers #maybe 

def add : ℕ → ℕ → ℕ  -- composition is addition
  | .zero, n     => n                 -- where zero is the identity arrow
  | .succ m, n   => .succ (add m n)   -- i don't yet know what this is, associativity?

-- Maybe this is different, because there is recursion here, is there recursion in the topos definition?

🤖 deep bridge between induction, recursion, and topos-theoretic categorical structure    - defines m + n by peeling m down to .zero and building back up    - structurally inductive, mirrors inductive construction of ℕ
1 ──0──▶ ℕ ──s──▶ ℕ
NNO initial object in the category of ℕ-algebras
a universal recursion principle: ∀ a : A , zeroA : A ∧ succA : A → A,
∃ ! f : ℕ ⟶ A respecting them!
in categorical logic, recursion arises from universal properties    —no loops, just arrows with commutative diagrams

  

add zero     n = n
add (succ m) n = succ (add m n)

≈ ∃ ! f,

f(0) = zeroA
f(succ n) = succA (f n)

add is #maybe like 🖇

--What is .succ in the topos diagram?
hitting a drum analogy

🤖🌿

This kind of geometry:
    doesn’t rely on length, shape, or angles.
   but on *form, function, and flow.*
     like voice leading in jazz 🎹🎷: 
     notes move by rules of harmony, not by metric space.

topos as a kind of logical geometry

-- *In this example what are topos as a kind of logical geometry, form, function and flow? *

This seems already recursive:
def N
| z : N

def A
| a : A 

def N | z : N
def A | a : A

def ø | ø ⟶ ø def 🕳 | 🕳 ⟶ 🕳

Hom(ø, ø) = {id}

def ⟶ | ⟶  : ⟶ ?

def ⟶
| ⟶ : ⟶ 
| ⟶ : ⟶ ⟶ ⟶ 

def ⟹
| z : ⟹
| σ : ⟹ ⟶ ⟹

inductive ⟹ where
| z : ⟹                       -- base arrow, like identity or zero
| σ : ⟹ → ⟹ → ⟹              -- composition of two arrows

🤖 a category of arrows, where morphisms compose recursively 

z ≈ stay σ a b ≈ go along a then b

a path category

      a     b
   ● —→ ● —→ ●
     ↘︎σ(a,b)

⼝ + ⼀ + ⼇ → 語

• Previous: Is a pebble mathematical?
• Next: 🦑 N ⟶ N, 0 + n = n 💎 Take 2