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