Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.BasicFunctions where
open import foundations.BasicTypes public

_·_
  : ∀ {ℓ : Level} {A : Type ℓ}  {x y z : A}
  → (p : x ≡ y)
  → (q : y ≡ z)
  --------------
  → x ≡ z

_·_ idp q = q

infixl  _·_

_⁻¹
  : ∀ {ℓ : Level} {A : Type ℓ}  {a b : A}
  → a ≡ b
  --------
  → b ≡ a

idp ⁻¹ = idp
inv = _⁻¹
!_  = inv
infixl  _⁻¹ !_

id
  : ∀ {ℓ : Level} {A : Type ℓ}
  ----------------
  → A → A

id = λ x → x

identity = id

id-on
  : ∀ {ℓ : Level} (A : Type ℓ)
  ---------------
  → (A → A)

id-on A = λ x → x

constant-function
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → (b : B)
  ---------
  → (A → B)

constant-function b = λ _ → b

¬¬ ¬¬¬
  : ∀ {ℓ : Level}
  → Type ℓ
  → Type ℓ

¬¬ A  = ¬(¬ A)
¬¬¬ A = ¬(¬¬ A)

neg¬
  : Bool
  → Bool

neg¬ tt = ff

contrapositive
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level}{A : Type ℓ₁}{B : Type ℓ₂}
  → (A → B)
  → ((B → ⊥ ℓ₃) → (A → ⊥ ℓ₃))

contrapositive f v a = v (f a)

_∘_
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (a : A) → (B a → Type ℓ₃)}
  → (g : {a : A} → ∏ (B a) (C a))
  → (f : ∏ A B)
  -------------------------------
  → ∏ A (λ a → C a (f a))

g ∘ f = λ x → g (f x)

infixr  _∘_

Synonym for composition (diagrammatic version)

_:>_ _︔_
   : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (a : A) → (B a → Type ℓ₃)}
  → (f : Π A B)
  → (g : {a : A} → Π (B a) (C a))
  -------------------------------
  → Π A (λ a → C a (f a))

f :> g = g ∘ f

_︔_ = _:>_

infixr  _:>_
infixr  _︔_

domain
  : ∀ {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁}{B : Type ℓ₂}
  → (A → B)
  → Type ℓ₁

domain {A = A} _ = A

codomain
  : ∀ {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁}{B : Type ℓ₂}
  → (A → B)
  → Type ℓ₂

codomain {B = B} _ = B

type-of
  : ∀ {ℓ : Level}{X : Type ℓ}
  → X → Type ℓ

type-of {X = X} _ = X

level-of
  : ∀ {ℓ : Level}
  → (A : Type ℓ)
  → Level

level-of {ℓ} A = ℓ

∘-lassoc
  : ∀ {ℓ : Level} {A B C D : Type ℓ}
  → (h : C → D) → (g : B → C) → (f : A → B)
  -----------------------------------------
  → (h ∘ (g ∘ f)) ≡ ((h ∘ g) ∘ f)

∘-lassoc h g f = refl (λ x → h (g (f x)))

∘-rassoc
  : ∀ {ℓ : Level} {A B C D : Type ℓ}
  → (h : C → D) → (g : B → C) → (f : A → B)
  -----------------------------------------
  → ((h ∘ g) ∘ f) ≡ (h ∘ (g ∘ f))

∘-rassoc h g f = sym (∘-lassoc h g f)

:>-lassoc
  : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}{D : Type ℓ₄}
  → (f : A → B) → (g : B → C) → (h : C → D)
  -----------------------------------------
  → (f :> (g :> h)) ≡ ((f :> g) :> h)

:>-lassoc f g h = idp

:>-rassoc
  : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}{D : Type ℓ₄}
  → (f : A → B) → (g : B → C) → (h : C → D)
  -----------------------------------------
  → ((f :> g) :>  h) ≡ (f :> (g :> h))

:>-rassoc f g h = sym (:>-lassoc f g h)

_←_ : ∀ {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : Type ℓ₂) → Type (ℓ₁ ⊔ ℓ₂)
B ← A = A → B

