{-# 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)