Investigations on graph-theoretical constructions in Homotopy type theory

foundations.IntegerType.md.

Version of Sunday, January 22, 2023, 10:42 PM

{-# OPTIONS --without-K --exact-split #-} open import foundations.TransportLemmas open import foundations.EquivalenceType open import foundations.HomotopyType open import foundations.FunExtAxiom open import foundations.QuasiinverseType open import foundations.DecidableEquality open import foundations.NaturalsType open import foundations.HLevelTypes open import foundations.HedbergLemmas

module foundations.IntegerType where data ℤ : Type₀ where zer : ℤ pos : ℕ → ℤ neg : ℕ → ℤ -- Inclusion of the natural numbers into the integers NtoZ : ℕ → ℤ NtoZ zero = zer NtoZ (succ n ) = pos n -- Successor function zsucc : ℤ → ℤ zsucc zer = pos 0 zsucc (pos x ) = pos (succ x ) zsucc (neg zero ) = zer zsucc (neg (succ x )) = neg x -- Predecessor function zpred : ℤ → ℤ zpred zer = neg 0 zpred (pos zero ) = zer zpred (pos (succ x )) = pos x zpred (neg x ) = neg (succ x ) -- Successor and predecessor zsuccpred-id : (n : ℤ ) → zsucc (zpred n ) ≡ n zsuccpred-id zer = refl _ zsuccpred-id (pos zero ) = refl _ zsuccpred-id (pos (succ n )) = refl _ zsuccpred-id (neg n ) = refl _ zpredsucc-id : (n : ℤ ) → zpred (zsucc n ) ≡ n zpredsucc-id zer = refl _ zpredsucc-id (pos n ) = refl _ zpredsucc-id (neg zero ) = refl _ zpredsucc-id (neg (succ n )) = refl _ zpredsucc-succpred : (n : ℤ ) → zpred (zsucc n ) ≡ zsucc (zpred n ) zpredsucc-succpred zer = refl zer zpredsucc-succpred (pos zero ) = refl (pos zero ) zpredsucc-succpred (pos (succ x )) = refl (pos (succ x )) zpredsucc-succpred (neg zero ) = refl (neg zero ) zpredsucc-succpred (neg (succ x )) = refl (neg (succ x )) zsuccpred-predsucc : (n : ℤ ) → zsucc (zpred n ) ≡ zpred (zsucc n ) zsuccpred-predsucc n = inv (zpredsucc-succpred n ) -- Equivalence given by successor and predecessor zequiv-succ : ℤ ≃ ℤ zequiv-succ = qinv-≃ zsucc (zpred , (zsuccpred-id , zpredsucc-id )) -- Negation private - : ℤ → ℤ - zer = zer - (pos x ) = neg x - (neg x ) = pos x double- : (z : ℤ ) → - (- z ) ≡ z double- zer = refl _ double- (pos x ) = refl _ double- (neg x ) = refl _ zequiv- : ℤ ≃ ℤ zequiv- = qinv-≃ - (- , (double- , double-)) -- Addition on integers infixl 60 _+ᶻ_ _+ᶻ_ : ℤ → ℤ → ℤ zer +ᶻ m = m pos zero +ᶻ m = zsucc m pos (succ x ) +ᶻ m = zsucc (pos x +ᶻ m ) neg zero +ᶻ m = zpred m neg (succ x ) +ᶻ m = zpred (neg x +ᶻ m ) -- s on addition +ᶻ-lunit : (n : ℤ ) → n ≡ n +ᶻ zer +ᶻ-lunit zer = refl _ +ᶻ-lunit (pos zero ) = refl _ +ᶻ-lunit (pos (succ x )) = ap zsucc (+ᶻ-lunit (pos x )) +ᶻ-lunit (neg zero ) = refl _ +ᶻ-lunit (neg (succ x )) = ap zpred (+ᶻ-lunit (neg x )) +ᶻ-unit-zsucc : (n : ℤ ) → zsucc n ≡ (n +ᶻ pos zero ) +ᶻ-unit-zsucc zer = refl _ +ᶻ-unit-zsucc (pos zero ) = refl _ +ᶻ-unit-zsucc (pos (succ x )) = ap zsucc (+ᶻ-unit-zsucc (pos x )) +ᶻ-unit-zsucc (neg zero ) = refl _ +ᶻ-unit-zsucc (neg (succ x )) = inv (zpredsucc-id (neg x )) · ap zpred (+ᶻ-unit-zsucc (neg x )) +ᶻ-unit-zpred : (n : ℤ ) → zpred n ≡ (n +ᶻ neg zero ) +ᶻ-unit-zpred zer = refl _ +ᶻ-unit-zpred (pos zero ) = refl zer +ᶻ-unit-zpred (pos (succ x )) = inv (zsuccpred-id (pos x )) · ap zsucc (+ᶻ-unit-zpred (pos x )) +ᶻ-unit-zpred (neg zero ) = refl _ +ᶻ-unit-zpred (neg (succ x )) = ap zpred (+ᶻ-unit-zpred (neg x )) +ᶻ-pos-zsucc : (n : ℤ ) → (x : ℕ ) → zsucc (n +ᶻ pos x ) ≡ n +ᶻ pos (succ x ) +ᶻ-pos-zsucc zer x = refl _ +ᶻ-pos-zsucc (pos zero ) x = refl _ +ᶻ-pos-zsucc (pos (succ n )) x = ap zsucc (+ᶻ-pos-zsucc (pos n ) x ) +ᶻ-pos-zsucc (neg zero ) x = zsuccpred-id (pos x ) +ᶻ-pos-zsucc (neg (succ n )) x = zsuccpred-predsucc (neg n +ᶻ pos x ) · ap zpred (+ᶻ-pos-zsucc (neg n ) x ) +ᶻ-neg-zpred : (n : ℤ ) → (x : ℕ ) → zpred (n +ᶻ neg x ) ≡ n +ᶻ neg (succ x ) +ᶻ-neg-zpred zer x = refl _ +ᶻ-neg-zpred (pos zero ) x = zpredsucc-id (neg x ) +ᶻ-neg-zpred (pos (succ n )) x = zpredsucc-succpred (pos n +ᶻ neg x ) · ap zsucc (+ᶻ-neg-zpred (pos n ) x ) +ᶻ-neg-zpred (neg zero ) x = refl _ +ᶻ-neg-zpred (neg (succ n )) x = ap zpred (+ᶻ-neg-zpred (neg n ) x ) +ᶻ-comm : (n m : ℤ ) → n +ᶻ m ≡ m +ᶻ n +ᶻ-comm zer m = +ᶻ-lunit m +ᶻ-comm (pos zero ) m = +ᶻ-unit-zsucc m +ᶻ-comm (pos (succ x )) m = ap zsucc (+ᶻ-comm (pos x ) m ) · +ᶻ-pos-zsucc m x +ᶻ-comm (neg zero ) m = +ᶻ-unit-zpred m +ᶻ-comm (neg (succ x )) m = ap zpred (+ᶻ-comm (neg x ) m ) · +ᶻ-neg-zpred m x -- Decidable equality pos-inj : {n m : ℕ } → pos n ≡ pos m → n ≡ m pos-inj {n } {.n } idp = refl n neg-inj : {n m : ℕ } → neg n ≡ neg m → n ≡ m neg-inj {n } {.n } idp = refl n z-decEq : decEq ℤ z-decEq zer zer = inl (refl zer ) z-decEq zer (pos x ) = inr (λ ()) z-decEq zer (neg x ) = inr (λ ()) z-decEq (pos x ) zer = inr (λ ()) z-decEq (pos n ) (pos m ) with (nat-decEq n m ) z-decEq (pos n ) (pos m ) | inl p = inl (ap pos p ) z-decEq (pos n ) (pos m ) | inr f = inr (f ∘ pos-inj ) z-decEq (pos n ) (neg m ) = inr (λ ()) z-decEq (neg n ) zer = inr (λ ()) z-decEq (neg n ) (pos x₁ ) = inr (λ ()) z-decEq (neg n ) (neg m ) with (nat-decEq n m ) z-decEq (neg n ) (neg m ) | inl p = inl (ap neg p ) z-decEq (neg n ) (neg m ) | inr f = inr (f ∘ neg-inj ) z-isSet : isSet ℤ z-isSet = hedberg z-decEq -- Multiplication infixl 60 _*ᶻ_ _*ᶻ_ : ℤ → ℤ → ℤ zer *ᶻ m = zer pos zero *ᶻ m = m pos (succ x ) *ᶻ m = (pos x *ᶻ m ) +ᶻ m neg zero *ᶻ m = - m neg (succ x ) *ᶻ m = (neg x *ᶻ m ) +ᶻ (- m ) -- Ordering _<ᶻ_ : ℤ → ℤ → Type₀ zer <ᶻ zer = ⊥ lzero zer <ᶻ pos x = ⊤ lzero zer <ᶻ neg x = ⊥ lzero pos x <ᶻ zer = ⊥ lzero pos x <ᶻ pos y = x <ₙ y pos x <ᶻ neg y = ⊥ lzero neg x <ᶻ zer = ⊤ lzero neg x <ᶻ pos y = ⊤ lzero neg x <ᶻ neg y = y <ₙ x

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides