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

open import lib.Basics
open import lib.NType2
open import lib.PathFunctor
open import lib.PathGroupoid

open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim
open import nicolai.pseudotruncations.wconstSequence

module nicolai.pseudotruncations.PseudoTruncs-wconst-seq where

open import nicolai.pseudotruncations.pointed-O-Sphere
open import nicolai.pseudotruncations.LoopsAndSpheres
open import nicolai.pseudotruncations.PseudoTruncs

{- The special sequence that we consider -}
module PtruncsSeq {i} (X : Type i) where

A : ℕ → Type i
A O = X
A (S n) = Pseudo n -1-trunc (A n)

f : (n : ℕ) → A n → A (S n)
f n x = point n -1 x

C : Sequence {i}
C = (A , f)

{- A main result: If we have an inhabitant of X, then the sequence is weakly constant.
This is Lemma 6.2 ! -}
module PtruncSeqWC {i} (X : Type i) (x₀ : X) where

open PtruncsSeq {i} X

fs : (n : ℕ) → A n
fs O = x₀
fs (S n) = f n (fs n)

P : (n : ℕ) → (x : A n) → Type i
P n x = f n x == fs (S n)

{- This is the easy 'Case j ≡ -2' -}
f₀-x₀ : (y : X) → P O y
f₀-x₀ y = (spoke O -1 r (lift false)) ∙ ! (spoke O -1 r (lift true))  where

r : Sphere {i} O → X
r (lift true) = x₀
r (lift false) = y

{- Now, the general case is done by induction on n
(note that this variable is called 'j' in the paper).
Hence, what is 'j' in the paper is now 'S n'.

Unfortunately, we have to do everything in one "big"
step with many "where" clauses due to the mutual dependencies. -}

fₙ-x₀ : (n : ℕ) → (y : A n) → P n y
fₙ-x₀ O y = f₀-x₀ y
fₙ-x₀ (S n) = Pseudotrunc-ind n Point Hub Spoke where

-- just for convenience - saves brackets
norₙ' : Sphere' {i} n
norₙ' = nor' n

fⁿx₀ = fs n

Point : (w : A n) → P (S n) (point n -1 w)
Point w = ap (point (S n) -1) (fₙ-x₀ n w)

Hub : (r : Sphere' n → A n) → point S n -1 _ == _
Hub r = ap (point (S n) -1) (! (spoke n -1 r norₙ') ∙ fₙ-x₀ n (r norₙ'))

{- The definition of [Spoke] is the hard part.
First, we do the easy things that we have to do... -}
Spoke : (r : _) → (x : Sphere' n) → _
Spoke r = λ x → from-transp (P (S n))
(spoke n -1 r x)
(
transport (P (S n)) (spoke n -1 r x) (Point (r x))
=⟨ trans-ap₁ (f (S n)) (fs (S (S n))) (spoke n -1 r x) (Point (r x)) ⟩
! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x)
=⟨ ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ₗ ! (∙-unit-r (Point (r x))) ⟩
! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x) ∙ idp
{- Now comes the hard step which requires A LOT of work in the where clause
below: we can compose with something which, for a complicated reason, is idp! -}
=⟨ ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ₗ (Point (r x) ∙ₗ ! (k-const x)) ⟩
! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x) ∙ k x
{- From here, it's easy; we just have to re-associate paths and cancel inverses.
This could be done with standard library lemmas, but it's easier to just use
=⟨ multi-cancelling (ap (point S n -1) (spoke n -1 r x)) (Point (r x)) (Hub r) ⟩
Hub r
∎
)

where

{- Now, the actual work follows! -}

