Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.HLevelTypes where

open import foundations.BasicTypes
open import foundations.BasicFunctions
open import foundations.Transport

Higher levels of the homotopical structure:

A type is a type such that element is equal to a point, the of contraction.

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

isContr A = Σ A (λ a → ((x : A) → a ≡ x))

Contractible = isContr
is-singleton = isContr
isSingleton  = isContr
_is-contr    = isContr

center-of
  : ∀ {ℓ : Level}
  → {A : Type ℓ}
  → A is-contr
  → A
center-of (a , _) = a

contr-connects
  : ∀ {ℓ : Level} {A : Type ℓ}
  → A is-contr
  ----------------------
  → (a a' : A) → a ≡ a'

contr-connects (c₁ , f) c₂ x = ! (f c₂) · (f x)

isProp
  : ∀ {ℓ : Level} (A : Type ℓ) → Type ℓ

isProp A = ((x y : A) → x ≡ y)

More syntax:

is-subsingleton = isProp
isSubsingleton  = isProp
_is-prop         = isProp

Let’s stop a bit. So, these propositios, also named ``mere’’ propositions tell us: in a proposition, its elements are connected with each other. Subsinglenton (which is, subset of a singlenton (a unit point set)) is empty or it has the element. Propositions can be seen as equivalent to 𝟘 or 𝟙.

Therefore, we will find a theorem later that says ``if A is a proposition, and it’s inhabited then it’s contractible’’, and it makes sense perfectly.

hProp
  : ∀ (ℓ : Level) → Type (lsuc ℓ)

hProp ℓ = ∑ (Type ℓ) isProp

In practice, we might want to say a type holds certain property and then we can use the convenient following predicate.

_has-property_
  : ∀ {ℓ : Level}
  → (A : Type ℓ)
  → (P : Type ℓ → hProp ℓ)
  → Type ℓ

A has-property P = π₁ (P A)

_holds-property = _has-property_

_has-fun-property_
  : ∀ {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁}{Y : Type ℓ₂}
  → (f : X → Y)
  → (P : ∀ {X : Type ℓ₁}{Y : Type ℓ₂} → (X → Y) → hProp (ℓ₁ ⊔ ℓ₂))
  → Type (ℓ₁ ⊔ ℓ₂)

f has-fun-property P = π₁ (P f)

_has-endo-property_
  : ∀ {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁}
  → (f : X → X)
  → (P : ∀ {X : Type ℓ₁} → (X → X) → hProp ℓ₂)
  → Type ℓ₂

f has-endo-property P = π₁ (P f)

Additionally, we may need to say, more explicity that two type share any property whenever they are equivalent. Recall, these types do not need to be in the same universe, however, for simplicity and to avoid dealing with lifting types, we’ll assume they live in the same universe. Also, we require a path, instead of the equivalence because at this point, we have not define yet its type.

_has-all-properties-of_because-of-≡_
    : ∀ {ℓ : Level}
    → (A : Type ℓ)
    → (B : Type ℓ)
    → A ≡ B
    -------------------------------------
    → (P : Type ℓ → hProp ℓ)
    → B has-property P → A has-property P

A has-all-properties-of B because-of-≡ path
  = λ P BholdsP → tr (_has-property P) (! path) BholdsP

Now with (homotopy) propositional, we can consider the notion of subtype, which is, just the ∑-type about the collection of terms that holds some given property, we can use the following type for a proposition (P : A → U) for some type (A). Assuming at least there

subtype
  : ∀ {ℓ : Level} {A : Type ℓ}
  → (P : A → hProp ℓ)
  → Type ℓ

subtype P = ∑ (domain P) (π₁ ∘ P)

We prove now that the basic type (⊥, ⊤) are indeed (mere) propositions:

⊥-is-prop : ∀ {ℓ : Level} →  isProp (⊥ ℓ)
⊥-is-prop ()

⊤-is-prop : ∀ {ℓ : Level} →  isProp (⊤ ℓ)
⊤-is-prop _ _ = idp

More syntax:

𝟘-is-prop = ⊥-is-prop
𝟙-is-prop = ⊤-is-prop

A type is a dimensional structure*, all parallel paths are homotopic and the homotopy is given by a continuous function on the two paths.

isSet
  : ∀ {ℓ : Level} → Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

More syntax:

_is-set = isSet

The type of sets

hSet
  :  ∀ (ℓ : Level) → Type (lsuc ℓ)

hSet ℓ = ∑ (Type ℓ) isSet

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

isGroupoid A  = (a₀ a₁ : A) → isSet (a₀ ≡ a₁)

More syntax:

_is-groupoid = isGroupoid

Groupoid
  : ∀ (ℓ : Level) → Type (lsuc ℓ)

Groupoid ℓ = ∑ (Type ℓ) isGroupoid

And, in case, we go a bit further, we have 2-groupoids. We can continue define more h-levels for all natural numbers, however, we are not going to use them.

is-2-Groupoid
   : ∀ {ℓ : Level} → Type ℓ → Type ℓ

is-2-Groupoid A  = (a₀ a₁ : A) → isGroupoid (a₀ ≡ a₁)

is-2-groupoid = is-2-Groupoid

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