From 03dc09d0f6fddf296322be8ccfbf44f32f659259 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sun, 23 Nov 2025 18:01:52 +0100
Subject: [PATCH 1/4] Attempt at the INT construction

---
 src/Data/Integer/IntConstruction.agda         |  50 ++++
 .../Integer/IntConstruction/Properties.agda   | 249 ++++++++++++++++++
 2 files changed, 299 insertions(+)
 create mode 100644 src/Data/Integer/IntConstruction.agda
 create mode 100644 src/Data/Integer/IntConstruction/Properties.agda

diff --git a/src/Data/Integer/IntConstruction.agda b/src/Data/Integer/IntConstruction.agda
new file mode 100644
index 0000000000..be7d10fcce
--- /dev/null
+++ b/src/Data/Integer/IntConstruction.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction where
+
+open import Data.Nat.Base as ℕ using (ℕ)
+open import Function.Base using (flip)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+infixl 6 _⊖_
+
+record ℤ : Set where
+  constructor _⊖_
+  field
+    minuend : ℕ
+    subtrahend : ℕ
+
+_≃_ : Rel ℤ _
+(a ⊖ b) ≃ (c ⊖ d) = a ℕ.+ d ≡ c ℕ.+ b
+
+_≤_ : Rel ℤ _
+(a ⊖ b) ≤ (c ⊖ d) = a ℕ.+ d ℕ.≤ c ℕ.+ b
+
+_≥_ : Rel ℤ _
+_≥_ = flip _≤_
+
+_<_ : Rel ℤ _
+(a ⊖ b) < (c ⊖ d) = a ℕ.+ d ℕ.< c ℕ.+ b
+
+_>_ : Rel ℤ _
+_>_ = flip _<_
+
+0ℤ : ℤ
+0ℤ = 0 ⊖ 0
+
+1ℤ : ℤ
+1ℤ = 1 ⊖ 0
+
+_+_ : ℤ → ℤ → ℤ
+(a ⊖ b) + (c ⊖ d) = (a ℕ.+ c) ⊖ (b ℕ.+ d)
+
+_*_ : ℤ → ℤ → ℤ
+(a ⊖ b) * (c ⊖ d) = (a ℕ.* c ℕ.+ b ℕ.* d) ⊖ (a ℕ.* d ℕ.+ b ℕ.* c)
+
+-_ : ℤ → ℤ
+- (a ⊖ b) = b ⊖ a
+
+∣_∣ : ℤ → ℕ
+∣ a ⊖ b ∣ = ℕ.∣ a - b ∣′
+
diff --git a/src/Data/Integer/IntConstruction/Properties.agda b/src/Data/Integer/IntConstruction/Properties.agda
new file mode 100644
index 0000000000..7848c7a1eb
--- /dev/null
+++ b/src/Data/Integer/IntConstruction/Properties.agda
@@ -0,0 +1,249 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction.Properties where
+
+import Algebra.Properties.CommutativeSemigroup as CommSemigroupProps
+open import Data.Integer.IntConstruction
+open import Data.Nat.Base as ℕ using (ℕ)
+import Data.Nat.Properties as ℕ
+open import Function.Base
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary.Decidable
+
+open import Algebra.Definitions _≃_
+
+private
+  trans-helper
+    : ∀ {r} (R : Rel ℕ r)
+      → ∀ a b c d e f
+      → R (a ℕ.+ d ℕ.+ (c ℕ.+ f)) (c ℕ.+ b ℕ.+ (e ℕ.+ d))
+     → R ((a ℕ.+ f) ℕ.+ (d ℕ.+ c)) ((e ℕ.+ b) ℕ.+ (d ℕ.+ c))
+  trans-helper R a b c d e f mono = subst₂ R preamble postamble mono
+    where
+      open ≡-Reasoning
+      open CommSemigroupProps ℕ.+-commutativeSemigroup
+      preamble : (a ℕ.+ d) ℕ.+ (c ℕ.+ f) ≡ (a ℕ.+ f) ℕ.+ (d ℕ.+ c)
+      preamble = begin
+        (a ℕ.+ d) ℕ.+ (c ℕ.+ f) ≡⟨ cong (a ℕ.+ d ℕ.+_) (ℕ.+-comm c f) ⟩
+        (a ℕ.+ d) ℕ.+ (f ℕ.+ c) ≡⟨ medial a d f c ⟩
+        (a ℕ.+ f) ℕ.+ (d ℕ.+ c) ∎
+      postamble : (c ℕ.+ b) ℕ.+ (e ℕ.+ d) ≡ (e ℕ.+ b) ℕ.+ (d ℕ.+ c)
+      postamble = begin
+        (c ℕ.+ b) ℕ.+ (e ℕ.+ d) ≡⟨ ℕ.+-comm (c ℕ.+ b) (e ℕ.+ d) ⟩
+        (e ℕ.+ d) ℕ.+ (c ℕ.+ b) ≡⟨ cong (e ℕ.+ d ℕ.+_) (ℕ.+-comm c b) ⟩
+        (e ℕ.+ d) ℕ.+ (b ℕ.+ c) ≡⟨ medial e d b c ⟩
+        (e ℕ.+ b) ℕ.+ (d ℕ.+ c) ∎
+
+------------------------------------------------------------------------
+-- Properties of _≃_
+
+≃-refl : Reflexive _≃_
+≃-refl = refl
+
+≃-sym : Symmetric _≃_
+≃-sym = sym
+
+≃-trans : Transitive _≃_
+≃-trans {a ⊖ b} {c ⊖ d} {e ⊖ f} i≃j j≃k = ℕ.+-cancelʳ-≡ (d ℕ.+ c) (a ℕ.+ f) (e ℕ.+ b) $ trans-helper _≡_ a b c d e f (cong₂ ℕ._+_ i≃j j≃k)
+
+_≃?_ : Decidable _≃_
+(a ⊖ b) ≃? (c ⊖ d) = a ℕ.+ d ℕ.≟ c ℕ.+ b
+
+------------------------------------------------------------------------
+-- Properties of _≤_
+
+≤-refl : Reflexive _≤_
+≤-refl = ℕ.≤-refl
+
+≤-trans : Transitive _≤_
+≤-trans {a ⊖ b} {c ⊖ d} {e ⊖ f} i≤j j≤k = ℕ.+-cancelʳ-≤ (d ℕ.+ c) (a ℕ.+ f) (e ℕ.+ b) $ trans-helper ℕ._≤_ a b c d e f (ℕ.+-mono-≤ i≤j j≤k)
+
+≤-antisym : Antisymmetric _≃_ _≤_
+≤-antisym i≤j j≤i = ℕ.≤-antisym i≤j j≤i
+
+≤-total : Total _≤_
+≤-total (a ⊖ b) (c ⊖ d) = ℕ.≤-total (a ℕ.+ d) (c ℕ.+ b)
+
+_≤?_ : Decidable _≤_
+(a ⊖ b) ≤? (c ⊖ d) = a ℕ.+ d ℕ.≤? c ℕ.+ b
+
+------------------------------------------------------------------------
+-- Properties of _<_
+
+<-irrefl : Irreflexive _≃_ _<_
+<-irrefl = ℕ.<-irrefl
+
+<-trans : Transitive _<_
+<-trans {a ⊖ b} {c ⊖ d} {e ⊖ f} i<j j<k = ℕ.+-cancelʳ-< (d ℕ.+ c) (a ℕ.+ f) (e ℕ.+ b) $ trans-helper ℕ._<_ a b c d e f (ℕ.+-mono-< i<j j<k)
+
+<-respˡ-≃ : _<_ Respectsˡ _≃_
+<-respˡ-≃ {a ⊖ b} {c ⊖ d} {e ⊖ f} j≃k i>j = ℕ.+-cancelʳ-< (d ℕ.+ c) (e ℕ.+ b) (a ℕ.+ f) $ trans-helper ℕ._>_ a b c d e f (ℕ.+-mono-<-≤ i>j (ℕ.≤-reflexive (sym j≃k)))
+
+<-respʳ-≃ : _<_ Respectsʳ _≃_
+<-respʳ-≃ {a ⊖ b} {c ⊖ d} {e ⊖ f} j≃k i<j = ℕ.+-cancelʳ-< (d ℕ.+ c) (a ℕ.+ f) (e ℕ.+ b) $ trans-helper ℕ._<_ a b c d e f (ℕ.+-mono-<-≤ i<j (ℕ.≤-reflexive j≃k))
+
+_<?_ : Decidable _<_
+(a ⊖ b) <? (c ⊖ d) = a ℕ.+ d ℕ.<? c ℕ.+ b
+
+<-cmp : Trichotomous _≃_ _<_
+<-cmp (a ⊖ b) (c ⊖ d) = ℕ.<-cmp (a ℕ.+ d) (c ℕ.+ b)
+
+------------------------------------------------------------------------
+-- Algebraic properties of _+_
+
++-cong : Congruent₂ _+_
++-cong {a ⊖ b} {c ⊖ d} {e ⊖ f} {g ⊖ h} a+d≡c+b e+h≡g+f = begin
+  (a ℕ.+ e) ℕ.+ (d ℕ.+ h) ≡⟨ medial a e d h ⟩
+  (a ℕ.+ d) ℕ.+ (e ℕ.+ h) ≡⟨ cong₂ ℕ._+_ a+d≡c+b e+h≡g+f ⟩
+  (c ℕ.+ b) ℕ.+ (g ℕ.+ f) ≡⟨ medial c b g f ⟩
+  (c ℕ.+ g) ℕ.+ (b ℕ.+ f) ∎
+  where
+    open ≡-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+
++-assoc : Associative _+_
++-assoc (a ⊖ b) (c ⊖ d) (e ⊖ f) = cong₂ ℕ._+_ (ℕ.+-assoc a c e) (sym (ℕ.+-assoc b d f))
+
++-identityˡ : LeftIdentity 0ℤ _+_
++-identityˡ (a ⊖ b) = refl
+
++-identityʳ : RightIdentity 0ℤ _+_
++-identityʳ (a ⊖ b) = cong₂ ℕ._+_ (ℕ.+-identityʳ a) (sym (ℕ.+-identityʳ b))
+
++-comm : Commutative _+_
++-comm (a ⊖ b) (c ⊖ d) = cong₂ ℕ._+_ (ℕ.+-comm a c) (ℕ.+-comm d b)
+
+------------------------------------------------------------------------
+-- Properties of _+_ and _≤_
+
++-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
++-mono-≤ {a ⊖ b} {c ⊖ d} {e ⊖ f} {g ⊖ h} a+d≤c+b e+h≤g+f = begin
+  (a ℕ.+ e) ℕ.+ (d ℕ.+ h) ≡⟨ medial a e d h ⟩
+  (a ℕ.+ d) ℕ.+ (e ℕ.+ h) ≤⟨ ℕ.+-mono-≤ a+d≤c+b e+h≤g+f ⟩
+  (c ℕ.+ b) ℕ.+ (g ℕ.+ f) ≡⟨ medial c b g f ⟩
+  (c ℕ.+ g) ℕ.+ (b ℕ.+ f) ∎
+  where
+    open ℕ.≤-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+
+------------------------------------------------------------------------
+-- Algebraic properties of -_
+
+-‿cong : Congruent₁ -_
+-‿cong {a ⊖ b} {c ⊖ d} a+d≡c+b = begin
+  b ℕ.+ c ≡⟨ ℕ.+-comm b c ⟩
+  c ℕ.+ b ≡⟨ a+d≡c+b ⟨
+  a ℕ.+ d ≡⟨ ℕ.+-comm a d ⟩
+  d ℕ.+ a ∎
+  where open ≡-Reasoning
+
++-inverseˡ : LeftInverse 0ℤ -_ _+_
++-inverseˡ (a ⊖ b) = trans (ℕ.+-identityʳ (b ℕ.+ a)) (ℕ.+-comm b a)
+
++-inverseʳ : RightInverse 0ℤ -_ _+_
++-inverseʳ (a ⊖ b) = trans (ℕ.+-identityʳ (a ℕ.+ b)) (ℕ.+-comm a b)
+
+------------------------------------------------------------------------
+-- Properties of -_ and _≤_
+
+-‿anti-≤ : Antitonic₁ _≤_ _≤_ -_
+-‿anti-≤ {a ⊖ b} {c ⊖ d} a+d≥c+b = begin
+  b ℕ.+ c ≡⟨ ℕ.+-comm b c ⟩
+  c ℕ.+ b ≤⟨ a+d≥c+b ⟩
+  a ℕ.+ d ≡⟨ ℕ.+-comm a d ⟩
+  d ℕ.+ a ∎
+  where open ℕ.≤-Reasoning
+
+------------------------------------------------------------------------
+-- Algebraic properties of _*_
+
+*-cong : Congruent₂ _*_
+*-cong {a ⊖ b} {c ⊖ d} {e ⊖ f} {g ⊖ h} a+d≡c+b e+h≡g+f = ℕ.+-cancelʳ-≡ (d ℕ.* e) _ _ $ begin
+  ((a ℕ.* e ℕ.+ b ℕ.* f) ℕ.+ (c ℕ.* h ℕ.+ d ℕ.* g)) ℕ.+ d ℕ.* e ≡⟨ ℕ.+-assoc (a ℕ.* e ℕ.+ b ℕ.* f) (c ℕ.* h ℕ.+ d ℕ.* g) (d ℕ.* e) ⟩
+  (a ℕ.* e ℕ.+ b ℕ.* f) ℕ.+ ((c ℕ.* h ℕ.+ d ℕ.* g) ℕ.+ d ℕ.* e) ≡⟨ cong (a ℕ.* e ℕ.+ b ℕ.* f ℕ.+_) (ℕ.+-comm (c ℕ.* h ℕ.+ d ℕ.* g) (d ℕ.* e)) ⟩
+  (a ℕ.* e ℕ.+ b ℕ.* f) ℕ.+ (d ℕ.* e ℕ.+ (c ℕ.* h ℕ.+ d ℕ.* g)) ≡⟨ medial (a ℕ.* e) (b ℕ.* f) (d ℕ.* e) (c ℕ.* h ℕ.+ d ℕ.* g) ⟩
+  (a ℕ.* e ℕ.+ d ℕ.* e) ℕ.+ (b ℕ.* f ℕ.+ (c ℕ.* h ℕ.+ d ℕ.* g)) ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribʳ-+ e a d) (ℕ.+-comm (c ℕ.* h ℕ.+ d ℕ.* g) (b ℕ.* f)) ⟨
+  (a ℕ.+ d) ℕ.* e ℕ.+ ((c ℕ.* h ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)       ≡⟨ cong (λ k → k ℕ.* e ℕ.+ ((c ℕ.* h ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)) a+d≡c+b ⟩
+  (c ℕ.+ b) ℕ.* e ℕ.+ ((c ℕ.* h ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)       ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribʳ-+ e c b) (ℕ.+-assoc (c ℕ.* h) (d ℕ.* g) (b ℕ.* f)) ⟩
+  (c ℕ.* e ℕ.+ b ℕ.* e) ℕ.+ (c ℕ.* h ℕ.+ (d ℕ.* g ℕ.+ b ℕ.* f)) ≡⟨ medial (c ℕ.* e) (b ℕ.* e) (c ℕ.* h) (d ℕ.* g ℕ.+ b ℕ.* f) ⟩
+  (c ℕ.* e ℕ.+ c ℕ.* h) ℕ.+ (b ℕ.* e ℕ.+ (d ℕ.* g ℕ.+ b ℕ.* f)) ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribˡ-+ c e h) (ℕ.+-assoc (b ℕ.* e) (d ℕ.* g) (b ℕ.* f)) ⟨
+  c ℕ.* (e ℕ.+ h) ℕ.+ ((b ℕ.* e ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)       ≡⟨ cong (λ k → c ℕ.* k ℕ.+ ((b ℕ.* e ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)) e+h≡g+f ⟩
+  c ℕ.* (g ℕ.+ f) ℕ.+ ((b ℕ.* e ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)       ≡⟨ cong (ℕ._+ ((b ℕ.* e ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f)) (ℕ.*-distribˡ-+ c g f) ⟩
+  (c ℕ.* g ℕ.+ c ℕ.* f) ℕ.+ ((b ℕ.* e ℕ.+ d ℕ.* g) ℕ.+ b ℕ.* f) ≡⟨ medial (c ℕ.* g) (c ℕ.* f) (b ℕ.* e ℕ.+ d ℕ.* g) (b ℕ.* f) ⟩
+  (c ℕ.* g ℕ.+ (b ℕ.* e ℕ.+ d ℕ.* g)) ℕ.+ (c ℕ.* f ℕ.+ b ℕ.* f) ≡⟨ cong₂ ℕ._+_ (ℕ.+-assoc (c ℕ.* g) (b ℕ.* e) (d ℕ.* g)) (ℕ.*-distribʳ-+ f c b) ⟨
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ d ℕ.* g) ℕ.+ (c ℕ.+ b) ℕ.* f       ≡⟨ cong (λ k → ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ d ℕ.* g) ℕ.+ k ℕ.* f) a+d≡c+b ⟨
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ d ℕ.* g) ℕ.+ (a ℕ.+ d) ℕ.* f       ≡⟨ cong (c ℕ.* g ℕ.+ b ℕ.* e ℕ.+ d ℕ.* g ℕ.+_) (ℕ.*-distribʳ-+ f a d) ⟩
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ d ℕ.* g) ℕ.+ (a ℕ.* f ℕ.+ d ℕ.* f) ≡⟨ medial (c ℕ.* g ℕ.+ b ℕ.* e) (d ℕ.* g) (a ℕ.* f) (d ℕ.* f) ⟩
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ a ℕ.* f) ℕ.+ (d ℕ.* g ℕ.+ d ℕ.* f) ≡⟨ cong (((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ a ℕ.* f) ℕ.+_) (ℕ.*-distribˡ-+ d g f)  ⟨
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ a ℕ.* f) ℕ.+ d ℕ.* (g ℕ.+ f)       ≡⟨ cong (λ k → c ℕ.* g ℕ.+ b ℕ.* e ℕ.+ a ℕ.* f ℕ.+ d ℕ.* k) e+h≡g+f ⟨
+  ((c ℕ.* g ℕ.+ b ℕ.* e) ℕ.+ a ℕ.* f) ℕ.+ d ℕ.* (e ℕ.+ h)       ≡⟨ cong₂ (λ j k → j ℕ.+ d ℕ.* k) (ℕ.+-assoc (c ℕ.* g) (b ℕ.* e) (a ℕ.* f)) (ℕ.+-comm e h) ⟩
+  (c ℕ.* g ℕ.+ (b ℕ.* e ℕ.+ a ℕ.* f)) ℕ.+ d ℕ.* (h ℕ.+ e)       ≡⟨ cong₂ (λ j k → c ℕ.* g ℕ.+ j ℕ.+ k) (ℕ.+-comm (b ℕ.* e) (a ℕ.* f)) (ℕ.*-distribˡ-+ d h e) ⟩
+  (c ℕ.* g ℕ.+ (a ℕ.* f ℕ.+ b ℕ.* e)) ℕ.+ (d ℕ.* h ℕ.+ d ℕ.* e) ≡⟨ medial (c ℕ.* g) (a ℕ.* f ℕ.+ b ℕ.* e) (d ℕ.* h) (d ℕ.* e) ⟩
+  (c ℕ.* g ℕ.+ d ℕ.* h) ℕ.+ ((a ℕ.* f ℕ.+ b ℕ.* e) ℕ.+ d ℕ.* e) ≡⟨ ℕ.+-assoc (c ℕ.* g ℕ.+ d ℕ.* h) (a ℕ.* f ℕ.+ b ℕ.* e) (d ℕ.* e) ⟨
+  ((c ℕ.* g ℕ.+ d ℕ.* h) ℕ.+ (a ℕ.* f ℕ.+ b ℕ.* e)) ℕ.+ d ℕ.* e ∎
+  where
+    open ≡-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+
+*-assoc : Associative _*_
+*-assoc (a ⊖ b) (c ⊖ d) (e ⊖ f) = cong₂ ℕ._+_ (lemma a b c d e f) (sym (lemma a b c d f e))
+  where
+    open ≡-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+    lemma : ∀ u v w x y z → (u ℕ.* w ℕ.+ v ℕ.* x) ℕ.* y ℕ.+ (u ℕ.* x ℕ.+ v ℕ.* w) ℕ.* z
+                          ≡ u ℕ.* (w ℕ.* y ℕ.+ x ℕ.* z) ℕ.+ v ℕ.* (w ℕ.* z ℕ.+ x ℕ.* y)
+    lemma u v w x y z = begin
+      (u ℕ.* w ℕ.+ v ℕ.* x) ℕ.* y ℕ.+ (u ℕ.* x ℕ.+ v ℕ.* w) ℕ.* z                     ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribʳ-+ y (u ℕ.* w) (v ℕ.* x)) (ℕ.*-distribʳ-+ z (u ℕ.* x) (v ℕ.* w)) ⟩
+      ((u ℕ.* w) ℕ.* y ℕ.+ (v ℕ.* x) ℕ.* y) ℕ.+ ((u ℕ.* x) ℕ.* z ℕ.+ (v ℕ.* w) ℕ.* z) ≡⟨ cong₂ ℕ._+_ (cong₂ ℕ._+_ (ℕ.*-assoc u w y) (ℕ.*-assoc v x y)) (cong₂ ℕ._+_ (ℕ.*-assoc u x z) (ℕ.*-assoc v w z)) ⟩
+      (u ℕ.* (w ℕ.* y) ℕ.+ v ℕ.* (x ℕ.* y)) ℕ.+ (u ℕ.* (x ℕ.* z) ℕ.+ v ℕ.* (w ℕ.* z)) ≡⟨ medial (u ℕ.* (w ℕ.* y)) (v ℕ.* (x ℕ.* y)) (u ℕ.* (x ℕ.* z)) (v ℕ.* (w ℕ.* z)) ⟩
+      (u ℕ.* (w ℕ.* y) ℕ.+ u ℕ.* (x ℕ.* z)) ℕ.+ (v ℕ.* (x ℕ.* y) ℕ.+ v ℕ.* (w ℕ.* z)) ≡⟨ cong ((u ℕ.* (w ℕ.* y) ℕ.+ u ℕ.* (x ℕ.* z)) ℕ.+_) (ℕ.+-comm (v ℕ.* (x ℕ.* y)) (v ℕ.* (w ℕ.* z))) ⟩
+      (u ℕ.* (w ℕ.* y) ℕ.+ u ℕ.* (x ℕ.* z)) ℕ.+ (v ℕ.* (w ℕ.* z) ℕ.+ v ℕ.* (x ℕ.* y)) ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribˡ-+ u (w ℕ.* y) (x ℕ.* z)) (ℕ.*-distribˡ-+ v (w ℕ.* z) (x ℕ.* y)) ⟨
+      u ℕ.* (w ℕ.* y ℕ.+ x ℕ.* z) ℕ.+ v ℕ.* (w ℕ.* z ℕ.+ x ℕ.* y)                     ∎
+
+*-zeroˡ : LeftZero 0ℤ _*_
+*-zeroˡ _ = refl
+
+*-zeroʳ : RightZero 0ℤ _*_
+*-zeroʳ _ = ℕ.+-identityʳ _
+
+*-identityˡ : LeftIdentity 1ℤ _*_
+*-identityˡ (a ⊖ b) = cong₂ ℕ._+_ (lemma a) (sym (lemma b))
+  where
+    lemma : ∀ n → n ℕ.+ 0 ℕ.+ 0 ≡ n
+    lemma n = trans (ℕ.+-identityʳ (n ℕ.+ 0)) (ℕ.+-identityʳ n)
+
+*-identityʳ : RightIdentity 1ℤ _*_
+*-identityʳ (a ⊖ b) = cong₂ ℕ._+_ l (sym r)
+  where
+    l : a ℕ.* 1 ℕ.+ b ℕ.* 0 ≡ a
+    l = trans (cong₂ ℕ._+_ (ℕ.*-identityʳ a) (ℕ.*-zeroʳ b)) (ℕ.+-identityʳ a)
+    r : a ℕ.* 0 ℕ.+ b ℕ.* 1 ≡ b
+    r = trans (cong₂ ℕ._+_ (ℕ.*-zeroʳ a) (ℕ.*-identityʳ b)) (ℕ.+-identityˡ b)
+
+*-distribˡ-+ : _*_ DistributesOverˡ _+_
+*-distribˡ-+ (a ⊖ b) (c ⊖ d) (e ⊖ f) = cong₂ ℕ._+_ (lemma a b c d e f) (sym (lemma a b d c f e))
+  where
+    open ≡-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+    lemma : ∀ u v w x y z → u ℕ.* (w ℕ.+ y) ℕ.+ v ℕ.* (x ℕ.+ z)
+                            ≡ (u ℕ.* w ℕ.+ v ℕ.* x) ℕ.+ (u ℕ.* y ℕ.+ v ℕ.* z)
+    lemma u v w x y z = begin
+      u ℕ.* (w ℕ.+ y) ℕ.+ v ℕ.* (x ℕ.+ z)             ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribˡ-+ u w y) (ℕ.*-distribˡ-+ v x z) ⟩
+      (u ℕ.* w ℕ.+ u ℕ.* y) ℕ.+ (v ℕ.* x ℕ.+ v ℕ.* z) ≡⟨ medial (u ℕ.* w) (u ℕ.* y) (v ℕ.* x) (v ℕ.* z) ⟩
+      (u ℕ.* w ℕ.+ v ℕ.* x) ℕ.+ (u ℕ.* y ℕ.+ v ℕ.* z) ∎
+
+*-distribʳ-+ : _*_ DistributesOverʳ _+_
+*-distribʳ-+ (a ⊖ b) (c ⊖ d) (e ⊖ f) = cong₂ ℕ._+_ (lemma a b c d e f) (sym (lemma b a c d e f))
+  where
+    open ≡-Reasoning
+    open CommSemigroupProps ℕ.+-commutativeSemigroup
+    lemma : ∀ u v w x y z → (w ℕ.+ y) ℕ.* u ℕ.+ (x ℕ.+ z) ℕ.* v
+                          ≡ (w ℕ.* u ℕ.+ x ℕ.* v) ℕ.+ (y ℕ.* u ℕ.+ z ℕ.* v)
+    lemma u v w x y z = begin
+      (w ℕ.+ y) ℕ.* u ℕ.+ (x ℕ.+ z) ℕ.* v             ≡⟨ cong₂ ℕ._+_ (ℕ.*-distribʳ-+ u w y) (ℕ.*-distribʳ-+ v x z) ⟩
+      (w ℕ.* u ℕ.+ y ℕ.* u) ℕ.+ (x ℕ.* v ℕ.+ z ℕ.* v) ≡⟨ medial (w ℕ.* u) (y ℕ.* u) (x ℕ.* v) (z ℕ.* v) ⟩
+      (w ℕ.* u ℕ.+ x ℕ.* v) ℕ.+ (y ℕ.* u ℕ.+ z ℕ.* v) ∎
+
+*-comm : Commutative _*_
+*-comm (a ⊖ b) (c ⊖ d) = cong₂ ℕ._+_ (cong₂ ℕ._+_ (ℕ.*-comm a c) (ℕ.*-comm b d)) (trans (ℕ.+-comm (c ℕ.* b) (d ℕ.* a)) (cong₂ ℕ._+_ (ℕ.*-comm d a) (ℕ.*-comm c b)))

