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

{- In this module, we derive the truncations of
* a truncated type,
* the unit type,
* dependent sums (and product types),
* path spaces
given truncations of their components.

More commonly later on, we will be given a truncation operator Tr
that returns a truncation for any given input type (at a fixed level).
Instead of trying to show, say,

Tr (Σ A (B ∘ cons (Tr A))) ≃ Σ (Tr A) (Tr ∘ B),

directly, it turns out to be much easier to just *derive* the truncation on
the left-hand side from Tr A and Tr ∘ B and then use unicity of truncation to
deduce the above equivalence. Significant parts of the unicity proof would be
duplicated in any direct proof of equivalence, while this approach allows us
to avoid a number of manual elimination and propositional reduction steps. -}
module Universe.Trunc.TypeConstructors where

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.types.Unit
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse

open import Universe.Trunc.Universal
open import Universe.Trunc.Basics

open trunc-ty
open trunc-prop

module trunc-self {i} {n : ℕ₋₂} (A : n -Type i) where
trunc : ∀ {j} → trunc-ty n ⟦ A ⟧ j
trunc = record
{ type = A
; cons = idf _
; univ = λ _ → snd (ide _) }

module trunc-⊤ {n : ℕ₋₂} = trunc-self {n = n} ⊤-≤

{- The truncation of a dependent sum type (where the predicate depends
only on the truncation of the first component) is the dependent sums
of the truncations. -}
module trunc-Σ {ia ib j} {n : ℕ₋₂} {A : Type ia}
(TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
{B : ⟦ type TrA ⟧ → Type ib}
(TrB : (ta : ⟦ type TrA ⟧) → trunc-ty n (B ta) (ib ⊔ j)) where

trunc : trunc-ty n (Σ A (B ∘ cons TrA)) (ib ⊔ j)
trunc = record
{ type = Σ-≤ (type TrA) (type ∘ TrB)
; cons = λ {(a , b) → (cons TrA a , cons (TrB (cons TrA a)) b)}
; univ = snd ∘ e } where

e : (U : n -Type _) → _
e U =
(⟦ Σ-≤ (type TrA) (type ∘ TrB) ⟧         → ⟦ U ⟧)  ≃⟨ curry-equiv ⟩
((ta : ⟦ type TrA ⟧) → ⟦ type (TrB ta) ⟧ → ⟦ U ⟧)  ≃⟨ equiv-Π-r eb ⟩
((ta : ⟦ type TrA ⟧) → B ta              → ⟦ U ⟧)  ≃⟨ ea ⟩
((a : A)             → B (cons TrA a)    → ⟦ U ⟧)  ≃⟨ curry-equiv ⁻¹ ⟩
(Σ A (B ∘ cons TrA)                      → ⟦ U ⟧)  ≃∎ where

ea = dup {j = ib ⊔ j} TrA (λ ta → B ta →-≤ U)
eb = λ ta → up {j = ib ⊔ j} (TrB ta) U

-- Products are a special case of dependent sums.
module trunc-× {ia ib j} {n : ℕ₋₂} {A : Type ia} {B : Type ib}
(TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
(TrB : trunc-ty n B (ib ⊔ j)) =
trunc-Σ {j = j} TrA (λ _ → TrB)

{- The n-truncation of a path space is the path space of the (n+1)-truncation.
The use of the encode-decode method is the reason why we have to assume
elimination into Type (lsucc i): large recursion is used to define
the type of codes. -}
module trunc-path {i j} {n : ℕ₋₂} {A : Type i} (TrA : trunc-ty (S n) A (lsucc (i ⊔ j))) where
private
l : ULevel
l = i ⊔ j

TrAA : trunc-ty (S n) (A × A) (lsucc l)
TrAA = trunc-×.trunc {j = lsucc l} TrA TrA

module MA  = trunc-prop {j = lsucc l} {k = l} TrA
module MAA = trunc-prop {j = lsucc l} {k = l} TrAA
--    module MAL = trunc-elim {j = _} TrAA

{- There is some Yoneda hidden here that would enable us to express the final
equivalence e neatly as a sequence of trivial steps like in trunc-Σ;
unfortunately we lack the necessary category theoretic framework
in this code base. -}
module code (U : n -Type l) where
abstract
{- Large recursion used here.
Since we cannot talk about the truncation of a₀ == a₁ yet,
we instead talk about the continuation type (a₀ == a₁ → U) → U
for any n-type U instead. -}
code : ⟦ type TrAA ⟧ → n -Type l
code = rec {j = lsucc l} TrAA (n -Type-≤ l) (λ {(a₀ , a₁) → (a₀ == a₁ → ⟦ U ⟧) →-≤ U})

code-β : {a₀ a₁ : A} → ⟦ code (cons TrAA (a₀ , a₁)) ⟧
≃ ((a₀ == a₁ → ⟦ U ⟧) → ⟦ U ⟧)
code-β = coe-equiv (ap ⟦_⟧ (rec-β TrAA _))

-- We can encode a path in the truncation, ...
encode : {ta₀ ta₁ : ⟦ type TrA ⟧} → ta₀ == ta₁ → ⟦ code (ta₀ , ta₁) ⟧
encode idp = MA.elim (λ ta → raise (code (ta , ta)))
(λ _ → <– code-β (λ f → f idp)) _

--- ...reducing when coming from a path in the original type.
encode-β : {a₀ a₁ : A} (p : a₀ == a₁) (f : a₀ == a₁ → ⟦ U ⟧)
→ –> code-β (encode (ap (cons TrA) p)) f == f p
encode-β idp = app= (ap (–> code-β) (MA.elim-β _) ∙ <–-inv-r code-β _)

-- We can decode into the U-continuation of a path in the truncation, ...
decode : {ta₀ ta₁ : ⟦ type TrA ⟧}
→ ⟦ code (ta₀ , ta₁) ⟧ → (ta₀ == ta₁ → ⟦ U ⟧) → ⟦ U ⟧
decode = MAA.elim
(λ {(ta₀ , ta₁) → _ →-≤ (ta₀ == ta₁ → ⟦ U ⟧) →-≤ raise U})
(λ _ c g → –> code-β c (g ∘ ap (cons TrA))) _ where

-- ...reducing
decode-β : {a₀ a₁ : A} (c : ⟦ code (cons TrAA (a₀ , a₁)) ⟧)
(g : cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧)
→ decode c g == –> code-β c (g ∘ ap (cons TrA))
decode-β = app= ∘ app= (MAA.elim-β _)

-- encoding followed by decoding produces the expected continuation
decode-encode : {ta₀ ta₁ : ⟦ type TrA ⟧} (q : ta₀ == ta₁)
(g : ta₀ == ta₁ → ⟦ U ⟧) → decode (encode q) g == g q
decode-encode idp = MA.elim
(λ ta → Π-≤ (ta == ta → ⟦ U ⟧)
(λ g → Path-≤ (raise U) (decode (encode idp) g) (g idp)))
(λ _ g → decode-β (encode idp) g ∙ encode-β idp (g ∘ ap (cons TrA))) _

trunc : (a₀ a₁ : A) → trunc-ty n (a₀ == a₁) l
trunc a₀ a₁ = record
{ type = Path-< (type TrA) (cons TrA a₀) (cons TrA a₁)
; cons = ap (cons TrA)
; univ = snd ∘ e } where

e : (U : _) → (cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) ≃ (a₀ == a₁ → ⟦ U ⟧)
e U = equiv u v u-v v-u where
open code U

u : (cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) → a₀ == a₁ → ⟦ U ⟧
u g = g ∘ ap (cons TrA)

v : (a₀ == a₁ → ⟦ U ⟧) → cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧
v f q = –> code-β (encode q) f

u-v : (f : a₀ == a₁ → ⟦ U ⟧) → u (v f) == f
u-v f = λ= (λ p → encode-β p f)

v-u : (g : cons TrA a₀ == cons TrA a₁ → ⟦ U ⟧) → v (u g) == g
v-u g = λ= (λ q → ! (decode-β (encode q) g) ∙ decode-encode q g)
```