{-# 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. -}
      duniv : is-equiv  (f :  Π-≤  type  P )  f  cons)
      duniv = snd eqv