From 0627e8a018288f01dbe9aa84a4867b8fe85a9090 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sun, 23 Nov 2025 18:15:28 +0100
Subject: [PATCH 2/4] module headers

---
 src/Data/Integer/IntConstruction.agda            | 6 ++++++
 src/Data/Integer/IntConstruction/Properties.agda | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/src/Data/Integer/IntConstruction.agda b/src/Data/Integer/IntConstruction.agda
index be7d10fcce..4ba9eba3b3 100644
--- a/src/Data/Integer/IntConstruction.agda
+++ b/src/Data/Integer/IntConstruction.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Construction of integers as a pair of naturals
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --cubical-compatible #-}
 
 module Data.Integer.IntConstruction where
diff --git a/src/Data/Integer/IntConstruction/Properties.agda b/src/Data/Integer/IntConstruction/Properties.agda
index 7848c7a1eb..c7bc946be9 100644
--- a/src/Data/Integer/IntConstruction/Properties.agda
+++ b/src/Data/Integer/IntConstruction/Properties.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the construction of integers as a pair of naturals
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --cubical-compatible #-}
 
 module Data.Integer.IntConstruction.Properties where

From c87650903f9fc3588ffc130dac024cdbdc69f09c Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 24 Nov 2025 09:50:57 +0100
Subject: [PATCH 3/4] Add relation between integer definitions

