Investigations on graph-theoretical constructions in Homotopy type theory

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

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

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

module _ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{C : A → Type ℓ₂}{D : A → Type ℓ₃}
    (e : (a : A) → (C a ≃ D a))
  where

  private
    f : (a : A) → C a → D a
    f a = lemap (e a)

    f⁻¹ : (a : A) → D a → C a
    f⁻¹ a = remap (e a)

    α : (a : A) → (f a) ∘ (f⁻¹ a) ∼ id
    α a x = lrmap-inverse (e a)

    β : (a : A) → (f⁻¹ a) ∘ (f a) ∼ id
    β a x = rlmap-inverse (e a)

    ΠAC→ΠAD : Π A C → Π A D
    ΠAC→ΠAD p = λ a → (f a) (p a)

    ΠAD→ΠAC : Π A D → Π A C
    ΠAD→ΠAC p = λ a → (f⁻¹ a) (p a)

    H₁ : ΠAC→ΠAD ∘ ΠAD→ΠAC ∼ id
    H₁ p =
      begin
        (ΠAC→ΠAD ∘ ΠAD→ΠAC) p
          ≡⟨ idp ⟩
        ΠAC→ΠAD (λ a → (f⁻¹ a) (p a))
          ≡⟨ idp ⟩
        (λ aa → (f aa) (f⁻¹ aa (p aa)))
          ≡⟨ funext (λ x → α x (p x)) ⟩
        (λ aa → p aa)
      ∎

    H₂ : ΠAD→ΠAC ∘ ΠAC→ΠAD ∼ id
    H₂ p =
      begin
        (ΠAD→ΠAC ∘ ΠAC→ΠAD) p
          ≡⟨ idp ⟩
        ΠAD→ΠAC (λ a → (f a) (p a))
          ≡⟨ idp ⟩
        (λ aa → (f⁻¹ aa) (f aa (p aa)))
          ≡⟨ funext (λ x → β x (p x)) ⟩
        (λ aa → p aa)
      ∎

  pi-equivalence
    : Π A C ≃ Π A D -- by (e : (a : A) → (C a ≃ D a))

  pi-equivalence = qinv-≃ ΠAC→ΠAD (ΠAD→ΠAC , H₁ , 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