Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.UnivalenceTransport where

open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.FunExtAxiom
open import foundations.QuasiinverseType
open import foundations.QuasiinverseLemmas

open import foundations.UnivalenceAxiom

transport-family-ap
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
  → (B : A → Type ℓ₂)
  → {x y : A}
  → (p : x ≡ y)
  → (u : B x)
  ---------------------------------------------------
  → tr B p u ≡ tr (λ X → X) (ap B p) u

transport-family-ap B idp u = idp

transport-family-idtoeqv
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
  → (B : A → Type ℓ₂)
  → {x y : A}
  → (p : x ≡ y)
  → (u : B x)
  ----------------------------------------------
  → tr B p u ≡ fun≃ (idtoeqv (ap B p)) u

transport-family-idtoeqv B idp u = idp

:

transport-ua
     : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
     → (B : A → Type ℓ₂)
     → {x y : A}
     → (p : x ≡ y)
     → (e : B x ≃ B y)
     → ap B p ≡ ua e
     -----------------
     → (u : B x) → tr B p u ≡ (fun≃ e) u

transport-ua B idp e q u =
     begin
       tr B idp u
         ≡⟨ transport-family-idtoeqv B idp u ⟩
       fun≃ (idtoeqv (ap B idp)) u
         ≡⟨ ap (λ r → fun≃ (idtoeqv r) u) q ⟩
       fun≃ (idtoeqv (ua e)) u
         ≡⟨ ap (λ r → fun≃ r u) (ua-β e) ⟩
       fun≃ e u
     ∎

funext-transport-ua
   : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
   → (B : A → Type ℓ₂)
   → {x y : A}
   → (p : x ≡ y)
   → (e : B x ≃ B y)
   → ap B p ≡ ua e
   -----------------
   → tr B p ≡ (fun≃ e)

funext-transport-ua B p e x₁ = funext (transport-ua B p e x₁)

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

 abstract
   coe-ua
     : (α : A ≃ B)
     -------------------------------------
     → (∀ x → (coe (ua α) x) ≡ ((α ∙) x))

   coe-ua α = happly (ap (lemap) (ua-β α))

   coe-!-ua
     : (α : A ≃ B)
     -------------------------------------
     → (∀ x → (coe (! ua α) x) ≡ ((rapply α ) x))

   coe-!-ua α = happly (ap (remap) (ua-β α))

   coe-ua-·
     : {C : Type ℓ}
     → (α : A ≃ B)
     → (β : B ≃ C)
     --------------------------------------------------
     → coe (ua α · ua β) ≡ ((coe (ua α)) :> coe (ua β))

   coe-ua-· α β =
       begin
         coe (ua α · ua β)
           ≡⟨⟩
         tr (λ X → X) (ua α · ua β)
           ≡⟨ ! (transport-comp (ua α) (ua β)) ⟩
         (tr (λ X → X) (ua α)) :> (tr (λ X → X) (ua β))
           ≡⟨ idp ⟩
         ((coe (ua α)) :> coe (ua β))
       ∎

   idtoequiv-ua-· ite-ua-·
     : {C : Type ℓ}
     → (α : A ≃ B)
     → (β : B ≃ C)
     ---------------------------------------------------
     → idtoeqv (ua α · ua β) ≡ ((idtoeqv (ua α)) :>≃ (idtoeqv (ua β)))

   idtoequiv-ua-· α β = sameEqv (coe-ua-· α β)
       where open import foundations.HLevelLemmas
   ite-ua-· = idtoequiv-ua-·

   :>≃-ite-ua
     : {C : Type ℓ}
     → (α : A ≃ B)  → (β : B ≃ C)
     ------------------------------
     → (α :>≃ β) ≡ idtoeqv (ua α · ua β)

   :>≃-ite-ua {C = C} α β =
     begin
       (α :>≃ β)
         ≡⟨ sameEqv cβ ⟩
       (α :>≃ (idtoeqv (ua β)))
         ≡⟨ sameEqv cα ⟩
       (idtoeqv {A = A} (ua {A = A} α)) :>≃ (idtoeqv (ua β))
         ≡⟨ ! ite-ua-· {C = C} α β ⟩
       idtoeqv (ua α · ua β)
       ∎
       where
       open import foundations.HLevelLemmas

       cβ : π₁ (α :>≃ β) ≡ π₁ (α :>≃ idtoeqv (ua β))
       cβ = ap (λ w → π₁ (α :>≃ w)) (! ua-β β)

       cα : π₁ (α :>≃ idtoeqv (ua β)) ≡ π₁ (idtoeqv (ua α) :>≃ idtoeqv (ua β))
       cα = ap (λ w → π₁ (w :>≃ idtoeqv (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