---
 .../IntConstruction/IntProperties.agda        | 72 +++++++++++++++++++
 src/Data/Integer/IntConstruction/Tmp.agda     | 24 +++++++
 2 files changed, 96 insertions(+)
 create mode 100644 src/Data/Integer/IntConstruction/IntProperties.agda
 create mode 100644 src/Data/Integer/IntConstruction/Tmp.agda

diff --git a/src/Data/Integer/IntConstruction/IntProperties.agda b/src/Data/Integer/IntConstruction/IntProperties.agda
new file mode 100644
index 0000000000..2b6a16b09d
--- /dev/null
+++ b/src/Data/Integer/IntConstruction/IntProperties.agda
@@ -0,0 +1,72 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- To be merged into Data.Integer.Properties before merging!
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction.IntProperties where
+
+open import Data.Integer.Base
+open import Data.Integer.IntConstruction as INT using (_≃_)
+open import Data.Integer.IntConstruction.Tmp
+open import Data.Integer.Properties
+import Data.Nat.Base as ℕ
+open import Data.Product.Base
+open import Function.Base
+open import Relation.Binary.PropositionalEquality
+
+fromINT-cong : ∀ {i j} → i ≃ j → fromINT i ≡ fromINT j
+fromINT-cong {a INT.⊖ b} {c INT.⊖ d} a+d≡c+b = begin
+  a ⊖ b                       ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b                   ≡⟨ cong (_- + b) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) - + b            ≡⟨ cong (λ z → (+ a + z) - + b) (+-inverseʳ (+ d)) ⟨
+  (+ a + (+ d - + d)) - + b   ≡⟨ cong (_- + b) (+-assoc (+ a) (+ d) (- + d)) ⟨
+  (+ (a ℕ.+ d) - + d) - + b   ≡⟨ cong (λ z → (+ z - + d) - + b) a+d≡c+b ⟩
+  (+ (c ℕ.+ b) - + d) - + b   ≡⟨ cong (_- + b) (+-assoc (+ c) (+ b) (- + d)) ⟩
+  (+ c + (+ b - + d)) - + b   ≡⟨ cong (λ z → (+ c + z) - + b) (+-comm (+ b) (- + d)) ⟩
+  (+ c + (- + d + + b)) - + b ≡⟨ cong (_- + b) (+-assoc (+ c) (- + d) (+ b)) ⟨
+  ((+ c - + d) + + b) - + b   ≡⟨ +-assoc (+ c - + d) (+ b) (- + b) ⟩
+  (+ c - + d) + (+ b - + b)   ≡⟨ cong₂ _+_ (m-n≡m⊖n c d) (+-inverseʳ (+ b)) ⟩
+  c ⊖ d + 0ℤ                  ≡⟨ +-identityʳ (c ⊖ d) ⟩
+  c ⊖ d                       ∎
+  where open ≡-Reasoning
+
+fromINT-injective : ∀ {i j} → fromINT i ≡ fromINT j → i ≃ j
+fromINT-injective {a INT.⊖ b} {c INT.⊖ d} a⊖b≡c⊖d = +-injective $ begin
+  + a + + d                   ≡⟨ cong (_+ + d) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) + + d            ≡⟨ cong (λ z → (+ a + z) + + d) (+-inverseˡ (+ b)) ⟨
+  (+ a + (- + b + + b)) + + d ≡⟨ cong (_+ + d) (+-assoc (+ a) (- + b) (+ b)) ⟨
+  ((+ a - + b) + + b) + + d   ≡⟨ cong (λ z → (z + + b) + + d) (m-n≡m⊖n a b) ⟩
+  (a ⊖ b + + b) + + d         ≡⟨ cong (λ z → (z + + b) + + d) a⊖b≡c⊖d ⟩
+  (c ⊖ d + + b) + + d         ≡⟨ cong (λ z → (z + + b) + + d) (m-n≡m⊖n c d) ⟨
+  ((+ c - + d) + + b) + + d   ≡⟨ cong (_+ + d) (+-assoc (+ c) (- + d) (+ b)) ⟩
+  (+ c + (- + d + + b)) + + d ≡⟨ cong (λ z → (+ c + z) + + d) (+-comm (- + d) (+ b)) ⟩
+  (+ c + (+ b - + d)) + + d   ≡⟨ cong (_+ + d) (+-assoc (+ c) (+ b) (- + d)) ⟨
+  ((+ c + + b) - + d) + + d   ≡⟨ +-assoc (+ c + + b) (- + d) (+ d) ⟩
+  (+ c + + b) + (- + d + + d) ≡⟨ cong (_+_ (+ c + + b)) (+-inverseˡ (+ d)) ⟩
+  (+ c + + b) + 0ℤ            ≡⟨ +-identityʳ (+ c + + b) ⟩
+  + c + + b                   ∎
+  where open ≡-Reasoning
+
+fromINT-surjective : ∀ j → ∃[ i ] ∀ {z} → z ≃ i → fromINT z ≡ j
+fromINT-surjective j .proj₁ = toINT j
+fromINT-surjective (+ n) .proj₂ {a INT.⊖ b} a+0≡n+b = begin
+  a ⊖ b             ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b         ≡⟨ cong (_- + b) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) - + b  ≡⟨ cong (λ z → + z - + b) a+0≡n+b ⟩
+  (+ n + + b) - + b ≡⟨ +-assoc (+ n) (+ b) (- + b) ⟩
+  + n + (+ b - + b) ≡⟨ cong (_+_ (+ n)) (+-inverseʳ (+ b)) ⟩
+  + n + 0ℤ          ≡⟨ +-identityʳ (+ n) ⟩
+  + n               ∎
+  where open ≡-Reasoning
+fromINT-surjective (-[1+ n ]) .proj₂ {a INT.⊖ b} a+sn≡b = begin
+  a ⊖ b                     ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b                 ≡⟨ cong (λ z → + a - + z) a+sn≡b ⟨
+  + a - (+ a + + ℕ.suc n)   ≡⟨ cong (_+_ (+ a)) (neg-distrib-+ (+ a) (+ ℕ.suc n)) ⟩
+  + a + (- + a - + ℕ.suc n) ≡⟨ +-assoc (+ a) (- + a) (- + ℕ.suc n) ⟨
+  (+ a - + a) - + ℕ.suc n   ≡⟨ cong (_- + ℕ.suc n) (+-inverseʳ (+ a)) ⟩
+  0ℤ - + ℕ.suc n            ≡⟨ +-identityˡ (- + ℕ.suc n) ⟩
+  -[1+ n ]                  ∎
+  where open ≡-Reasoning
diff --git a/src/Data/Integer/IntConstruction/Tmp.agda b/src/Data/Integer/IntConstruction/Tmp.agda
new file mode 100644
index 0000000000..a585346618
--- /dev/null
+++ b/src/Data/Integer/IntConstruction/Tmp.agda
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- To be merged into Data.Integer.Base before merging!
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction.Tmp where
+
+open import Data.Integer.Base
+import Data.Integer.IntConstruction as INT
+import Data.Nat.Base as ℕ
+
+fromINT : INT.ℤ → ℤ
+fromINT (m INT.⊖ n) = m ⊖ n
+
+toINT : ℤ → INT.ℤ
+toINT (+ n) = n INT.⊖ 0
+toINT (-[1+ n ]) = 0 INT.⊖ ℕ.suc n
+
+-- here we have a choice:
+-- * either we can show the definitions in Data.Int.Base match those on INT under the above isomorphism;
+-- * or we could _redefine_ those operations _as_ the operations on INT under the above isormophism.

