Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.UnivalenceLemmas where
open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.FunExtAxiom

open import foundations.EquivalenceType
open import foundations.QuasiinverseType
open import foundations.QuasiinverseLemmas
open import foundations.UnivalenceAxiom
open import foundations.UnivalenceTransport
open import foundations.UnivalenceIdEquiv
open import foundations.HLevelLemmas

abstract
  ua-comp
    : ∀ {ℓ : Level} {A B C : Type ℓ}
    → (α : A ≃ B)
    → (β : B ≃ C)
    ---------------------------------
    → ua (α :>≃ β) ≡ (ua α) · (ua β)

  ua-comp α β  =
    begin
      ua (α :>≃ β)
        ≡⟨ ap ua (:>≃-ite-ua α β) ⟩
      ua (ite (ua α · ua β))
        ≡⟨ ua-η ((ua α) · (ua β)) ⟩
      (ua α) · (ua β)
    ∎

ua-inv-r
  : ∀ {ℓ : Level} {A B : Type ℓ}
  → (α : A ≃ B)
  -------------------------------
  → ua α · ua (≃-sym α) ≡ refl A

ua-inv-r {A = A}{B} α =
  begin
    ua α · ua (≃-sym α)
      ≡⟨ ! ua-comp {A = A}{B}{A} α (≃-sym α) ⟩
    ua (α :>≃ (≃-sym α))
      ≡⟨ ap ua (sameEqv (ap π₁ (≃-trans-inv α))) ⟩
    ua idEqv
      ≡⟨ ua-id ⟩
    refl A
  ∎

ua-inv
  : ∀ {ℓ : Level} {A B : Type ℓ}
  → (α : A ≃ B)
  -------------------------
  → ua (≃-sym α) ≡ ! (ua α)

ua-inv α =
  begin
    ua (≃-sym α)
      ≡⟨ ap (_· ua (≃-sym α)) (! (·-linv (ua α))) ⟩
    ! (ua α) · ua α · ua (≃-sym α)
      ≡⟨ ·-assoc (! (ua α)) _ _ ⟩
    ! (ua α) · (ua α · ua (≃-sym α))
      ≡⟨ ap (! (ua α) ·_) (ua-inv-r α) ⟩
    ! (ua α) · refl _
      ≡⟨ ! (·-runit (! ((ua α)))) ⟩
    ! (ua α)
  ∎

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