Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}
module foundations.TruncationType where
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.HLevelLemmas
open import foundations.HedbergLemmas

Propositional truncation (or reflection) is the universal solution to the problem of mapping (X) to a proposition (P):

Notes:

For a different way of formalising trucation see: .

module
  TruncationType
  where

private
  data
    !∥_∥ {ℓ} (A : Type ℓ)
      : Type ℓ
      where
      !∣_∣ : A → !∥ A ∥

∥_∥
  : ∀ {ℓ : Level} (A : Type ℓ)
  → Type ℓ

∥ A ∥ = !∥ A ∥

prop-trunc = ∥_∥

∣_∣
  : ∀ {ℓ : Level} {X : Type ℓ}
  ------------
  → X → ∥ X ∥

∣ x ∣ = !∣ x ∣

∥∥-intro = ∣_∣

Any two elements of the truncated type are equal

{: .axiom}

postulate trunc : ∀ {ℓ} {A : Type ℓ} → isProp ∥ A ∥

Recursion principle

trunc-rec
  :  ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{P : Type ℓ₂}
  → isProp P
  → (A → P)
  -----------
  → ∥ A ∥ → P

trunc-rec _ f !∣ x ∣ = f x

trunc-elim = trunc-rec
∥∥-rec     = trunc-rec

There exists the possibility to charactherize, propositional truncation using an impredicative approach, which means, our definition will lay on a larger universe as on the right-hand side in the following formulation.

[∥ X ∥ ⇔ ∏ (P : ), (P) → (X → P) → P]

Remarks:

truncated-is-prop
  : ∀ {ℓ : Level} {A : Type ℓ}
  → isProp (∥ A ∥)

truncated-is-prop = trunc

∥∥-is-prop    = truncated-is-prop
trunc-is-prop = truncated-is-prop

trunc-≃-prop
  : ∀ {ℓ : Level} {A : Type ℓ}
  → A is-prop
  -----------
  → ∥ A ∥ ≃ A

trunc-≃-prop pA = lemma333 trunc pA (trunc-rec pA id) ∣_∣

Using propositional truncation, we are able to define properly the logical disjunction and existence as follows.

_∨_
  : ∀ {ℓ₁ ℓ₂ : Level}
  → (p : hProp ℓ₁) (q : hProp ℓ₂)
  → Type (ℓ₁ ⊔ ℓ₂)
(P , _) ∨ (Q , _) = ∥ P + Q ∥

infix  _∨_

Conjunction is the product of two mere propositons.

_∧_
  : ∀ {ℓ₁ ℓ₂ : Level}
  → (p : hProp ℓ₁) (q : hProp ℓ₂)
  → Type (ℓ₁ ⊔ ℓ₂)

(P , _) ∧ (Q , _) = P × Q

infix   _∧_

∃[_]_
  : ∀ {ℓ : Level}
  → (T : Type ℓ) → (P : T → hProp ℓ)
  → Type ℓ

∃[ T ] P = ∥ ∑ T (λ x → π₁ (P x)) ∥

Another use of propositional truncation is to say a type (A) is non-empty. In this case, we have an element of (∥A∥)

_is-non-empty
  : ∀ {ℓ : Level}
  → (A : Type ℓ)
  → Type ℓ
A is-non-empty = ∥ A ∥

infixl  _is-non-empty

is-non-empty-is-prop
  : ∀ {ℓ : Level}{A : Type ℓ}
  → isProp (A is-non-empty)

is-non-empty-is-prop = ∥∥-is-prop

For any type (A) and a term (a : A), we shall say the connected commponent of (a) is all the terms in (A) ``connected’’ with (a).

connected-component
  : ∀ {ℓ : Level} {A : Type ℓ}
  → (a : A)
  → Type ℓ

connected-component {A = A} a = ∑ A (λ x → ∥ a ≡ x ∥ )

Consequently, two terms appear to be in the same component whenever there is an element in ∥ x ≡ y ∥.

_is-in-the-same-component-of_
  : ∀ {ℓ : Level}{A : Type ℓ}
  → (x y : A) → Type ℓ

x is-in-the-same-component-of y = ∥ x ≡ y ∥

infix  _is-in-the-same-component-of_

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

A is-connected =
    (A is-non-empty)
  × ((x y : A) → (x is-in-the-same-component-of y))

is-connected-is-prop
  : ∀ {ℓ : Level} {A : Type ℓ}
  ---------------------------
  → isProp (A is-connected)

is-connected-is-prop =
  ×-is-prop
    is-non-empty-is-prop
    (pi-is-prop (λ x → pi-is-prop λ y → trunc-is-prop))

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