From 4092f7c3d62f7963dd1e2730ebddec8e12364c1c Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 24 Nov 2025 10:48:04 +0100
Subject: [PATCH 4/4] Relate nats and INT

---
 src/Data/Integer/IntConstruction.agda         | 13 ++++
 .../Integer/IntConstruction/Properties.agda   | 62 +++++++++++++++++++
 src/Data/Nat/Properties.agda                  |  4 ++
 3 files changed, 79 insertions(+)

diff --git a/src/Data/Integer/IntConstruction.agda b/src/Data/Integer/IntConstruction.agda
index 4ba9eba3b3..b9357536fb 100644
--- a/src/Data/Integer/IntConstruction.agda
+++ b/src/Data/Integer/IntConstruction.agda
@@ -21,6 +21,8 @@ record ℤ : Set where
     minuend : ℕ
     subtrahend : ℕ
 
+infix 4 _≃_ _≤_ _≥_ _<_ _>_
+
 _≃_ : Rel ℤ _
 (a ⊖ b) ≃ (c ⊖ d) = a ℕ.+ d ≡ c ℕ.+ b
 
@@ -42,15 +44,26 @@ _>_ = flip _<_
 1ℤ : ℤ
 1ℤ = 1 ⊖ 0
 
+infixl 6 _+_
 _+_ : ℤ → ℤ → ℤ
 (a ⊖ b) + (c ⊖ d) = (a ℕ.+ c) ⊖ (b ℕ.+ d)
 