_$_
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
  → (∀ (x : A) → B x)
  -------------
  → (∀ (x : A) → B x)

f $ x = f x

infixr  _$_

plus _+ₙ_ : ℕ → ℕ → ℕ
plus zero     y = y
plus (succ x) y = succ (plus x y)

infixl  _+ₙ_
_+ₙ_ = plus

plus' _+ℕ_ : ℕ → ℕ → ℕ
plus' x zero = x
plus' x (succ y) = succ (plus' x y)
_+ℕ_ = plus'

max : ℕ → ℕ → ℕ
max         n = n
max (succ n)  = succ n
max (succ n) (succ m) = succ (max n m)

min : ℕ → ℕ → ℕ
min         n = 
min (succ n)  = 
min (succ n) (succ m) = succ (min n m)

Now, we prove some lemmas about natural number addition are the following. Notice in the proofs, the extensive usage of rewriting, because at this point we have not showed that the equality type is a congruent relation.

plus-lunit
  :  (n : ℕ)
  ----------------
  → zero +ₙ n ≡ n

plus-lunit n = refl n

plus-runit
  : (n : ℕ)
  ----------------
  → n +ₙ zero ≡ n

plus-runit zero     = refl zero
plus-runit (succ n) rewrite (plus-runit n) = idp

plus-succ
  :  (n m : ℕ)
  ----------------------------------
  → succ (n +ₙ m) ≡ (n +ₙ (succ m))

plus-succ zero     m = refl (succ m)
plus-succ (succ n) m rewrite (plus-succ n m) = idp

plus-succ-rs
  : (n m o p : ℕ)
  →        n +ₙ m ≡ o +ₙ p
  --------------------------------
  → n +ₙ (succ m) ≡ o +ₙ (succ p)

plus-succ-rs  m  p α rewrite α = idp
plus-succ-rs  m (succ o) p α rewrite α | plus-succ o p = idp
plus-succ-rs (succ n) m  p α rewrite α | ! (plus-succ n m) | α = idp
plus-succ-rs (succ n) m (succ o) p α rewrite ! α | ! (plus-succ n m) | plus-succ o p | α = idp
-- other solution, just : ! (plus-succ n m) · ap succ α · (plus-succ o p)

Commutativity

plus-comm
  : (n m : ℕ)
  -----------------
  → n +ₙ m ≡ m +ₙ n

plus-comm zero     m = inv (plus-runit m)
plus-comm (succ n) m rewrite (plus-comm n m)  = plus-succ m n

Associativity

plus-assoc
  : (n m p : ℕ)
  ---------------------------------
  → n +ₙ (m +ₙ p) ≡ (n +ₙ m) +ₙ p

plus-assoc zero     m p = refl (m +ₙ p)
plus-assoc (succ n) m p  rewrite (plus-assoc n m p) = idp

Coproduct manipulation

+-map
  : ∀ {i j k l : Level} {A : Type i} {B : Type j} {A' : Type k} {B' : Type l}
  → (A → A')
  → (B → B')
  → A + B → A' + B'

+-map f g = cases (f :> inl) (g :> inr)

syntax +-map f g = 〈 f ⊕ g 〉

parallell
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (a : A) → (B a → Type ℓ₃)}
  → (f : (a : A) → B a)
  → ((a : A) → C a (f a))
  -------------------------
  → (a : A) → ∑ (B a) (C a)

parallell f g a = (f a , g a)

syntax parallell f g = 〈 f × g 〉

Curryfication

curry
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}  {C : Σ A B → Type ℓ₃}
  → ((s : ∑ A B) → C s)
  -------------------------------
  → ((x : A)(y : B x) → C (x , y))

curry f x y = f (x , y)

Uncurryfication

unCurry
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂} {C : Type ℓ₃}
  → (D : (a : A) → B a → C)
  ------------------------
  → (p : ∑ A B) → C

unCurry D p = D (proj₁ p) (proj₂ p)