{- First, we define the interesting loop.
In the paper, it is called [kₓ].
Here, it is just [k x].  -}
k : (x : Sphere' {i} n)
→ Ω (Pseudo S n -1-trunc (A (S n)) ,
f (S n) (f n fⁿx₀))
k x = ! (Point (r x)) ∙ ap (point (S n) -1) (spoke n -1 r x) ∙ (Hub r)

{- We want to show that [k] factors as [ap pₙ ∘ h].
First, we define h. -}
h : Sphere' {i} n
→ Ω (Pseudo n -1-trunc (A n) ,
f n fⁿx₀)
h x =   ! (fₙ-x₀ n (r x))
∙ (spoke n -1 r x)
∙ (! (spoke n -1 r norₙ') ∙ fₙ-x₀ n (r norₙ'))

{- The statement that k == ap pₙ ∘ h: -}
k-p-h : k == ap (point S n -1) ∘ h
k-p-h = λ= (λ (x : Sphere' {i} n)
→ k x
=⟨ idp ⟩
! (Point (r x))
∙ (ap (point (S n) -1) (spoke n -1 r x) ∙ (Hub r))
=⟨ !-ap (point S n -1) (fₙ-x₀ n (r x))
∙ᵣ (  ap (point S n -1) (spoke n -1 r x)
∙ Hub r) ⟩
ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
∙ ap (point (S n) -1) (spoke n -1 r x)
∙ (Hub r)
=⟨ ! (ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
∙ₗ ap-∙ point S n -1
(spoke n -1 r x)
_ ) ⟩
ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
∙ ap (point (S n) -1)
(  spoke n -1 r x
∙ (! (spoke n -1 r norₙ')
∙ fₙ-x₀ n (r norₙ')))
=⟨ ! (ap-∙ point S n -1 (! (fₙ-x₀ n (r x))) _) ⟩
ap (point S n -1) (h x)
∎)

{- [h] can be made into a a pointed map, written [ĥ] -}
ĥ : (⊙Sphere' {i} n)
→̇ ⊙Ω (A (S n) ,
f n fⁿx₀)
ĥ = h ,
(! (fₙ-x₀ n (r _))
∙ (spoke n -1 r _)
∙ ! (spoke n -1 r norₙ')
∙ fₙ-x₀ n (r norₙ')

=⟨ (! (fₙ-x₀ n (r _)))
∙ₗ (! (∙-assoc (spoke n -1 r _)
(! (spoke n -1 r norₙ'))
(fₙ-x₀ n (r norₙ')))) ⟩

! (fₙ-x₀ n (r _))
∙ ((spoke n -1 r _) ∙ (! (spoke n -1 r norₙ')))
∙ fₙ-x₀ n (r norₙ')

=⟨ ! (fₙ-x₀ n (r _))
∙ₗ !-inv-r (spoke n -1 r _)
∙ᵣ fₙ-x₀ n (r norₙ') ⟩

! (fₙ-x₀ n (r _))
∙ idp
∙ fₙ-x₀ n (r norₙ')

=⟨ !-inv-l (fₙ-x₀ n (r _)) ⟩

idp

∎ )

{- A pointed version of the first constructor. -}
pointsₙ : (A (S n) , f n fⁿx₀) →̇ A (S (S n)) , f (S n) (f n fⁿx₀)
pointsₙ = point S n -1 , idp

open null

points-Φ⁻¹-null : isNull∙ (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ)
points-Φ⁻¹-null = <– (isNull-equiv (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ))
-- translate from isNull∙'
(null-lequiv (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ)
-- translate from isNulld; this,
(cmp-nll'.from-sphere-null'∙ n (Φ⁻¹ _ _ ĥ)))

ap-points-ĥ-null : isNull∙ (⊙ap (point S n -1 , idp) ⊙∘ ĥ)
ap-points-ĥ-null = –> (combine-isnull-nat' ĥ (point S n -1 , idp)) points-Φ⁻¹-null

{- ... consequently, h is always refl [in the library "idp"]: -}
points-h-const : (x : Sphere' n) → ap (point S n -1) (h x) == idp
points-h-const x = null-lequiv-easy _ ap-points-ĥ-null x

{- ... and so is k: -}
k-const : (x : Sphere' n) → k x == idp
k-const x = app= k-p-h x  ∙ points-h-const x

{- Main result: each function in the sequence is propositional! -}
wconst-f : wconst-chain C
wconst-f n w₁ w₂ = fₙ-x₀ n w₁ ∙ ! (fₙ-x₀ n w₂)

{- Another important result:
if we want to show a proposition, we can assume A₀ instead of Aω
But this should follow from the general induction principle, so... TODO
-}
module PtruncSeqResult' {i} (X : Type i) where

open PtruncsSeq {i} X -- this defines the chain C of pseudo-truncations

SC = SeqCo C

reduction-lemma : (P : Type i) → (is-prop P) → (A O → P) → (SC → P)
reduction-lemma P ip ff = SeqCo-rec {C = C} {B = P} Ins Glue where

Ins : (n : ℕ) → A n → P
Ins O = ff
Ins (S n) = Pseudotrunc-rec {P = P} n Point-1 Hub-1 Spoke-1 where
Point-1 : _ → P
Point-1 x = Ins n x
Hub-1 : (Sphere' n → A n) → P
Hub-1 r = Ins n (r (nor' n))
Spoke-1 : (r : Sphere' n → A n) (x : Sphere' n) → Point-1 (r x) == Hub-1 r
Spoke-1 r x = prop-has-all-paths {A = P} ip _ _

Glue : (n : ℕ) (a : A n) → Ins n a == Ins (S n) (f n a)
Glue n a = prop-has-all-paths ip _ _

{- Corollary of the main result: The colimit of the considered sequence is propositional! -}
module PtruncSeqResult {i} (X : Type i) where

open PtruncsSeq {i} X -- this defines the chain C of pseudo-truncations

colim-is-prp : is-prop (SeqCo C)
colim-is-prp =
inhab-to-contr-is-prop
(PtruncSeqResult'.reduction-lemma X (is-contr (SeqCo C)) has-level-is-prop
(λ x₀ → ins O x₀ , prop-has-all-paths (wconst-prop C (PtruncSeqWC.wconst-f X x₀))
(ins O x₀)))

open PtruncSeqResult' X

{- If we have the propositional truncation in the theory: -}
open import lib.types.Truncation

colim-is-trunc : (Trunc ⟨-1⟩ X) ≃ SeqCo C
colim-is-trunc = equiv (Trunc-rec (colim-is-prp) (ins 0))
(reduction-lemma (Trunc ⟨-1⟩ X) Trunc-level [_])
(λ _ → prop-has-all-paths colim-is-prp _ _)
(λ _ → prop-has-all-paths Trunc-level _ _)

```