+infixl 7 _*_
 _*_ : ℤ → ℤ → ℤ
 (a ⊖ b) * (c ⊖ d) = (a ℕ.* c ℕ.+ b ℕ.* d) ⊖ (a ℕ.* d ℕ.+ b ℕ.* c)
 
+infix 8 -_
 -_ : ℤ → ℤ
 - (a ⊖ b) = b ⊖ a
 
+infix 8 ⁻_ ⁺_
+
+⁺_ : ℕ → ℤ
+⁺ n = n ⊖ 0
+
+⁻_ : ℕ → ℤ
+⁻ n = 0 ⊖ n
+
 ∣_∣ : ℤ → ℕ
 ∣ a ⊖ b ∣ = ℕ.∣ a - b ∣′
 
diff --git a/src/Data/Integer/IntConstruction/Properties.agda b/src/Data/Integer/IntConstruction/Properties.agda
index c7bc946be9..ecc4ceae77 100644
--- a/src/Data/Integer/IntConstruction/Properties.agda
+++ b/src/Data/Integer/IntConstruction/Properties.agda
@@ -12,6 +12,7 @@ import Algebra.Properties.CommutativeSemigroup as CommSemigroupProps
 open import Data.Integer.IntConstruction
 open import Data.Nat.Base as ℕ using (ℕ)
 import Data.Nat.Properties as ℕ
