Adding natural numbers defined by their associativity property

Cubical/Data/NatPlusOne/Base.agda

@@ -22,6 +22,9 @@ pattern 2+_ n = 1+ (suc n)
 suc₊₁ : ℕ₊₁ → ℕ₊₁
 suc₊₁ (1+ n) = 1+ (suc n)
 
+_+₁_ : ℕ₊₁ → ℕ₊₁ → ℕ₊₁
+(1+ m) +₁ (1+ n) = 1+ (suc (m + n))
+
 -- Natural number literals for ℕ₊₁
 
 open import Cubical.Data.Nat.Literals public

Cubical/Data/NatPlusOne/MoreNats/AssocNat.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.NatPlusOne.MoreNats.AssocNat where
+
+open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base public
+open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Properties public

Cubical/Data/NatPlusOne/MoreNats/AssocNat/Base.agda

@@ -0,0 +1,63 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Unit
+open import Cubical.Data.Nat hiding (_+_)
+
+infixl 6 _+₁_
+
+data ℕ₊₁ : Type where
+  one : ℕ₊₁
+  _+₁_ : ℕ₊₁ → ℕ₊₁ → ℕ₊₁
+  assoc : (a b c : ℕ₊₁) →  a +₁ (b +₁ c) ≡ a +₁ b +₁ c
+  trunc : isSet ℕ₊₁
+
+module Elim {ℓ'} {B : ℕ₊₁ → Type ℓ'}
+  (one* : B one) (_+₁*_ : {m n : ℕ₊₁} → B m → B n → B (m +₁ n))
+  (assoc* : {x y z : ℕ₊₁} (x' : B x) (y' : B y) (z' : B z)
+            → PathP (λ i → B (assoc x y z i))
+            (x' +₁* (y' +₁* z')) ((x' +₁* y') +₁* z'))
+  (trunc* : (n : ℕ₊₁) → isSet (B n)) where
+
+  f : (n : ℕ₊₁) → B n
+  f one = one*
+  f (m +₁ n) = f m +₁* f n
+  f (assoc x y z i) = assoc* (f x) (f y) (f z) i
+  f (trunc m n p q i j) =
+    isOfHLevel→isOfHLevelDep 2 trunc* (f m) (f n)
+    (cong f p) (cong f q) (trunc m n p q) i j
+
+module ElimProp {ℓ'} {B : ℕ₊₁ → Type ℓ'} (BProp : {n : ℕ₊₁} → isProp (B n))
+  (one* : B one) (_+₁*_ : {m n : ℕ₊₁} → B m → B n → B (m +₁ n)) where
+
+  f : (n : ℕ₊₁) → B n
+  f = Elim.f {B = B} one* _+₁*_
+        (λ {x} {y} {z} x' y' z' →
+          toPathP (BProp (transport (λ i → B (assoc x y z i))
+          (x' +₁* (y' +₁* z'))) ((x' +₁* y') +₁* z')))
+        λ n → isProp→isSet BProp
+
+module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B)
+  (one* : B) (_+₁*_ : B → B → B)
+  (assoc* : (a b c : B) → a +₁* (b +₁* c) ≡ (a +₁* b) +₁* c) where
+
+  f : ℕ₊₁ → B
+  f = Elim.f one* (λ m n → m +₁* n) assoc* λ _ → BType
+
+private
+  constraintNumber : ℕ → Type
+  constraintNumber zero = ⊥
+  constraintNumber (suc _) = Unit
+
+  fromNat' : (n : ℕ) ⦃ _ : constraintNumber n ⦄ → ℕ₊₁
+  fromNat' zero ⦃ () ⦄
+  fromNat' (suc zero) = one
+  fromNat' (suc (suc n)) = fromNat' (suc n) +₁ one
+
+instance
+  NumN : HasFromNat ℕ₊₁
+  NumN = record { Constraint = constraintNumber ; fromNat = fromNat' }

Cubical/Data/NatPlusOne/MoreNats/AssocNat/Properties.agda

@@ -0,0 +1,39 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.NatPlusOne.MoreNats.AssocNat.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Nat
+open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base
+open import Cubical.Data.NatPlusOne renaming (ℕ₊₁ to Nat; one to one'; _+₁_ to _+₁'_)
+
+Nat→ℕ₊₁ : Nat → ℕ₊₁
+Nat→ℕ₊₁ one' = 1
+Nat→ℕ₊₁ (2+ n) = 1 +₁ Nat→ℕ₊₁ (1+ n)
+
+ℕ₊₁→Nat : ℕ₊₁ → Nat
+ℕ₊₁→Nat one = 1
+ℕ₊₁→Nat (a +₁ b) = ℕ₊₁→Nat a +₁' ℕ₊₁→Nat b
+ℕ₊₁→Nat (assoc a b c i) = +₁-assoc (ℕ₊₁→Nat a) (ℕ₊₁→Nat b) (ℕ₊₁→Nat c) i
+ℕ₊₁→Nat (trunc m n p q i j) =
+  1+ (isSetℕ _ _ (λ k → -1+ (ℕ₊₁→Nat (p k))) (λ k → -1+ (ℕ₊₁→Nat (q k))) i j)
+
+ℕ₊₁→Nat→ℕ₊₁ : ∀ n → ℕ₊₁→Nat (Nat→ℕ₊₁ n) ≡ n
+ℕ₊₁→Nat→ℕ₊₁ one' = refl
+ℕ₊₁→Nat→ℕ₊₁ (2+ n) = cong (1+_ ∘ suc ∘ -1+_) (ℕ₊₁→Nat→ℕ₊₁ (1+ n))
+
+private
+  Nat→ℕ₊₁-+ : ∀ a b → Nat→ℕ₊₁ (a +₁' b) ≡ Nat→ℕ₊₁ a +₁ Nat→ℕ₊₁ b
+  Nat→ℕ₊₁-+ one' b = refl
+  Nat→ℕ₊₁-+ (2+ a) b = cong (one +₁_) (Nat→ℕ₊₁-+ (1+ a) b)
+    ∙ assoc one (Nat→ℕ₊₁ (1+ a)) (Nat→ℕ₊₁ b)
+
+Nat→ℕ₊₁→Nat : ∀ n → Nat→ℕ₊₁ (ℕ₊₁→Nat n) ≡ n
+Nat→ℕ₊₁→Nat = ElimProp.f (trunc _ _) (λ i → one)
+  λ {a} {b} m n → Nat→ℕ₊₁-+ (ℕ₊₁→Nat a) (ℕ₊₁→Nat b) ∙ (λ i → m i +₁ n i)
+
+ℕ₊₁≡Nat : ℕ₊₁ ≡ Nat
+ℕ₊₁≡Nat = isoToPath (iso ℕ₊₁→Nat Nat→ℕ₊₁ ℕ₊₁→Nat→ℕ₊₁ Nat→ℕ₊₁→Nat)

Cubical/Data/NatPlusOne/Properties.agda

@@ -25,6 +25,10 @@ private
   ℕ₊₁→ℕ-·₊₁-comm : ∀ m n → ℕ₊₁→ℕ (m ·₊₁ n) ≡ (ℕ₊₁→ℕ m) · (ℕ₊₁→ℕ n)
   ℕ₊₁→ℕ-·₊₁-comm (1+ m) (1+ n) = refl
 
++₁-assoc : ∀ m n o → m +₁ (n +₁ o) ≡ (m +₁ n) +₁ o
++₁-assoc one n o = refl
++₁-assoc (2+ m) n o = cong suc₊₁ (+₁-assoc (1+ m) n o)
+
 ·₊₁-comm : ∀ m n → m ·₊₁ n ≡ n ·₊₁ m
 ·₊₁-comm (1+ m) (1+ n) = cong 1+_ (injSuc (·-comm (suc m) (suc n)))