{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Sigma
open import lib.NType2

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit

open wtrunc
open with-weak-trunc

module Weakly_Constant_Functions where

-- Definition 5.1.1
factorizes-through :  {i j} {X : Type i} {Y : Type j}  Type i  (X  Y)  Type (i  j)
factorizes-through {X = X} {Y = Y} Z f = Σ (X  Z) λ f₁  Σ (Z  Y) λ f₂  (x : X)  f₂ (f₁ x) == f x

-- Definition 5.1.1 addendum: 'factorizes through the truncation'
-- In the theory of the thesis, universes are cumulative.
-- Here, we ask all the types to be in the same universe.
factorizes :  {i} {X : Type i} {Y : Type i}  (X  Y)  Type i
factorizes {X = X} = factorizes-through (∣∣ X ∣∣)

-- Principle 5.2.1
factorize-helper :  {i} {X : Type i} {Y : Type i}  (f : X  Y)  (P : Type i)  (X  is-prop P)  (factorizes-through P f)  factorizes f
factorize-helper {X = X} {Y = Y} f P xpp (f₁ , f₂ , q) = f₁' , f₂' , q' where
f₁' : X  ∣∣ X ∣∣
f₁' = ∣_∣

f₂' : ∣∣ X ∣∣  Y
f₂' z = f₂ (tr-rec {X = X} (tr-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₂ (tr-rec _ f₁  x  ) =⟨ ap f₂ (trunc-β _ f₁ x)
f₂ (f₁ x)           =⟨ q x
f x

-- Proposition 5.2.2
module st522 {i : ULevel} {X : Type i} {Y : Type i} (f : X  Y) (c : const f) where
One = ¬ X
Two = X
Three = ∣∣ X ∣∣  X
Four = coll X
Five = Y  X

One→Three : One  Three
One→Three nx z = Empty-elim {A = λ _  X} (tr-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↔splitSup , fst coll↔splitSup

Three→factorizes : Three  factorizes f
Three→factorizes s = ∣_∣ , f  s ,  x  c _ _)

-- Proposition 5.2.3 preparation
-- as a small preparation, let us define a function that applies the truncation tr-recursor twice.
-- Because of how we have defined the operator ∣∣_∣∣, we need everything to happen in the same universe
double-tr-rec :  {i} {X₁ X₂ P : Type i}  (is-prop P)  (X₁  X₂  P)  ∣∣ X₁ ∣∣  ∣∣ X₂ ∣∣  P
double-tr-rec {i} {X₁} {X₂} {P} pp f z₁ z₂ = next-step z₁ z₂ where
step : X₁  ∣∣ X₂ ∣∣  P
step x₁ = tr-rec {X = X₂} {P = P} pp (f x₁)
step-switch : ∣∣ X₂ ∣∣  X₁  P
step-switch z₂ x₁ = step x₁ z₂
next-step : ∣∣ X₁ ∣∣  ∣∣ X₂ ∣∣  P
next-step z₁ z₂ = tr-rec pp (step-switch z₂) z₁ -- tr-rec pp (step-switch z₂)

-- now, the actual Proposition 5.2.3
factorize-codomain-set :  {i} {X : Type i} {Y : Type i}  (f : X  Y)  const f  is-set Y  factorizes f
factorize-codomain-set {i} {X} {Y} f c h = factorize-helper f P  _  pp) fact-through-p where
P : Type i
P = Σ Y λ y  ∣∣ (Σ 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-tr-rec {P = y₁ == y₂} (h _ _)  {(x₁ , p₁) (x₂ , p₂)  ! p₁  c _ _  p₂}) t₁ t₂
ts = from-transp _ ys (prop-has-all-paths tr-is-prop _ _)

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.2.6
-- We need function extensionality and thus import
-- the following:
open import lib.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 :  {i} {X : Type i}  {Y Z : X  Type i}  {W : (x : X)  (Y x)  (Z x)  Type i}
(Σ 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)

-- Theorem 5.2.6, with the 'equivalence reasoning' tactic:
module thm526 {i : ULevel} {Q R Y : Type i} (qq : is-prop Q) (rr : is-prop R) (f : Coprod Q R  Y) (c : const f) where

P : Type i
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  Π₁-contr (q₀ , prop-has-all-paths 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)})

≃⟨ Σ₁-contr (pathto-is-contr _)

((r : R)  Σ (f(inl q₀) == f(inr r)) λ t-reduced
idp  t-reduced == c (inl q₀) (inr r))

≃⟨ Π₂-contr  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  Π₁-contr (r₀ , prop-has-all-paths 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₀)})

≃⟨ Σ₁-contr (pathto-is-contr _)

((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₀)))

≃⟨ Π₂-contr  q  pathto-is-contr _)

Unit                 ≃∎

given-q+r-reduce-P : Coprod 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 : Coprod Q R  P
Q+R→P x = <– (given-q+r-reduce-P x) _

P→Y : P  Y
P→Y = fst

open import lib.types.Unit

-- Finally : the statement of Theorem 5.2.6
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 : Coprod Q R)  P→Y (Q+R→P x) == f x
proof (inl q) = idp
proof (inr r) = idp

-- and Theorem 5.2.6 again (outside of a specialized module)
Theorem526 :  {i} {Q R Y : Type i}  (is-prop Q)  (is-prop R)  (f : Coprod Q R  Y)  (const f)  factorizes f
Theorem526 = thm526.factorize-f