TT.Groupoid.SetInterp

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

module TT.Groupoid.SetInterp (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Groupoid.Syntax X Y

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

⟦ con ⟧ₛ = hSet ℓ-zero
⟦ sub Δ Γ ⟧ₛ = Lift (⟦ Δ ⟧ .fst → ⟦ Γ ⟧ .fst)
⟦ ty Γ ⟧ₛ = ⟦ Γ ⟧ .fst → hSet ℓ-zero
⟦ tm Γ A ⟧ₛ = Lift ((γ : ⟦ Γ ⟧ .fst) → ⟦ A ⟧ γ .fst)

⟦ isSetSub Δ Γ γ₀ γ₁ P₀ P₁ i j ⟧ =
  isOfHLevelLift 2 (isSetΠ λ δ → ⟦ Γ ⟧ .snd)
    ⟦ γ₀ ⟧ ⟦ γ₁ ⟧
    (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧)
    i j
⟦ γ ∘ δ ⟧ .lower θ = ⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ)
⟦ assoc γ δ θ i ⟧ .lower ξ = ⟦ γ ⟧ .lower (⟦ δ ⟧ .lower (⟦ θ ⟧ .lower ξ))
⟦ id ⟧ .lower γ = γ
⟦ idr γ i ⟧ .lower δ = ⟦ γ ⟧ .lower δ
⟦ idl γ i ⟧ .lower δ = ⟦ γ ⟧ .lower δ

⟦ isGroupoidTy Γ A₀ A₁ P₀ P₁ S₀ S₁ i j k ⟧ =
  isGroupoidΠ (λ γ → isGroupoidHSet)
    ⟦ A₀ ⟧ ⟦ A₁ ⟧
    (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧)
    (λ j k → ⟦ S₀ j k ⟧) (λ j k → ⟦ S₁ j k ⟧)
    i j k
⟦ A [ γ ]ᵀ ⟧ δ = ⟦ A ⟧ (⟦ γ ⟧ .lower δ)
⟦ []ᵀ-∘ A γ δ i ⟧ θ = ⟦ A ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))
⟦ []ᵀ-id A i ⟧ γ = ⟦ A ⟧ γ

⟦ isSetTm Γ A a₀ a₁ P₀ P₁ i j ⟧ =
  isOfHLevelLift 2 (isSetΠ λ γ → ⟦ A ⟧ γ .snd)
    ⟦ a₀ ⟧ ⟦ a₁ ⟧
    (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧)
    i j
⟦ a [ γ ]ᵗ ⟧ .lower δ = ⟦ a ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ []ᵗ-∘ a γ δ i ⟧ .lower θ = ⟦ a ⟧ .lower (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))
⟦ []ᵗ-id a i ⟧ .lower γ = ⟦ a ⟧ .lower γ

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

⟦ Γ ▹ A ⟧ =
  (Σ[ γ ∈ ⟦ Γ ⟧ .fst ] ⟦ A ⟧ γ .fst) , isSetΣ (⟦ Γ ⟧ .snd) λ γ → ⟦ A ⟧ γ .snd
⟦ 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
⟦ []ᵀ-⁺-∘ B γ δ i ⟧ (θ , a) = ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a)
⟦ []ᵀ-⁺-∘-filler B γ δ i j ⟧ (θ , a) = ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a)
⟦ ⁺-id i ⟧ .lower (γ , a) = γ , a
⟦ []ᵀ-⁺-id B i ⟧ (γ , a) = ⟦ B ⟧ (γ , a)
⟦ []ᵀ-⁺-id-filler B i j ⟧ (γ , a) = ⟦ B ⟧ (γ , a)

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

⟦ U ⟧ γ = X
⟦ U-[] γ i ⟧ δ = X
⟦ U-[]-∘ γ δ i j ⟧ =
  fill (λ j → _ → hSet ℓ-zero) {φ = i ∨ ~ i} (λ j _ ξ → X) (inS λ ξ → X) j
⟦ U-[]-id i j ⟧ γ = X
⟦ Â [ γ ]ᵘ ⟧ .lower δ = ⟦ Â ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ []ᵘ-filler Â γ i ⟧ .lower δ = ⟦ Â ⟧ .lower (⟦ γ ⟧ .lower δ)
⟦ []ᵘ-∘ Â γ δ i ⟧ .lower θ = ⟦ Â ⟧ .lower (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))
⟦ []ᵘ-id Â i ⟧ .lower γ = ⟦ Â ⟧ .lower γ
⟦ El Â ⟧ γ = Y (⟦ Â ⟧ .lower γ)
⟦ El-[] Â γ i ⟧ δ = Y (⟦ Â ⟧ .lower (⟦ γ ⟧ .lower δ))
⟦ El-[]-∘ Â γ δ i j ⟧ =
  fill (λ j → _ → hSet ℓ-zero)
    {φ = i ∨ ~ i}
    (λ j _ θ → Y (⟦ Â ⟧ .lower (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))))
    (inS λ θ → Y (⟦ Â ⟧ .lower (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ))))
    j
⟦ El-[]-id Â i j ⟧ γ = Y (⟦ Â ⟧ .lower γ)

⟦ Π A B ⟧ γ =
  ((a : ⟦ A ⟧ γ .fst) → ⟦ B ⟧ (γ , a) .fst) , isSetΠ λ a → ⟦ B ⟧ (γ , a) .snd
⟦ Π-[] A B γ i ⟧ δ =
  ((a : ⟦ A ⟧ (⟦ γ ⟧ .lower δ) .fst) → ⟦ B ⟧ (⟦ γ ⟧ .lower δ , a) .fst) ,
  isSetΠ λ a → ⟦ B ⟧ (⟦ γ ⟧ .lower δ , a) .snd
⟦ Π-[]-∘ A B γ δ i j ⟧ =
  fill (λ j → _ → hSet ℓ-zero)
    {φ = i ∨ ~ i}
    (λ j _ θ →
      ( (a : ⟦ A ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ)) .fst) →
        ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a) .fst) ,
      isSetΠ λ a → ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a) .snd)
    (inS λ θ →
      ( (a : ⟦ A ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ)) .fst) →
        ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a) .fst) ,
      isSetΠ λ a → ⟦ B ⟧ (⟦ γ ⟧ .lower (⟦ δ ⟧ .lower θ) , a) .snd)
    j
⟦ Π-[]-id A B i j ⟧ γ =
  ((a : ⟦ A ⟧ γ .fst) → ⟦ B ⟧ (γ , a) .fst) , isSetΠ λ a → ⟦ B ⟧ (γ , a) .snd
⟦ 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