{-# 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

-- Definition 5.1
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

-- Definition 5.1 addendum: "factorizes through the truncation"
factorizes : {X Y : Type}  (X  Y)  Type
factorizes {X} = factorizes-through (Trunc X)

-- Principle 5.2
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                  

-- Theorem 5.3
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 _ _)

-- Theorem 5.4
-- as a small preparation, let us define a function that applies the truncation recursor twice:
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₂)

-- now, the actual Theorem 5.4
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

-- Theorem 5.5
-- Note that this lemma requires function extensionality (hidden in the use of the library.types.Pi library: 
-- at one point, we use that Π X Y is propositional as soon as Y x is (for all x)).

open import library.types.Pi

-- a general auxiliary function which switches the second and third component of a Σ-type with four components
-- (provided that it is possible)
-- we formulate this explicitly as we will need it several times
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)

  -- This is going to be tedious: if q₀ : Q is given, we can show that P is equivalent to the Unit type.
  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

  -- Finally : the statement of Theorem 5.5
  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

-- and Theorem 5.5 again (outside of a specialized module)
Theorem55 : {Q R Y : Type}  (is-prop Q)  (is-prop R)  (f : Q + R  Y)  (const f)  factorizes f
Theorem55 = thm55.factorize-f