Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.EquivalenceType where

There are three definitions to say a function is an equivalence. All these definitions are required to be mere propositions and to hold the bi-implication of begin . We show this clearly in what follows. Nevertheless, we want to get the following fact:

open import foundations.BasicTypes
open import foundations.HLevelTypes
open import foundations.FibreType

open import foundations.Transport
open import foundations.HomotopyType

[(f) (f) (f).]

A map is if the fiber in any point is contractible, that is, each element has a unique preimagen.

isContrMap
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → (f : A → B)
  → Type (ℓ₁ ⊔ ℓ₂)

isContrMap {B = B} f = (b : B) → isContr (fib f b)

Synomyns:

map-contractible = isContrMap
_is-contr-map    = isContrMap

There exists an equivalence between two types if there exists a contractible function between them.

isEquiv
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → (f : A → B)
  → Type (ℓ₁ ⊔ ℓ₂)

isEquiv f = isContrMap f

Synomyms:

isEquivalence   = isEquiv
_is-equivalence = isEquiv
_is-equiv       = isEquiv

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

A ≃ B = Σ (A → B) isEquiv

module _ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}  where

  lemap ≃-to-→ fun≃ _∙ _∙→ apply
    : A ≃ B
    -------
    → (A → B)

  lemap = π₁

More syntax:

  ≃-to-→ = lemap
  fun≃   = lemap
  _∙     = lemap
  _∙→    = lemap
  apply  = lemap

  infixl  _∙ _∙→

  remap ≃-to-← invfun≃ _∙← rapply
    : A ≃ B
    ---------
    → (B → A)

  remap (f , contrf) b = π₁ (π₁ (contrf b))

  ≃-to-←  = remap
  invfun≃ = remap
  _∙←     = remap
  rapply  = remap

  infixl  _∙←

The maps of an equivalence are inverses in particular

  lrmap-inverse ∙→∘∙←
    : (e : A ≃ B) → {b : B}
    -----------------------
    → (e ∙→) ((e ∙←) b) ≡ b
  lrmap-inverse (f , eqf) {b} = fib-eq (π₁ (eqf b))
  ∙→∘∙← = lrmap-inverse

  rlmap-inverse ∙←∘∙→
    : (e : A ≃ B) → {a : A}
    ------------------------
    → (e ∙←) ((e ∙→) a) ≡ a
  rlmap-inverse (f , eqf) {a} = ap π₁ ((π₂ (eqf (f a))) fib-image)
  ∙←∘∙→ = rlmap-inverse

  lrmap-inverse-h  ∙→∘∙←-h
    : (e : A ≃ B)
    ------------------------
    → ((e ∙→) ∘ (e ∙←)) ∼ id
  lrmap-inverse-h e = λ x → lrmap-inverse e {x}
  ∙→∘∙←-h = lrmap-inverse-h

  rlmap-inverse-h ∙←∘∙→-h
    : (e : A ≃ B)
    ------------------------
    → ((e ∙←) ∘ (e ∙→)) ∼ id
  rlmap-inverse-h e = λ x → rlmap-inverse e {x}
  ∙←∘∙→-h = rlmap-inverse-h

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