Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.NaturalsType where

open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.ProductIdentities
open import foundations.CoproductIdentities

open import foundations.HomotopyType
open import foundations.FunExtAxiom
open import foundations.QuasiinverseType
open import foundations.DecidableEquality
open import foundations.HLevelTypes
open import foundations.HedbergLemmas
open import  foundations.MonoidType

private
  code : ℕ → ℕ → Type₀
  code                 = ⊤ lzero
  code         (succ m) = ⊥ lzero
  code (succ n)         = ⊥ lzero
  code (succ n) (succ m) = code n m

crefl : (n : ℕ) → code n n
crefl zero     = ★
crefl (succ n) = crefl n

private
  encode : (n m : ℕ) → (n ≡ m) → code n m
  encode n m p = tr (code n) p (crefl n)

  decode : (n m : ℕ) → code n m → n ≡ m
  decode zero zero c = refl zero
  decode zero (succ m) ()
  decode (succ n) zero ()
  decode (succ n) (succ m) c = ap succ (decode n m c)

zero-not-succ
  : (n : ℕ)
  → ¬ (succ n ≡ zero)

zero-not-succ n = encode (succ n) 

The successor function is injective.

succ-inj
  : {n m : ℕ}
  → (succ n ≡ succ m)
  → n ≡ m

succ-inj {n} {m} p = decode n m (encode (succ n) (succ m) p)

+-inj
  : (k : ℕ) {n m : ℕ}
  → (k +ₙ n ≡ k +ₙ m)
  → n ≡ m

+-inj zero   p = p
+-inj (succ k) p = +-inj k (succ-inj p)

nat-decEq
  : decEq ℕ

nat-decEq zero zero = inl (refl zero)
nat-decEq zero (succ m) = inr (λ ())
nat-decEq (succ n) zero = inr (λ ())
nat-decEq (succ n) (succ m) with (nat-decEq n m)
nat-decEq (succ n) (succ m) | inl p = inl (ap succ p)
nat-decEq (succ n) (succ m) | inr f = inr λ p → f (succ-inj p)

natIsDec
  : (n m : ℕ)
  → (n ≡ m) + (¬ (n ≡ m))

natIsDec zero zero     = inl idp
natIsDec zero (succ m) = inr (λ ())
natIsDec (succ n) zero = inr (λ ())
natIsDec (succ n) (succ m) with natIsDec n m
... | inl p  = inl (ap succ p)
... | inr ¬p = inr λ sn=sm → ¬p (succ-inj sn=sm)

nat-is-set : isSet ℕ
nat-is-set = hedberg natIsDec

ℕ-is-set : isSet ℕ
ℕ-is-set = nat-is-set
nat-isSet = nat-is-set

ℕ-plus-monoid : Monoid
ℕ-plus-monoid = record
  { M = ℕ
  ; M-is-set = nat-isSet
  ; _⊕_     = plus
  ; e = zero
  ; l-unit = plus-lunit
  ; r-unit = plus-runit
  ; assoc = plus-assoc
  }

_<ₙ_ : ℕ → ℕ → Type₀
n <ₙ m = Σ ℕ (λ k → n +ₙ succ k ≡ m)

<-isProp
  : (n m : ℕ)
  → isProp (n <ₙ m)

<-isProp n m (k1 , p1) (k2 , p2) =
  Σ-bycomponents (succ-inj (+-inj n (p1 · inv p2)) , nat-isSet _ _ _ _)

module _ {ℓ : Level} where
  open ℕ-ordering ℓ
  succ-<-inj
    : ∀ {n m : ℕ}
    → succ n < succ m
    → n < m
  succ-<-inj {} {succ m} ∗ = ∗
  succ-<-inj {succ n} {succ m} p = succ-<-inj {n}{m} p

  _≤ₙ_ : ℕ → ℕ → Type ℓ
       ≤ₙ      = ⊤ ℓ
       ≤ₙ succ b = ⊤ ℓ
  succ a ≤ₙ      = ⊥ ℓ
  succ a ≤ₙ succ b = a ≤ₙ b

We can express the property of being the minimum of some given predicate as follows (See the symmetry book).

_is-the-minimum-of_
  : ∀ {ℓ : Level}
  → (n : ℕ )
  → (P : ℕ → hProp ℓ)
  → Type ℓ
n is-the-minimum-of P = π₁ (P n) × ((m : ℕ) → π₁ (P m) → n <ₙ (m +ₙ ))
  -- where open ℕ-< {level-of (π₁ (P n))}

_is-the-maximum-of_
  : {ℓ : Level}
  → (n : ℕ )
  → (P : ℕ → hProp ℓ)
  → Type ℓ

n is-the-maximum-of P = π₁ (P n) × ((m : ℕ) → π₁ (P m) →  (m +ₙ ) <ₙ n )

Move this somewhere else:

\texttt{agda(m\ +ₙ\ 1)\ Max\ :\ ∀\ \{ℓ\ :\ Level\}\ →\ (P\ :\ ℕ\ →\ hProp\ ℓ)\ →\ Type\ ℓ\ \ Max\ P\ =\ ∑\ ℕ\ (λ\ a\ →\ a\ is-the-maximum-of\ P)\ \textbackslash{}}

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