+open import Data.Product.Base
 open import Function.Base
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
@@ -62,6 +63,9 @@ _≃?_ : Decidable _≃_
 ≤-refl : Reflexive _≤_
 ≤-refl = ℕ.≤-refl
 
+≤-reflexive : _≃_ ⇒ _≤_
+≤-reflexive = ℕ.≤-reflexive
+
 ≤-trans : Transitive _≤_
 ≤-trans {a ⊖ b} {c ⊖ d} {e ⊖ f} i≤j j≤k = ℕ.+-cancelʳ-≤ (d ℕ.+ c) (a ℕ.+ f) (e ℕ.+ b) $ trans-helper ℕ._≤_ a b c d e f (ℕ.+-mono-≤ i≤j j≤k)
 
@@ -253,3 +257,61 @@ _<?_ : Decidable _<_
 
 *-comm : Commutative _*_
 *-comm (a ⊖ b) (c ⊖ d) = cong₂ ℕ._+_ (cong₂ ℕ._+_ (ℕ.*-comm a c) (ℕ.*-comm b d)) (trans (ℕ.+-comm (c ℕ.* b) (d ℕ.* a)) (cong₂ ℕ._+_ (ℕ.*-comm d a) (ℕ.*-comm c b)))
+
+------------------------------------------------------------------------
+-- Properties of ⁺_
+
+⁺-cong : ∀ {m n} → m ≡ n → ⁺ m ≃ ⁺ n
+⁺-cong refl = refl
+
+⁺-injective : ∀ {m n} → ⁺ m ≃ ⁺ n → m ≡ n
+⁺-injective {m} {n} m+0≡n+0 = begin
+  m       ≡⟨ ℕ.+-identityʳ m ⟨
+  m ℕ.+ 0 ≡⟨ m+0≡n+0 ⟩
+  n ℕ.+ 0 ≡⟨ ℕ.+-identityʳ n ⟩
+  n       ∎
+  where open ≡-Reasoning
+
+⁺-mono-≤ : Monotonic₁ ℕ._≤_ _≤_ ⁺_
+⁺-mono-≤ = ℕ.+-monoˡ-≤ 0
+
+⁺-mono-< : Monotonic₁ ℕ._<_ _<_ ⁺_
+⁺-mono-< = ℕ.+-monoˡ-< 0
+
+⁺-+-homo : ∀ m n → ⁺ (m ℕ.+ n) ≃ ⁺ m + ⁺ n
+⁺-+-homo m n = refl
+
+⁺-0-homo : ⁺ 0 ≡ 0ℤ
+⁺-0-homo = refl
+
+⁺-*-homo : ∀ m n → ⁺ (m ℕ.* n) ≃ ⁺ m * ⁺ n
+⁺-*-homo m n = begin
+  m ℕ.* n ℕ.+ (m ℕ.* 0 ℕ.+ 0) ≡⟨ cong (m ℕ.* n ℕ.+_) (ℕ.+-identityʳ (m ℕ.* 0)) ⟩
+  m ℕ.* n ℕ.+ m ℕ.* 0         ≡⟨ cong (m ℕ.* n ℕ.+_) (ℕ.*-zeroʳ m) ⟩
+  m ℕ.* n ℕ.+ 0               ≡⟨ ℕ.+-identityʳ (m ℕ.* n ℕ.+ 0) ⟨
+  m ℕ.* n ℕ.+ 0 ℕ.+ 0         ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of ∣_∣
+
+∣∣-cong : ∀ {i j} → i ≃ j → ∣ i ∣ ≡ ∣ j ∣
+∣∣-cong {a ⊖ b} {c ⊖ d} a+d≡c+b = begin
+  ℕ.∣ a - b ∣′            ≡⟨ ℕ.∣-∣≡∣-∣′ a b ⟨
+  ℕ.∣ a - b ∣             ≡⟨ ℕ.∣m+o-n+o∣≡∣m-n∣ a b d ⟨
+  ℕ.∣ a ℕ.+ d - b ℕ.+ d ∣ ≡⟨ cong ℕ.∣_- b ℕ.+ d ∣ a+d≡c+b ⟩
+  ℕ.∣ c ℕ.+ b - b ℕ.+ d ∣ ≡⟨ cong ℕ.∣_- b ℕ.+ d ∣ (ℕ.+-comm c b) ⟩
+  ℕ.∣ b ℕ.+ c - b ℕ.+ d ∣ ≡⟨ ℕ.∣m+n-m+o∣≡∣n-o∣ b c d ⟩
+  ℕ.∣ c - d ∣             ≡⟨ ℕ.∣-∣≡∣-∣′ c d ⟩
+  ℕ.∣ c - d ∣′            ∎
+  where open ≡-Reasoning
+
+∣⁺_∣ : ∀ n → ∣ ⁺ n ∣ ≡ n
+∣⁺ n ∣ = refl
+
+∣⁻_∣ : ∀ n → ∣ ⁻ n ∣ ≡ n
+∣⁻ ℕ.zero ∣ = refl
+∣⁻ ℕ.suc n ∣ = refl
+
+∣∣-surjective : ∀ n → ∃[ i ] ∀ {j} → j ≃ i → ∣ j ∣ ≡ n
+∣∣-surjective n = ⁺ n , λ {j} j≃⁺n → trans (∣∣-cong {i = j} j≃⁺n) ∣⁺ n ∣
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index dc40f03132..9c5dd8ebc5 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1834,6 +1834,10 @@ m≤n⇒∣m-n∣≡n∸m {n = _}     (s≤s m≤n) = m≤n⇒∣m-n∣≡n∸m
 ∣m+n-m+o∣≡∣n-o∣ zero    n o = refl
 ∣m+n-m+o∣≡∣n-o∣ (suc m) n o = ∣m+n-m+o∣≡∣n-o∣ m n o
 
+∣m+o-n+o∣≡∣m-n∣ : ∀ m n o → ∣ m + o - n + o ∣ ≡ ∣ m - n ∣
+∣m+o-n+o∣≡∣m-n∣ m n zero = cong₂ ∣_-_∣ (+-identityʳ m) (+-identityʳ n)
+∣m+o-n+o∣≡∣m-n∣ m n (suc o) = trans (cong₂ ∣_-_∣ (+-suc m o) (+-suc n o)) (∣m+o-n+o∣≡∣m-n∣ m n o)
+
 m∸n≤∣m-n∣ : ∀ m n → m ∸ n ≤ ∣ m - n ∣
 m∸n≤∣m-n∣ m n with ≤-total m n
 ... | inj₁ m≤n = subst (_≤ ∣ m - n ∣) (sym (m≤n⇒m∸n≡0 m≤n)) z≤n