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

-- "Real" Contexts, i.e. towers of real types

module context where

open import Level

_⊔₂ : Level → Level
i ⊔₂ = i ⊔ suc (suc zero)

Lift₂ : ∀ {i} → Set i → Set (i ⊔₂)
Lift₂ {i} X = Lift {i} {i ⊔₂} X

open import Data.Product
open import Data.Unit

-- Context is in Set2, because the types in our context will contain
-- the universe.  I can't figure out how to do this polymorphically.
data Context : Set₂ where
 ε : Context
 fam : (A : Set₁) → (B : A → Context) → Context

_⇨_ : ∀ {i} → Context → Set i → Set (i ⊔₂)
(ε ⇨ X) = Lift₂ X
(fam A B ⇨ X) = ((a : A) → (B a ⇨ X))

sum : Context → Set₁
sum ε = Lift ⊤
sum (fam A B) = Σ[ X ∈ A ] (sum (B X))

sumto⇨ : ∀ {i} (Γ : Context) (X : Set i) → (sum Γ → X) → (Γ ⇨ X)
sumto⇨ ε X P =  lift (P (lift tt))
sumto⇨ (fam A B) X P = λ a → sumto⇨ (B a) X (λ s → P (a , s))

extend : (Γ : Context) → (Γ ⇨ Set₁) → Context
extend ε (lift X) = fam X (λ x → ε)
extend (fam A B) Y = fam A (λ a → extend (B a) (Y a))

sumextend : (Γ : Context) → (X : sum Γ → Set₁) → sum (extend Γ (sumto⇨ Γ Set₁ X)) → Σ[ x ∈ sum Γ ] X x
sumextend ε X s = (lift tt , proj₁ s)
sumextend (fam A B) X (a , b) =  ((a , proj₁ (sumextend (B a) (λ b → X (a , b)) b)) ,  proj₂ (sumextend (B a) (λ b → X (a , b)) b))