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

{- After a few preliminary lemmata about representing dependent functions,
this module will derive the dependent universal property of
our truncations (defined later) from the non-dependent one. -}
module Universe.Trunc.Universal where

open import lib.Basics
open import lib.Equivalences2
open import lib.NType2
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Unit

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

-- In the fibration fst : Σ A B → A, the fiber over a is given by B a.
trivial-fibers : ∀ {i j} {A : Type i} {B : A → Type j} (a : A)
→ B a ≃ Σ (Σ A B) (λ s → a == fst s)
trivial-fibers {A = A} {B} a =
B a                               ≃⟨ Σ₁-Unit ⁻¹ ⟩
Σ ⊤ (λ _ → B a)                   ≃⟨ equiv-Σ-fst _ (snd (e ⁻¹)) ⟩
Σ (Σ A (λ s → a == s)) (B ∘ fst)  ≃⟨ Σ-comm-snd ⟩
Σ (Σ A B) (λ s → a == fst s)      ≃∎ where

e : Σ A (λ s → a == s) ≃ ⊤
e = contr-equiv-Unit (pathfrom-is-contr a)

{- Liftings of u : Π A B through fst : {a : A} → Σ (B a) (C a) → B a
correponds to dependent functions from (a : A) to C a (u a).

As mentioned in the article, we will make use only of a special case:
liftings of u : A → B through fst : Σ B C → B correponds to
dependent functions from (a : A) to C a. -}
Π-as-liftings : ∀ {i j k} {A : Type i} {B : A → Type j}
(u : Π A B) {C : (a : A) → B a → Type k} → _
Π-as-liftings {A = A} {B} u {C} =
Π A (λ a → C a (u a))
≃⟨ trivial-fibers u ⟩
Σ (Σ (Π A B) (λ r → Π A (λ a → C a (r a)))) (λ {(r , _) → u == r})
≃⟨ equiv-Σ-fst _ (snd choice) ⁻¹ ⟩
Σ (Π A (λ a → Σ (B a) (C a))) (λ s → u == fst ∘ s)
≃∎

{- Dependent functions from (a : A) to B a
are given by sections of fst : Σ A B → A.

Noting that sections are non-dependent functions, this folklore insight
is a main ingredient in passing from non-dependent universal property
to the dependent one. -}
Π-as-sections : ∀ {i j} {A : Type i} {B : A → Type j}
→ Π A B ≃ Σ (A → Σ A B) (λ s → idf _ == fst ∘ s)
Π-as-sections = Π-as-liftings (idf _)

{- Fix a truncation level n and a Type A. We will examine what it means
for an n-type 'type' with constructor cons : A → ⟦ type ⟧
to have the universal property of the n-truncation of A. -}
module _ {i} {n : ℕ₋₂} {A : Type i}
(type : n -Type i) (cons : A → ⟦ type ⟧) where

{- The (non-dependent) universal property:
λ f → f ∘ cons  iinduces  type → X ≃ A → X -}
univ-Type : ∀ (k : ULevel) → Type (i ⊔ lsucc k)
univ-Type k = (X : n -Type k) → is-equiv
{A = ⟦ type ⟧ → ⟦ X ⟧}
{B = A → ⟦ X ⟧}
(λ f → f ∘ cons)

{- The dependent universal property:
λ f → f ∘ cons  induces  ((a : type) → X a) ≃ ((a : A) → X (cons a)) -}
duniv-Type : ∀ (k : ULevel) → Type (i ⊔ lsucc k)
duniv-Type k = (X : ⟦ type ⟧ → n -Type k) → is-equiv
{A = Π ⟦ type ⟧ (⟦_⟧ ∘ X )}
{B = Π A (⟦_⟧ ∘ X ∘ cons)}
(λ f → f ∘ cons)

{- If the universal property holds for a certain elimination universe U_j₂,
then also for an elimination universe U_j₁ with j₁ ≤ j₂.
Agda does not support specifying ordering relations between
universe levels directly, but we may simulate j₁ ≤ j₂
by decomposing j₁ = k₁ and j₂ = k₁ ⊔ k₂. -}
univ-lower : ∀ {k₁} (k₂ : ULevel) → univ-Type (k₁ ⊔ k₂) → univ-Type k₁
univ-lower {k₁} k₂ univ X = transport (λ z → is-equiv (λ f → z ∘ f ∘ cons))
(λ= (<–-inv-r e)) hup where
e : Lift {j = k₁ ⊔ k₂} ⟦ X ⟧ ≃ ⟦ X ⟧
e = lift-equiv

hup : is-equiv (λ f → –> e ∘ <– e ∘ f ∘ cons)
hup = pre∘-is-equiv (snd e)
∘ise univ (Lift-≤ X)
∘ise pre∘-is-equiv (snd (e ⁻¹))

{- We will now prove the main lemma of this section:
The (non-dependent) universal property implies the dependent one. -}
module with-univ {j} (univ : univ-Type (i ⊔ j)) (P : ⟦ type ⟧ → n -Type j) where

-- abbreviating the underlying types (for readability)
T = ⟦ type ⟧
Q = ⟦_⟧ ∘ P

{- As is usual for deriving dependent eliminators, the crux for deriving
the dependent universal property is to first transform the *dependent*
function spaces into *non-dependent* sections/liftings according to
the lemmata above. -}
eqv : Π T Q ≃ Π A (Q ∘ cons)
eqv = Π-as-liftings cons ⁻¹ ∘e eqv-liftings ∘e Π-as-liftings (idf _) where

{- Our goal now is an equivalence of Σ-types where the first components
fit the template of the *non-dependent* universal property. -}
eqv-liftings : Σ (T → Σ T Q) (λ s → idf _ == fst ∘ s)
≃ Σ (A → Σ T Q) (λ t → cons  == fst ∘ t)
eqv-liftings = equiv-Σ' (_ , univ (Σ-≤ type P)) lem where

{- What remains is just the universal property applied to X itself,
and then switching to path spaces. In the usual derivation of
dependent elimination, this corresponds to application of
the η-rule to the identity function. -}
lem : (s : T → Σ T Q) → (idf _ == fst ∘ s) ≃ (cons == fst ∘ s ∘ cons)
lem s = equiv-ap (_ , univ-lower (i ⊔ j) univ type) (idf _) (fst ∘ s)

{- Due to construction of the above equivalence via conjugation of
the (non-dependent) universal property (on the first component),
its action ends up being precisely composition with the constructor.
Because of technical limitations of the Agda type-checker,
we encapsulate the result in an abstract block to prevent
the type checker from unnecessarily unfolding its value later on. -}
abstract
duniv : is-equiv (λ (f : ⟦ Π-≤ ⟦ type ⟧ P ⟧) → f ∘ cons)
duniv = snd eqv
```