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.QuasiinverseType where
open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.HomotopyLemmas
open import foundations.HalfAdjointType

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

  qinv
    : (A → B)
    → Type (ℓ₁ ⊔ ℓ₂)

  qinv f = Σ (B → A) (λ g → ((f ∘ g) ∼ id) × ((g ∘ f) ∼ id))

  quasiinverse = qinv

  linv
    : (A → B)
    → Type (ℓ₁ ⊔ ℓ₂)

  linv f = Σ (B → A) (λ g → (g ∘ f) ∼ id-on A)

  left-inverse = linv

  rinv
    : (A → B)
    → Type (ℓ₁ ⊔ ℓ₂)

  rinv f = Σ (B → A) (λ g → (f ∘ g) ∼ id-on B)

  right-inverse = rinv

Biinverse is another equivalent notion of the right equivalence for HoTT.

  biinv : (A → B) → Type (ℓ₁ ⊔ ℓ₂)
  biinv f = linv f × rinv f

  biinverse  = biinv
  bi-inverse = biinv

A desire consequence (qinv → biinv):

  qinv-biinv : (f : A → B) → qinv f → biinv f
  qinv-biinv f (g , (u1 , u2)) = (g , u2) , (g , u1)

  biinv-qinv
    : (f : A → B)
    → biinv f → qinv f

  biinv-qinv f ((h , α) , (g , β)) = g , (β , δ)
    where
      γ1 : g ∼ ((h ∘ f) ∘ g)
      γ1 = rcomp-∼ g (h-sym (h ∘ f) id α)

      γ2 : ((h ∘ f) ∘ g) ∼ (h ∘ (f ∘ g))
      γ2 x = idp

      γ : g ∼ h
      γ = γ1 ● (γ2 ● (lcomp-∼ h β))

      δ : (g ∘ f) ∼ id
      δ = (rcomp-∼ f γ) ● α

  equiv-biinv
    : (f : A → B)
    → isContrMap f
    --------------
    → biinv f

  equiv-biinv f contrf =
    (remap eq , rlmap-inverse-h eq) , (remap eq , lrmap-inverse-h eq)
    where
      eq : A ≃ B
      eq = f , contrf

  qinv-ishae
    : {f : A → B}
    → qinv f
    ---------
    → ishae f

  qinv-ishae {f} (g , (ε , η)) = record {
      g = g ;
      η = η ;
      ε = λ b → inv (ε (f (g b))) · ap f (η (g b)) · ε b ;
      τ = τ
    }
    where
      aux-lemma : (a : A) → ap f (η (g (f a))) · ε (f a) ≡ ε (f (g (f a))) · ap f (η a)
      aux-lemma a =
        begin
          ap f (η ((g ∘ f) a)) · ε (f a)
            ≡⟨ ap (λ u → ap f u · ε (f a)) (h-naturality-id η) ⟩
          ap f (ap (g ∘ f) (η a)) · ε (f a)
            ≡⟨ ap (_· ε (f a)) (ap-comp (g ∘ f) f (η a)) ⟩
          ap (f ∘ (g ∘ f)) (η a) · ε (f a)
            ≡⟨ inv (h-naturality (λ x → ε (f x)) (η a)) ⟩
          ε (f (g (f a))) · ap f (η a)
        ∎

      τ : (a : A) → ap f (η a) ≡ (inv (ε (f (g (f a)))) · ap f (η (g (f a))) · ε (f a))
      τ a =
        begin
          ap f (η a)
            ≡⟨ ap (_· ap f (η a)) (inv (·-linv (ε (f (g (f a)))))) ⟩
          inv (ε (f (g (f a)))) · ε (f (g (f a))) · ap f (η a)
            ≡⟨ ·-assoc (inv (ε (f (g (f a))))) _ (ap f (η a)) ⟩
          inv (ε (f (g (f a)))) · (ε (f (g (f a))) · ap f (η a))
            ≡⟨ ap (inv (ε (f (g (f a)))) ·_) (inv (aux-lemma a)) ⟩
          inv (ε (f (g (f a)))) · (ap f (η (g (f a))) · ε (f a))
            ≡⟨ inv (·-assoc (inv (ε (f (g (f a))))) _ (ε (f a))) ⟩
          inv (ε (f (g (f a)))) · ap f (η (g (f a))) · ε (f a)
        ∎

Quasiinverses create equivalences.

  qinv-≃
    : (f : A → B)
    → qinv f
    -------------
    → A ≃ B

  qinv-≃ f = ishae-≃ ∘ qinv-ishae

  quasiinverse-to-≃ = qinv-≃

  ≃-qinv
    : A ≃ B
    ----------------
    → Σ (A → B) qinv

  ≃-qinv eq =
    lemap eq , (remap eq , (lrmap-inverse-h eq , rlmap-inverse-h eq))

  ≃-to-quasiinverse = ≃-qinv

Half-adjoint equivalences are quasiinverses.

  ishae-qinv
    : {f : A → B}
    → ishae f
    ---------
    → qinv f

  ishae-qinv {f} (hae g η ε τ) = g , (ε , η)

  ≃-ishae
    : (e : A ≃ B)
    --------------
    → ishae (e ∙→)

  ≃-ishae e = qinv-ishae (π₂ (≃-qinv e))

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