foundations.BasicTypes.md.

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

Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3

Investigations on graph-theoretical constructions in Homotopy type theory

Jonathan Prieto-Cubides j.w.w. HΓ₯kon Robbestad Gylterud

Department of Informatics

University of Bergen, Norway

{-# OPTIONS --without-K --exact-split #-}
module foundations.BasicTypes where
open import foundations.Type public

data
  𝟘 (β„“ : Level)
    : Type β„“
  where

βŠ₯     = 𝟘
Empty = 𝟘

exfalso
  : βˆ€ {ℓ₁ β„“β‚‚ : Level} {A : Type ℓ₁}
  ------------
  β†’ (βŠ₯ β„“β‚‚ β†’ A)

exfalso ()

Empty-elim = exfalso
βŠ₯-elim     = exfalso
𝟘-elim     = exfalso

infixr 50 Β¬_
Β¬_ : βˆ€ {β„“ : Level} β†’ Type β„“ β†’ Type β„“
Β¬_ {β„“} A = A β†’ βŠ₯ β„“

record
  πŸ™ (β„“ : Level)
    : Type β„“
  where
  constructor unit

Unit = πŸ™
⊀    = πŸ™

For the data constructor:

pattern β˜… = unit
pattern βˆ— = unit

unit-elim
  : βˆ€ {ℓ₁ β„“β‚‚ : Level} {A : Type β„“β‚‚}
  β†’ (a : A)
  ------------
  β†’ (πŸ™ ℓ₁  β†’ A)
unit-elim a βˆ— = a

data
  𝟚 (β„“ : Level)
    : Type (lsuc β„“)
  where
  πŸ˜β‚‚ : 𝟚 β„“
  πŸ™β‚‚ : 𝟚 β„“

Bool = 𝟚 lzero
false : 𝟚 lzero
false = πŸ˜β‚‚

true : 𝟚 lzero
true  = πŸ™β‚‚

ff = false
tt = true

-- data
--   β„• : Type lzero
--   where
--   zero : β„•
--   succ : β„• β†’ β„•

-- {-# BUILTIN NATURAL β„• #-} -- for importing cubical

open import Agda.Builtin.Nat
  renaming (Nat to β„•; suc to succ)
  hiding (_+_ ; _<_ ; _-_)
  public

Nat = β„•

-- record
--   Ξ£ {ℓ₁ β„“β‚‚ : Level}
--    (A : Type ℓ₁) (B : A β†’ Type β„“β‚‚)
--    -------------------------------
--    : Type (ℓ₁ βŠ” β„“β‚‚)
--   where
--   constructor _,_
--   field
--     π₁ : A
--     Ο€β‚‚ : B π₁

-- infixr 60 _,_
-- open Ξ£ public

open import Agda.Builtin.Sigma public
π₁ = fst
Ο€β‚‚ = snd

-- {-# BUILTIN SIGMA Ξ£ #-}

βˆ‘ = Ξ£ -- \Sigma and \sum

syntax βˆ‘ A (Ξ» a β†’ B) = βˆ‘[ a ∢ A ] B

Ξ£-s0 : βˆ€ {ℓ₁ β„“β‚‚} (A : Type ℓ₁) β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
Ξ£-s0 A = Ξ£ _
syntax Ξ£-s0 A (Ξ» x β†’ B) = Ξ£[ x ∢ A ] B

Ξ£-s1 : βˆ€ {ℓ₁ β„“β‚‚} {A : Type ℓ₁} β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
Ξ£-s1 = Ξ£ _
syntax Ξ£-s1 (Ξ» x β†’ B) = βˆ‘[ x ] B

Ξ£-s2 : βˆ€ {ℓ₁ β„“β‚‚} {A : Type ℓ₁} β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
Ξ£-s2 = Ξ£ _
syntax Ξ£-s2 (Ξ» x β†’ B) = Ξ£[ x ] B

proj₁ = π₁
projβ‚‚ = Ο€β‚‚
pr₁   = π₁
prβ‚‚   = Ο€β‚‚
#     =  π₁

∏
  : βˆ€ {ℓ₁ β„“β‚‚ : Level}
  β†’ (A : Type ℓ₁) (B : A β†’ Type β„“β‚‚)
  ---------------------------------
  β†’ Type (ℓ₁ βŠ” β„“β‚‚)

∏ A B = (x : A) β†’ B x

-- \prod vs \Pi
Π = ∏

syntax ∏ A (Ξ» a β†’ B) = ∏[ a ∢ A ] B

∏-s0 : βˆ€ {ℓ₁ β„“β‚‚} (A : Type ℓ₁) β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
∏-s0 A = ∏ _
syntax ∏-s0 A (Ξ» x β†’ B) = Ξ [ x ∢ A ] B

∏-s1 : βˆ€ {ℓ₁ β„“β‚‚} {A : Type ℓ₁} β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
∏-s1 = ∏ _
syntax ∏-s1 (Ξ» x β†’ B) = ∏[ x ] B

∏-s2 : βˆ€ {ℓ₁ β„“β‚‚} {A : Type ℓ₁} β†’ (A β†’ Type β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
∏-s2 = ∏ _
syntax ∏-s2 (Ξ» x β†’ B) = Ξ [ x ] B

_Γ—_
  : βˆ€ {ℓ₁ β„“β‚‚ : Level}
  β†’ (A : Type ℓ₁) (B : Type β„“β‚‚)
  -----------------------------
  β†’ Type (ℓ₁ βŠ” β„“β‚‚)

A Γ— B = βˆ‘ A (Ξ» _ β†’ B)

infixl  39 _Γ—_

data
  _+_ {ℓ₁ β„“β‚‚ : Level} (A : Type ℓ₁)(B : Type β„“β‚‚)
    : Type (ℓ₁ βŠ” β„“β‚‚)
  where
  inl : A β†’ A + B
  inr : B β†’ A + B

infixr 31 _+_

+-elim
  : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃ : Level}
  β†’ {A : Type ℓ₁}{B : Type β„“β‚‚} {C : Type ℓ₃}
  β†’ (A β†’ C) β†’ (B β†’ C)
  -------------------
  β†’ (A + B) β†’ C

+-elim A→C _  (inl x) = A→C x
+-elim _  B→C (inr x) = B→C x

cases = +-elim
syntax cases f g = ⟨ f + g ⟩

module _ {β„“ : Level}  where

  ⟦_βŸ§β‚‚ : β„• β†’ Type β„“
  ⟦_βŸ§β‚‚ zero      = 𝟘 _
  ⟦_βŸ§β‚‚ (succ n)  = πŸ™ β„“ + ⟦ n βŸ§β‚‚

  βŸ¦βŸ§β‚‚-succ
    : {n : β„•}
    β†’ ⟦ n βŸ§β‚‚ β†’ ⟦ succ n βŸ§β‚‚

  βŸ¦βŸ§β‚‚-succ {succ n} (inl x) = inr (inl unit)
  βŸ¦βŸ§β‚‚-succ {succ n} (inr x) = inr (βŸ¦βŸ§β‚‚-succ x)

  βŸ¦βŸ§β‚‚-pred
    : βˆ€ (n : β„•)
    β†’ ⟦ n βŸ§β‚‚ β†’ ⟦ n βŸ§β‚‚

  βŸ¦βŸ§β‚‚-pred (succ n) (inl x) = inl x
  βŸ¦βŸ§β‚‚-pred (succ n) (inr x) = inr (βŸ¦βŸ§β‚‚-pred n x)

-- data
--   _≑_ {β„“ : Level}{A : Type β„“} (a : A)
--     : A β†’ Type β„“
--   where
--   idp : a ≑ a

-- {-# BUILTIN EQUALITY _≑_  #-}

open import Agda.Builtin.Equality
  renaming (refl to idp )
  public

Eq   = _≑_
Id   = _≑_
Path = _≑_
_⇝_  = _≑_   -- type this '\r~'

_β‰ _ : βˆ€ {β„“}{A : Type β„“}(x y : A) β†’ Type β„“
x β‰  y = Β¬ (x ≑ y)

refl
  : βˆ€ {β„“ : Level} {A : Type β„“}
  β†’ (a : A)
  ---------
  β†’ a ≑ a

refl a = idp

sym
  : βˆ€ {β„“ : Level} {A : Type β„“} {x y : A}
  β†’ x ≑ y
  --------
  β†’ y ≑ x

sym idp = idp

syntax sym p = βˆ’ p

J
  : βˆ€ {β„“ : Level} {A : Type β„“} {a : A} {β„“β‚‚ : Level}
  β†’ (B : (a' : A) (p : a ≑ a') β†’ Type β„“β‚‚)
  β†’ (B a idp)
  ----------------------------------------
  β†’ ({a' : A} (p : a ≑ a') β†’ B a' p)

J _ b idp = b

data
  _β‡’_ {ℓ₁ β„“β‚‚ : Level}
    (A : Type ℓ₁) (B : Type β„“β‚‚)
    ---------------------------
    : Type (ℓ₁ βŠ” β„“β‚‚)
  where
  fun : (A β†’ B) β†’ A β‡’ B

_⇔_
  : βˆ€ {ℓ₁ β„“β‚‚}
  β†’ Type ℓ₁ β†’ Type β„“β‚‚
  -------------------
  β†’ Type (ℓ₁ βŠ” β„“β‚‚)

A ⇔ B = (A β†’ B) Γ— (B β†’ A)
_↔_ = _⇔_
infix 30 _↔_ _⇔_

data
  Dec {β„“ : Level}(P : Type β„“)
    : Type β„“
  where
  yes : ( p : P) β†’ Dec P
  no  : (Β¬p : P β†’ βŠ₯ β„“) β†’ Dec P

⌊_βŒ‹ : βˆ€ {β„“ : Level}{P : Type β„“} β†’ Dec P β†’ 𝟚 β„“
⌊ yes _ βŒ‹ = πŸ™β‚‚
⌊ no  _ βŒ‹ = πŸ˜β‚‚

Decidable
  : βˆ€ {ℓ₁ β„“β‚‚ β„“ : Level} {A : Type ℓ₁}{B : Type β„“β‚‚}
  β†’ (A β†’ B β†’ Type β„“)
  β†’ Type (ℓ₁ βŠ” β„“β‚‚ βŠ” β„“)

Decidable _∼_ = βˆ€ x y β†’ Dec (x ∼ y)

module β„•-ordering (β„“ : Level) where
  _<_ : β„• β†’ β„• β†’ Type β„“
  zero   < zero   = βŠ₯ _
  zero   < succ b = ⊀ _
  succ _ < zero   = βŠ₯ _
  succ a < succ b = a < b

  infixl -1 _<_

  bound : βˆ€ {k n : β„•} β†’ k < n β†’ β„•
  bound {n = n} _ = n

  _>_ : β„• β†’ β„• β†’ Type β„“
  a > b = b < a

  _≀_ : β„• β†’ β„• β†’ Type β„“
  a ≀ b = (a < b) + (a ≑ b)

  _β‰₯_ : β„• β†’ β„• β†’ Type β„“
  a β‰₯ b = (a > b) + (a ≑ b)

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