Equivalences preserved by Sigma types¶
{-# OPTIONS --without-K --exact-split #-}
module _ where
open import TransportLemmas
open import ProductIdentities
open import CoproductIdentities
open import EquivalenceType
open import HomotopyType
open import HomotopyLemmas
open import HalfAdjointType
open import QuasiinverseType
open import QuasiinverseLemmas
module
SigmaPreserves {ℓ₁ ℓ₂ ℓ₃ : 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₂)
open SigmaPreserves
module SigmaPreserves-≃ {ℓ₁ ℓ₂ ℓ₃}
{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' = transport 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'' = transport C ((α (f b)) ⁻¹) c'
-- patho : c'' == c' [ (C ∘ f) ↓ (β b)]
patho : transport (λ x → C (f x)) (β b) c'' == c'
patho =
begin
transport (λ x → C (f x)) (β b) c''
==⟨ transport-family (β b) c'' ⟩
transport C (ap f (β b)) c''
==⟨ ap (λ γ → transport C γ c'') (τ b) ⟩
transport C (α (f b)) c''
==⟨ transport-comp-h ((α (f b)) ⁻¹) (α (f b)) c' ⟩
transport C ( ((α (f b)) ⁻¹) · α (f b)) c'
==⟨ ap (λ γ → transport C γ c') (·-linv (α (f b))) ⟩
transport C idp c'
==⟨⟩
c'
∎
private
H₂ : ΣBCf-to-ΣAC ∘ ΣAC-to-ΣBCf ∼ id
H₂ (a , c) = pair= (α a , patho)
where
patho : transport C (α a) (transport C ((α a) ⁻¹) c) == c
patho =
begin
transport C (α a) (transport C ((α a) ⁻¹) c)
==⟨ transport-comp-h (((α a) ⁻¹)) (α a) c ⟩
transport C ( ((α a) ⁻¹) · (α a) ) c
==⟨ ap (λ γ → transport C γ c) (·-linv (α a)) ⟩
transport 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-≃ α))
where
open SigmaPreserves
open SigmaPreserves-≃