{-# OPTIONS --without-K #-}
open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.NType2
open import Sec2preliminaries
open import Sec3hedberg
open import Sec4collapsibility
module Sec5factorConst where
factorizes-through : {X Y : Type} → Type → (X → Y) → Type
factorizes-through {X} {Y} Z f = Σ (X → Z) λ f₁ → Σ (Z → Y) λ f₂ → (x : X) → f₂ (f₁ x) == f x
factorizes : {X Y : Type} → (X → Y) → Type
factorizes {X} = factorizes-through (Trunc X)
factorize-helper : {X Y : Type} → (f : X → Y) → (P : Type) → (X → is-prop P) → (factorizes-through P f) → factorizes f
factorize-helper {X} {Y} f P xpp (f₁ , f₂ , q) = f₁' , f₂' , q' where
f₁' : X → Trunc X
f₁' = ∣_∣
f₂' : Trunc X → Y
f₂' z = f₂ (rec {X} (rec is-prop-is-prop xpp z) f₁ z)
q' : (x : X) → f₂' (f₁' x) == f x
q' x =
f₂' (f₁' x) =⟨ idp ⟩
f₂' ∣ x ∣ =⟨ idp ⟩
f₂ (rec _ f₁ ∣ x ∣ ) =⟨ ap f₂ (trunc-β _ f₁ x) ⟩
f₂ (f₁ x) =⟨ q x ⟩
f x ∎
module thm53 {X Y : Type} (f : X → Y) (c : const f) where
One = ¬ X
Two = X
Three = Trunc X → X
Four = coll X
Five = Y → X
One→Three : One → Three
One→Three nx z = Empty-elim {A = λ _ → X} (rec Empty-elim nx z)
Two→Three : Two → Three
Two→Three x = λ _ → x
Five→Four : Five → Four
Five→Four g = g ∘ f , (λ x₁ x₂ → ap g (c x₁ x₂))
Three↔Four : Three ↔ Four
Three↔Four = snd coll↔hstable , fst coll↔hstable
Three→factorizes : Three → factorizes f
Three→factorizes s = ∣_∣ , f ∘ s , (λ x → c _ _)
double-rec : {X₁ X₂ P : Type} → (is-prop P) → (X₁ → X₂ → P) → Trunc X₁ → Trunc X₂ → P
double-rec {X₁} {X₂} {P} pp f z₁ z₂ = next-step z₂ z₁ where
step : X₁ → Trunc X₂ → P
step x₁ = rec {X = X₂} {P = P} pp (f x₁)
step-switch : Trunc X₂ → X₁ → P
step-switch z₂ x₁ = step x₁ z₂
next-step : Trunc X₂ → Trunc X₁ → P
next-step z₂ = rec pp (step-switch z₂)
factorize-codomain-set : {X Y : Type} → (f : X → Y) → const f → is-set Y → factorizes f
factorize-codomain-set {X} {Y} f c h = factorize-helper f P (λ _ → pp) fact-through-p where
P : Type
P = Σ Y λ y → Trunc(Σ X λ x → f x == y)
pp : is-prop P
pp = all-paths-is-prop all-paths where
all-paths : has-all-paths P
all-paths (y₁ , t₁) (y₂ , t₂) = pair= ys ts where
ys = double-rec {P = y₁ == y₂} (h _ _) (λ {(x₁ , p₁) (x₂ , p₂) → ! p₁ ∙ c _ _ ∙ p₂}) t₁ t₂
ts = from-transp _ ys (prop-has-all-paths (h-tr _) _ _)
fact-through-p : factorizes-through P f
fact-through-p = f₁ , f₂ , q where
f₁ : X → P
f₁ x = f x , ∣ x , idp ∣
f₂ : P → Y
f₂ = fst
q : (x : X) → f₂ (f₁ x) == f x
q x = idp
open import library.types.Pi
switch23 : {X : Type} → {Y Z : X → Type} → {W : (x : X) → (Y x) → (Z x) → Type} →
(Σ X λ x → Σ (Y x) λ y → Σ (Z x) λ z → (W x y z)) ≃
(Σ X λ x → Σ (Z x) λ z → Σ (Y x) λ y → (W x y z))
switch23 = equiv (λ {(y , s , t , coh) → (y , t , s , coh)}) (λ {(y , t , s , coh) → (y , s , t , coh)}) (λ _ → idp) (λ _ → idp)
module thm55aux {P : Type} {Y : P → Type} (pp : is-prop P) (x₀ : P) where
neutral-contr-base-space : Σ P Y ≃ Y x₀
neutral-contr-base-space =
Σ P Y ≃⟨ (equiv-Σ-fst {A = Unit} {B = P} Y
{λ _ → x₀}
(is-eq _ (λ _ → unit) (λ _ → prop-has-all-paths pp _ _) (λ _ → idp))) ⁻¹ ⟩
Σ Unit (λ _ → Y x₀) ≃⟨ Σ₁-Unit ⟩
Y x₀ ≃∎
neutral-contr-exp : Π P Y ≃ Y x₀
neutral-contr-exp =
Π P Y ≃⟨ (equiv-Π-l {A = Unit} {B = P} Y
{λ _ → x₀}
(is-eq _ (λ _ → unit) (λ _ → prop-has-all-paths pp _ _) (λ _ → idp))) ⁻¹ ⟩
Π Unit (λ _ → Y x₀) ≃⟨ Π₁-Unit ⟩
Y x₀ ≃∎
module thm55 {Q R Y : Type} (qq : is-prop Q) (rr : is-prop R) (f : Q + R → Y) (c : const f) where
P : Type
P = Σ Y λ y →
Σ ((q : Q) → y == f(inl q)) λ s →
Σ ((r : R) → y == f(inr r)) λ t →
(q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r)
given-q-reduce-P : Q → P ≃ Unit
given-q-reduce-P q₀ =
P
≃⟨ switch23 ⟩
(Σ Y λ y →
Σ ((r : R) → y == f(inr r)) λ t →
Σ ((q : Q) → y == f(inl q)) λ s →
(q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩
(Σ Y λ y →
Σ ((r : R) → y == f(inr r)) λ t →
(q : Q) → Σ (y == f(inl q)) λ s-reduced →
(r : R) → ! s-reduced ∙ (t r) == c (inl q) (inr r))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → thm55aux.neutral-contr-exp qq q₀)) ⟩
(Σ Y λ y →
Σ ((r : R) → y == f(inr r)) λ t →
Σ (y == f(inl q₀)) λ s-reduced →
(r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))
≃⟨ switch23 ⟩
(Σ Y λ y →
Σ (y == f(inl q₀)) λ s-reduced →
Σ ((r : R) → y == f(inr r)) λ t →
(r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩
(Σ Y λ y →
Σ (y == f(inl q₀)) λ s-reduced →
(r : R) → Σ (y == f(inr r)) λ t-reduced →
! s-reduced ∙ t-reduced == c (inl q₀) (inr r))
≃⟨ Σ-assoc ⁻¹ ⟩
(Σ (Σ Y λ y → (y == f(inl q₀))) λ {(y , s-reduced) →
(r : R) → Σ (y == f(inr r)) λ t-reduced →
! s-reduced ∙ t-reduced == c (inl q₀) (inr r)})
≃⟨ thm55aux.neutral-contr-base-space (contr-is-prop (pathto-is-contr _)) (f(inl q₀) , idp) ⟩
((r : R) → Σ (f(inl q₀) == f(inr r)) λ t-reduced →
idp ∙ t-reduced == c (inl q₀) (inr r))
≃⟨ neutral-codomain (λ r → pathto-is-contr _) ⟩
Unit ≃∎
given-r-reduce-P : R → P ≃ Unit
given-r-reduce-P r₀ =
P
≃⟨ equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → switch-args))) ⟩
(Σ Y λ y →
Σ ((q : Q) → y == f(inl q)) λ s →
Σ ((r : R) → y == f(inr r)) λ t →
(r : R) → (q : Q) → ! (s q) ∙ (t r) == c (inl q) (inr r))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩
(Σ Y λ y →
Σ ((q : Q) → y == f(inl q)) λ s →
(r : R) → Σ (y == f(inr r)) λ t-reduced →
(q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → thm55aux.neutral-contr-exp rr r₀)) ⟩
(Σ Y λ y →
Σ ((q : Q) → y == f(inl q)) λ s →
Σ (y == f(inr r₀)) λ t-reduced →
(q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))
≃⟨ switch23 ⟩
(Σ Y λ y →
Σ (y == f(inr r₀)) λ t-reduced →
Σ ((q : Q) → y == f(inl q)) λ s →
(q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))
≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩
(Σ Y λ y →
Σ (y == f(inr r₀)) λ t-reduced →
(q : Q) → Σ (y == f(inl q)) λ s-reduced →
! s-reduced ∙ t-reduced == c (inl q) (inr r₀))
≃⟨ Σ-assoc ⁻¹ ⟩
(Σ (Σ Y λ y → (y == f(inr r₀))) λ {(y , t-reduced) →
(q : Q) → Σ (y == f(inl q)) λ s-reduced →
! s-reduced ∙ t-reduced == c (inl q) (inr r₀)})
≃⟨ thm55aux.neutral-contr-base-space (contr-is-prop (pathto-is-contr _)) (f(inr r₀) , idp) ⟩
((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
! s-reduced ∙ idp == c (inl q) (inr r₀))
≃⟨ equiv-Π-r (λ q → equiv-Σ-snd (λ proof →
! proof ∙ idp == c (inl q) (inr r₀) ≃⟨ delete-idp _ _ ⟩
! proof == c (inl q) (inr r₀) ≃⟨ reverse-paths _ _ ⟩
proof == ! (c (inl q) (inr r₀)) ≃∎
)) ⟩
((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
s-reduced == ! (c (inl q) (inr r₀)))
≃⟨ neutral-codomain (λ q → pathto-is-contr _) ⟩
Unit ≃∎
given-q+r-reduce-P : Q + R → P ≃ Unit
given-q+r-reduce-P (inl q) = given-q-reduce-P q
given-q+r-reduce-P (inr r) = given-r-reduce-P r
Q+R→P : Q + R → P
Q+R→P x = <– (given-q+r-reduce-P x) _
P→Y : P → Y
P→Y = fst
open import library.types.Unit
factorize-f : factorizes f
factorize-f = factorize-helper f P (λ x → equiv-preserves-level ((given-q+r-reduce-P x) ⁻¹) Unit-is-prop) (Q+R→P , P→Y , proof) where
proof : (x : Q + R) → P→Y (Q+R→P x) == f x
proof (inl q) = idp
proof (inr r) = idp
Theorem55 : {Q R Y : Type} → (is-prop Q) → (is-prop R) → (f : Q + R → Y) → (const f) → factorizes f
Theorem55 = thm55.factorize-f