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

{- The type of all types in some universe with a fixed truncation level
   behaves almost like a universe itself. In this utility module, we develop
   some notation for efficiently working with this pseudo-universe.
   It will lead to considerably more briefer and more comprehensible proofs. -}
module Universe.Utility.TruncUniverse where

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

open import Universe.Utility.General


module _ {n : ℕ₋₂} where
  ⟦_⟧ :  {i}  n -Type i  Type i
   (B , _)  = B

module _ {n : ℕ₋₂} where
  Lift-≤ :  {i j}  n -Type i  n -Type (i  j)
  Lift-≤ {i} {j} (A , h) = (Lift {j = j} A , equiv-preserves-level (lift-equiv ⁻¹) h)

  raise :  {i}  n -Type i  S n -Type i
  raise (A , h) = (A , raise-level n h)

  raise-≤T :  {i} {m n : ℕ₋₂}  m ≤T n  m -Type i  n -Type i
  raise-≤T p (A , h) = (A , raise-level-≤T p h)

  ⊤-≤ : n -Type lzero
  ⊤-≤ = ( , raise-level-≤T (-2≤T n) Unit-is-contr)

  Π-≤ :  {i j} (A : Type i)  (A  n -Type j)  n -Type (i  j)
  Π-≤ A B = (Π A (fst  B) , Π-level (snd  B))

  infixr 2 _→-≤_

  _→-≤_ :  {i j}  Type i  n -Type j  n -Type (i  j)
  A →-≤ B = Π-≤ A  _  B)

  Σ-≤ :  {i j} (A : n -Type i)  ( A   n -Type j)  n -Type (i  j)
  Σ-≤ A B = (Σ  A   a   B a ) , Σ-level (snd A) (snd  B))

  infixr 4 _×-≤_

  _×-≤_ :  {i j}  n -Type i  n -Type j  n -Type (i  j)
  A ×-≤ B = Σ-≤ A  _  B)

  Path-< :  {i} (A : S n -Type i) (x y :  A )  n -Type i
  Path-< A x y = (x == y , snd A _ _)

  Path-≤ :  {i} (A : n -Type i) (x y :  A )  n -Type i
  Path-≤ A x y = Path-< (raise A) x y

  _≃-≤_ :  {i j} (A : n -Type i) (B : n -Type j)  n -Type (i  j)
  A ≃-≤ B = ( A    B  , ≃-level (snd A) (snd B))

_-Type-≤_ : (n : ℕ₋₂) (i : ULevel)  S n -Type lsucc i
n -Type-≤ i = (n -Type i , n -Type-level i)