open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.HLevels
open import Cubical.Data.Unit

module TT.Wild.TypeInterp (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Wild.Syntax X Y

⟦_⟧ₛ : Sort → Type₁
⟦_⟧ : ∀ {S} → EL S → ⟦ S ⟧ₛ

⟦ con ⟧ₛ = Type
⟦ sub Δ Γ ⟧ₛ = Lift (⟦ Δ ⟧ → ⟦ Γ ⟧)
⟦ ty Γ ⟧ₛ = ⟦ Γ ⟧ → Type
⟦ tm Γ A ⟧ₛ = Lift ((γ : ⟦ Γ ⟧) → ⟦ A ⟧ γ)

⟦ γ ∘ δ ⟧ .lower θ = ⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ)
⟦ assoc γ δ θ i ⟧ .lower ξ = ⟦ γ ⟧ .lower (⟦ δ ⟧ .lower (⟦ θ ⟧ .lower ξ))
⟦ id ⟧ .lower γ = γ
⟦ idr γ i ⟧ .lower δ = ⟦ γ ⟧ .lower δ
⟦ idl γ i ⟧ .lower δ = ⟦ γ ⟧ .lower δ

⟦ A [ γ ]ᵀ ⟧ δ = ⟦ A ⟧ (⟦ γ ⟧ .lower δ)
⟦ []ᵀ-∘ A γ δ i ⟧ θ = ⟦ A ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))
⟦ []ᵀ-id A i ⟧ γ = ⟦ A ⟧ γ
⟦ a [ γ ]ᵗ ⟧ .lower δ = ⟦ a ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ []ᵗ-∘ a γ δ i ⟧ .lower θ = ⟦ a ⟧ .lower (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))
⟦ []ᵗ-id a i ⟧ .lower γ = ⟦ a ⟧ .lower γ

⟦ ◇ ⟧ = Unit
⟦ ε ⟧ .lower γ = tt
⟦ ε-∘ γ i ⟧ .lower δ = tt
⟦ ◇-η i ⟧ .lower tt = tt

⟦ Γ ▹ A ⟧ = Σ[ γ ∈ ⟦ Γ ⟧ ] ⟦ A ⟧ γ
⟦ p ⟧ .lower (γ , a) = γ
⟦ q ⟧ .lower (γ , a) = a
⟦ γ ⁺ ⟧ .lower (δ , a) = ⟦ γ ⟧ .lower δ , a
⟦ ⟨ a ⟩ ⟧ .lower γ = γ , ⟦ a ⟧ .lower γ
⟦ ⟨⟩-∘ a γ i ⟧ .lower δ = ⟦ γ ⟧ .lower δ , ⟦ a ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ ▹-η i ⟧ .lower (γ , a) = γ , a
⟦ ⁺-∘ γ δ i ⟧ .lower (θ , a) = ⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a
⟦ ⁺-id i ⟧ .lower (γ , a) = γ , a

⟦ p-⁺ γ i ⟧ .lower (δ , a) = ⟦ γ ⟧ .lower δ
⟦ []ᵀ-p-⁺ B γ i ⟧ (δ , a) = ⟦ B ⟧ (⟦ γ ⟧ .lower δ)
⟦ q-⁺ γ i ⟧ .lower (δ , a) = a
⟦ p-⟨⟩ a i ⟧ .lower γ = γ
⟦ []ᵀ-p-⟨⟩ B a i ⟧ γ = ⟦ B ⟧ γ
⟦ q-⟨⟩ a i ⟧ .lower γ = ⟦ a ⟧ .lower γ

⟦ U ⟧ γ = X .fst
⟦ U-[] γ i ⟧ δ = X .fst
⟦ Â [ γ ]ᵘ ⟧ .lower δ = ⟦ Â ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ []ᵘ-filler  γ i ⟧ .lower δ = ⟦  ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ El  ⟧ γ = Y (⟦  ⟧ .lower γ) .fst
⟦ El-[] Â γ i ⟧ δ = Y (⟦ Â ⟧ .lower (⟦ γ ⟧ .lower δ)) .fst

⟦ Π A B ⟧ γ = (a : ⟦ A ⟧ γ) → ⟦ B ⟧ (γ , a)
⟦ Π-[] A B γ i ⟧ δ = (a : ⟦ A ⟧ (⟦ γ ⟧ .lower δ)) → ⟦ B ⟧ (⟦ γ ⟧ .lower δ , a)
⟦ app f ⟧ .lower (γ , a) = ⟦ f ⟧ .lower γ a
⟦ lam b ⟧ .lower γ a = ⟦ b ⟧ .lower (γ , a)
⟦ lam-[] b γ i ⟧ .lower δ a = ⟦ b ⟧ .lower (⟦ γ ⟧ .lower δ , a)
⟦ Π-β b i ⟧ .lower (γ , a) = ⟦ b ⟧ .lower (γ , a)
⟦ Π-η f i ⟧ .lower γ a = ⟦ f ⟧ .lower γ a

⟦ in-X x ⟧ .lower tt = x
⟦ in-Y y ⟧ .lower tt = y