Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.SigmaPreserves where

open import foundations.TransportLemmas
open import foundations.ProductIdentities
open import foundations.CoproductIdentities

open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.HomotopyLemmas

open import foundations.HalfAdjointType
open import foundations.QuasiinverseType
open import foundations.QuasiinverseLemmas

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-to-ΣAD : Σ A C → Σ A D
    ΣAC-to-ΣAD (a , c) = (a , (f a) c)

    ΣAD-to-ΣAC : Σ A D → Σ A C
    ΣAD-to-ΣAC (a , d) = (a , (f⁻¹ a) d)

    H₁ : ΣAC-to-ΣAD ∘ ΣAD-to-ΣAC ∼ id
    H₁ (a , d) = pair= (idp , α a d)

    H₂ : ΣAD-to-ΣAC ∘ ΣAC-to-ΣAD ∼ id
    H₂ (a , c) = pair= (idp , β a c)

  sigma-preserves : Σ A C ≃ Σ A D
  sigma-preserves = qinv-≃ ΣAC-to-ΣAD (ΣAD-to-ΣAC , H₁ , H₂)

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

  private
    f : B → A
    f = lemap e

    ishaef : ishae f
    ishaef = ≃-ishae e

    f⁻¹ : A → B
    f⁻¹ = ishae.g ishaef

    α : f ∘ f⁻¹ ∼ id
    α = ishae.ε ishaef

    β : f⁻¹ ∘ f  ∼ id
    β = ishae.η ishaef

    τ : (b : B) → ap f (β b) ≡ α (f b)
    τ = ishae.τ ishaef

  ΣAC-to-ΣBCf : Σ A C → Σ B (λ b → C (f b))
  ΣAC-to-ΣBCf (a , c) = f⁻¹ a , c'
    where
      c' : C (f (f⁻¹ a))
      c' = tr C ((α a) ⁻¹) c

  ΣBCf-to-ΣAC : Σ B (λ b → C (f b)) → Σ A C
  ΣBCf-to-ΣAC (b , c') = f b , c'

  private
    H₁ : ΣAC-to-ΣBCf ∘ ΣBCf-to-ΣAC ∼ id
    H₁ (b , c') = pair= (β b , patho)
      where
      c'' : C (f (f⁻¹ (f b)))
      c'' = tr C ((α (f b)) ⁻¹) c'

      -- patho : c'' ≡ c' [ (C ∘ f) ↓ (β b)]
      patho : tr (λ x → C (f x)) (β b) c'' ≡ c'
      patho =
        begin
          tr (λ x → C (f x)) (β b) c''
            ≡⟨ transport-family (β b) c'' ⟩
          tr C (ap f (β b)) c''
            ≡⟨ ap (λ γ → tr C γ c'') (τ b) ⟩
          tr C (α (f b)) c''
            ≡⟨ transport-comp-h ((α (f b)) ⁻¹) (α (f b)) c' ⟩
          tr C ( ((α (f b)) ⁻¹) · α (f b)) c'
            ≡⟨ ap (λ γ → tr C γ c') (·-linv (α (f b))) ⟩
          tr C idp c'
            ≡⟨⟩
          c'
        ∎

  private
    H₂ : ΣBCf-to-ΣAC ∘ ΣAC-to-ΣBCf ∼ id
    H₂ (a , c) = pair= (α a , patho)
      where
      patho : tr C (α a) (transport C ((α a) ⁻¹) c) ≡ c
      patho =
        begin
          tr C (α a) (transport C ((α a) ⁻¹) c)
            ≡⟨ transport-comp-h (((α a) ⁻¹)) (α a) c ⟩
          tr C ( ((α a) ⁻¹) · (α a) ) c
            ≡⟨ ap (λ γ → tr C γ c) (·-linv (α a)) ⟩
          tr C idp c
            ≡⟨⟩
          c
        ∎

  sigma-preserves-≃
    : Σ A C ≃ Σ B (λ b → C (f b))

  sigma-preserves-≃ = qinv-≃ ΣAC-to-ΣBCf (ΣBCf-to-ΣAC , H₁ , H₂)

sigma-maps-≃
  : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Type ℓ₁} {A' : Type ℓ₄} {B : A → Type ℓ₂}{B' : A' → Type ℓ₃}
  → (α : A ≃ A')
  → ((a : A) → (B a ≃ B' ((α ∙) a)))
  ----------------------------------
  → Σ A B ≃ Σ A' B'

sigma-maps-≃ {A = A}{A'}{B}{B'} α β =
  ≃-trans (sigma-preserves β) (≃-sym (sigma-preserves-≃ α))

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