{-# OPTIONS --without-K #-}
open import function.extensionality.core
module hott.weak-equivalence.alternative where
open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.extensionality.dependent
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.utils
open import hott.hlevel.core
open import hott.weak-equivalence.core
open import hott.univalence
private
module Properties {i j}{X : Set i}{Y : Set j} where
open ≅-Reasoning
private
A : (f : X → Y)(g : Y → X) → Set _
A f g = (x : X) → g (f x) ≡ x
B : (f : X → Y)(g : Y → X) → Set _
B f g = (y : Y) → f (g y) ≡ y
GB : (f : X → Y) → Set _
GB f = Σ (Y → X) (B f)
Φ : (f : X → Y)(g : Y → X) → Set _
Φ f g = (y : Y)(x : X) → f x ≡ y → g y ≡ x
Ψ : (f : X → Y)(g : Y → X)(β : B f g)(φ : Φ f g) → Set _
Ψ f g β φ = (y : Y)(x : X)(p : f x ≡ y) → cong f (φ y x p) ⊚ p ≡ β y
W : Set _
W = Σ (X → Y) λ f
→ Σ (GB f) λ { (g , β)
→ Σ (Φ f g) (Ψ f g β) }
Π-iso : ∀ {i j j'} {X : Set i}
{Y : X → Set j}{Y' : X → Set j'}
→ ((x : X) → Y x ≅ Y' x)
→ ((x : X) → Y x)
≅ ((x : X) → Y' x)
Π-iso = Π-cong-iso ext' refl≅
_⋆_ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
→ Y ≅ Z → X ≅ Y → X ≅ Z
isom ⋆ isom' = trans≅ isom' isom
contr-split : (f : X → Y)(g : Y → X)(β : B f g)
→ ((y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x)
≅ Σ (Φ f g) (Ψ f g β)
contr-split f g β = begin
((y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x)
≅⟨ (Π-iso λ y → curry-iso (λ x p → (g y , β y) ≡ (x , p))) ⟩
((y : Y)(x : X)(p : f x ≡ y) → (g y , β y) ≡ (x , p))
≅⟨ (Π-iso λ y → Π-iso λ x → Π-iso λ p
→ sym≅ (Σ-split-iso {b = β y}{b' = p})) ⟩
((y : Y)(x : X)(p : f x ≡ y) → Σ (g y ≡ x) λ q
→ subst (λ x → f x ≡ y) q (β y) ≡ p)
≅⟨ (ΠΣ-swap-iso ⋆ Π-iso λ y
→ ΠΣ-swap-iso ⋆ Π-iso λ x
→ ΠΣ-swap-iso {Z = λ p q → subst (λ x → f x ≡ y) q (β y) ≡ p}) ⟩
( Σ (Φ f g) λ φ
→ (y : Y)(x : X)(p : f x ≡ y)
→ subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p )
≅⟨ (Σ-cong-iso refl≅ λ φ
→ Π-iso λ y → Π-iso λ x → Π-iso λ p
→ lem f g β φ y x p) ⟩
Σ (Φ f g) (Ψ f g β)
∎
where
lem : (f : X → Y)(g : Y → X)(β : (y : Y) → f (g y) ≡ y)
(φ : (y : Y)(x : X) → f x ≡ y → g y ≡ x)
→ (y : Y)(x : X)(p : f x ≡ y)
→ (subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p)
≅ (cong f (φ y x p) ⊚ p ≡ β y)
lem f g β φ y x p = begin
subst (λ x → f x ≡ y) (φ y x p) (β y) ≡ p
≡⟨ cong (λ z → z ≡ p)
( subst-naturality (λ x → x ≡ y) f (φ y x p) (β y)
⊚ subst-eq (cong f (φ y x p)) (β y) ) ⟩
sym (cong f (φ y x p)) ⊚ β y ≡ p
≅⟨ sym≅ (move-≡-iso (cong f (φ y x p)) p (β y)) ⟩
cong f (φ y x p) ⊚ p ≡ β y
∎
weak-equiv-split : (X ≈ Y) ≅ W
weak-equiv-split =
Σ-cong-iso refl≅ (λ f → begin
weak-equiv f
≅⟨ ΠΣ-swap-iso ⟩
Σ ((y : Y) → f ⁻¹ y) (λ { gβ
→ (y : Y)(x : f ⁻¹ y) → gβ y ≡ x })
≅⟨ Σ-cong-iso ΠΣ-swap-iso (λ _ → refl≅) ⟩
( Σ (GB f) λ { (g , β)
→ (y : Y)(x : f ⁻¹ y) → (g y , β y) ≡ x } )
≅⟨ Σ-cong-iso refl≅ (λ { (g , β) → contr-split f g β }) ⟩
( Σ (GB f) λ { (g , β)
→ Σ (Φ f g) (Ψ f g β) } )
∎ )
≈⇔≅' : (X ≈ Y) ≅ (X ≅' Y)
≈⇔≅' = begin
X ≈ Y
≅⟨ weak-equiv-split ⟩
W
≅⟨ Σ-cong-iso refl≅ (λ f
→ Σ-cong-iso refl≅ λ { (g , K)
→ Σ-cong-iso {Y = Ψ f g K}
(φ≅H f g)
(λ H → ψ≅γ f g H K) }) ⟩
( Σ (X → Y) λ f
→ Σ (GB f) λ { (g , K)
→ Σ (A f g) λ H
→ coherent (iso f g H K) } )
≅⟨ iso (λ { (f , (g , K) , H , γ) → iso f g H K , γ })
(λ { (iso f g H K , γ) → (f , (g , K) , H , γ) })
(λ _ → refl) (λ _ → refl) ⟩
X ≅' Y
∎
where
Ψ' : (f : X → Y)(g : Y → X)(K : B f g)(H : A f g) → Set _
Ψ' f g K H = ((y : Y)(x : X)(p : f x ≡ y)
→ cong f (sym (cong g p) ⊚ H x) ⊚ p ≡ K y)
φ≅H : (f : X → Y)(g : Y → X) → Φ f g ≅ A f g
φ≅H f g = record
{ to = λ φ x → φ (f x) x refl
; from = λ H y x p → sym (cong g p) ⊚ H x
; iso₁ = λ φ → ext' λ y → ext' λ x → ext' λ p → lem φ y x p
; iso₂ = λ H → refl }
where
lem : (φ : (y : Y)(x : X) → f x ≡ y → g y ≡ x)
→ (y : Y)(x : X)(p : f x ≡ y)
→ sym (cong g p) ⊚ φ (f x) x refl ≡ φ y x p
lem φ .(f x) x refl = refl
ψ≅γ : (f : X → Y)(g : Y → X)(H : A f g)(K : B f g)
→ Ψ' f g K H ≅ coherent (iso f g H K)
ψ≅γ f g H K = record
{ to = to
; from = from
; iso₁ = λ ψ → ext' λ y → ext' λ x → ext' λ p → lem₁ ψ y x p
; iso₂ = λ γ → ext' λ x → lem₂ γ x }
where
to : Ψ' f g K H → coherent (iso f g H K)
to ψ x = sym (left-unit _) ⊚ ψ (f x) x refl
from : coherent (iso f g H K) → Ψ' f g K H
from γ .(f x) x refl = left-unit _ ⊚ γ x
lem₁ : (ψ : Ψ' f g K H)(y : Y)(x : X)(p : f x ≡ y)
→ from (to ψ) y x p ≡ ψ y x p
lem₁ φ .(f x) x refl =
J (λ u v q → (z : f (g (f x)) ≡ f x)
(r : u ≡ z)
→ q ⊚ (sym q ⊚ r) ≡ r)
(λ u z r → refl) _ _
(left-unit (cong f (H x))) _
(φ (f x) x refl)
lem₂ : (γ : coherent (iso f g H K))(x : X)
→ to (from γ) x ≡ γ x
lem₂ γ x =
J (λ u v q → (z : f (g (f x)) ≡ f x)
→ (r : v ≡ z)
→ sym q ⊚ (q ⊚ r) ≡ r)
(λ u z r → refl) _ _
(left-unit (cong f (H x))) _
(γ x)
open _≅_ ≈⇔≅' public using ()
renaming ( to to ≈⇒≅'
; from to ≅'⇒≈ )
≅⇒≈ : (X ≅ Y) → (X ≈ Y)
≅⇒≈ = ≅'⇒≈ ∘ ≅⇒≅'
open Properties public