uncurry
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : (a : A) → (B a → Type ℓ₃)}
  → (f : (a : A) (b : B a) → C a b)
  ---------------------------------
  → (p : ∑ A B) → C (π₁ p) (π₂ p)

uncurry f (x , y) = f x y

Coproducts functions

inr-is-injective
  : ∀ {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁}{B : Type ℓ₂} {b₁ b₂ : B}
  → inr {A = A}{B} b₁ ≡ inr b₂
  ----------------------------
  → b₁ ≡ b₂

inr-is-injective idp = idp

inl-is-injective
  : ∀ {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁}{B : Type ℓ₂} {a₁ a₂ : A}
  → inl {A = A}{B} a₁ ≡ inl a₂
  ----------------------------
  → a₁ ≡ a₂

inl-is-injective idp = idp

Equational reasoning

Equational reasoning is a way to write readable chains of equalities.

module _ {ℓ : Level} {A : Type ℓ} where

  _≡⟨⟩_
    : ∀ (x {y} : A)
    -----------------
    → x ≡ y → x ≡ y

  _ ≡⟨⟩ p = p

  infixr  _≡⟨⟩_

  _≡⟨_⟩_
    : (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
    --------
    → x ≡ z

  _ ≡⟨ thm ⟩ q = thm · q
  infixr  _≡⟨_⟩_ _≡⟨_⟩_

Q.E.D:

  _∎
    : (x : A)
    → x ≡ x

  _∎ = λ x → idp

  infix  _∎

  begin_
    : {x y : A}
    → x ≡ y
    → x ≡ y

  begin_ p = p

  infix  begin_

Finite iteration of a function

For any endo-function in (A), (f: A A), the following function iterates (n) times (f)

[ f^{n+1}(x) = f (f^{n} (x)) ]

infixl  _^_
_^_
  : ∀ {ℓ : Level} {A : Type ℓ}
  → (f : A → A) → (n : ℕ)
  -----------------------
  → (A → A)

f ^  = id
f ^ succ n = λ x → f ((f ^ n) x)

ap
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → (f : A → B) {a₁ a₂ : A}
  → a₁ ≡ a₂
  --------------
  → f a₁ ≡ f a₂

ap f idp = idp

More syntax:

cong  = ap
app-≡ = ap

syntax app-≡ f p = f [[ p ]]

We can define a convenient syntax sugar for ap in equational reasoning.

infixl  ap
syntax ap f p = p |in-ctx f

app-comm
  : ∀ {ℓ : Level}{A : Type ℓ}
  → (f : A → A) → (n : ℕ)
  → (x : A)
  ---------------------------------
  → (f ((f ^ n) x) ≡ ((f ^ n) (f x)))

app-comm f  x = idp
app-comm f (succ n) x rewrite app-comm f n x = idp

app-comm₂
  : ∀ {ℓ : Level}{A : Type ℓ}
  → (f : A → A)
  → (n k : ℕ)
  → (x : A)
  ------------------------------------------
  → ((f ^ (n +ₙ k)) x) ≡ (f ^ n) ((f ^ k) x)

app-comm₂ f   x = idp
app-comm₂ f  (succ k) x = idp
app-comm₂ f (succ n)  x rewrite plus-runit n  = idp
app-comm₂ f (succ n) (succ k) x rewrite app-comm₂ f n (succ k) x = idp

app-comm₃
  : ∀ {ℓ : Level}{A : Type ℓ}
  → (f : A → A)
  → (k n : ℕ)
  → (x : A)
  ------------------------------------------
  → (f ^ k) ((f ^ n) x) ≡ (f ^ n) ((f ^ k) x)

app-comm₃ f k  x          = idp
app-comm₃ f k n@(succ _) x =
   begin
      (f ^ k) ((f ^ n) x)
      ≡⟨ ! (app-comm₂ f k n x) ⟩
      (f ^ (k +ₙ n)) x
      ≡⟨ ap (λ p → (f ^ p) x) (plus-comm k n) ⟩
      (f ^ (n +ₙ k)) x
      ≡⟨ app-comm₂ f n k x ⟩
      (f ^ n) ((f ^ k) 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