Investigations on graph-theoretical constructions in Homotopy type theory

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

Two functions are quasi-inverses if we can construct a function providing and for any given and .

module foundations.QuasiinverseLemmas where

open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.HomotopyLemmas


open import foundations.QuasiinverseType

module QuasiinverseLemmas where

The equivalence types are indeed equivalence

qinv-comp
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
  → Σ (A → B) qinv
  → Σ (B → C) qinv
  ----------------
  → Σ (A → C) qinv

qinv-comp (f , (if , (εf , ηf))) (g , (ig , (εg , ηg))) = (g ∘ f) , ((if ∘ ig) ,
   ( (λ x → ap g (εf (ig x)) · εg x)
   ,  λ x → ap if (ηg (f x)) · ηf x))

qinv-inv
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → Σ (A → B) qinv
  ----------------
  → Σ (B → A) qinv

qinv-inv (f , (g , (ε , η))) = g , (f , (η , ε))

Equivalence types are equivalence relations.

idEqv
  : ∀ {ℓ} {A : Type ℓ}
  -------
  → A ≃ A

idEqv = id , λ a → (a , refl a) , λ { (_ , idp) → refl (a , refl a) }

More syntax:

≃-refl = idEqv
A≃A    = idEqv

_:>≃_ ≃-trans
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
  → A ≃ B
  → B ≃ C
  -------
  → A ≃ C

_:>≃_ {A = A} {C = C} eq-f eq-g = qinv-≃ (π₁ qcomp) (π₂ qcomp)
 where
   qcomp : Σ (A → C) qinv
   qcomp = qinv-comp (≃-qinv eq-f) (≃-qinv eq-g)

More syntax:

compEqv = _:>≃_
≃-trans = _:>≃_

≃-sym
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → A ≃ B
  -------
  → B ≃ A

≃-sym {ℓ}{_} {A} {B} eq-f = qinv-≃ (π₁ qcinv) (π₂ qcinv)
 where
   qcinv : Σ (B → A) qinv
   qcinv = qinv-inv (≃-qinv eq-f)

More syntax:

invEqv = ≃-sym
≃-flip = ≃-sym

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