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

module TT.Set.ToGroupoid (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

import TT.Set.Syntax X Y as S
open import TT.Groupoid.Syntax X Y
open import TT.Groupoid.NTy X Y

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

⟦ S.con ⟧ₛ = con
⟦ S.sub Δ Γ ⟧ₛ = sub ⟦ Δ ⟧ ⟦ Γ ⟧
⟦ S.ty A ⟧ₛ = ty ⟦ A ⟧
⟦ S.tm Γ A ⟧ₛ = tm ⟦ Γ ⟧ ⟦ A ⟧

⟦ S.isSetSub Δ Γ γ₀ γ₁ P₀ P₁ i j ⟧ =
  isSetSub ⟦ Δ ⟧ ⟦ Γ ⟧ ⟦ γ₀ ⟧ ⟦ γ₁ ⟧ (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧) i j
⟦ γ S.∘ δ ⟧ = ⟦ γ ⟧ ∘ ⟦ δ ⟧
⟦ S.assoc γ δ θ i ⟧ = assoc ⟦ γ ⟧ ⟦ δ ⟧ ⟦ θ ⟧ i
⟦ S.id ⟧ = id
⟦ S.idr γ i ⟧ = idr ⟦ γ ⟧ i
⟦ S.idl γ i ⟧ = idl ⟦ γ ⟧ i

⟦ S.isSetTy Γ A₀ A₁ P₀ P₁ i j ⟧ =
  isSetTy ⟦ Γ ⟧ ⟦ A₀ ⟧ ⟦ A₁ ⟧ (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧) i j
⟦ A S.[ γ ]ᵀ ⟧ = ⟦ A ⟧ [ ⟦ γ ⟧ ]ᵀ
⟦ S.[]ᵀ-∘ A γ δ i ⟧ = []ᵀ-∘ ⟦ A ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ S.[]ᵀ-id A i ⟧ = []ᵀ-id ⟦ A ⟧ i

⟦ S.isSetTm Γ A a₀ a₁ P₀ P₁ i j ⟧ =
  isSetTm ⟦ Γ ⟧ ⟦ A ⟧ ⟦ a₀ ⟧ ⟦ a₁ ⟧ (λ j → ⟦ P₀ j ⟧) (λ j → ⟦ P₁ j ⟧) i j
⟦ a S.[ γ ]ᵗ ⟧ = ⟦ a ⟧ [ ⟦ γ ⟧ ]ᵗ
⟦ S.[]ᵗ-∘ a γ δ i ⟧ = []ᵗ-∘ ⟦ a ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ S.[]ᵗ-id a i ⟧ = []ᵗ-id ⟦ a ⟧ i

⟦ S.◇ ⟧ = ◇
⟦ S.ε ⟧ = ε
⟦ S.ε-∘ γ i ⟧ = ε-∘ ⟦ γ ⟧ i
⟦ S.◇-η i ⟧ = ◇-η i

⟦ Γ S.▹ A ⟧ = ⟦ Γ ⟧ ▹ ⟦ A ⟧
⟦ S.p ⟧ = p
⟦ S.q ⟧ = q
⟦ γ S.⁺ ⟧ = ⟦ γ ⟧ ⁺
⟦ S.⟨ a ⟩ ⟧ = ⟨ ⟦ a ⟧ ⟩
⟦ S.⟨⟩-∘ a γ i ⟧ = ⟨⟩-∘ ⟦ a ⟧ ⟦ γ ⟧ i
⟦ S.▹-η i ⟧ = ▹-η i

⟦ S.⁺-∘ γ δ i ⟧ = ⁺-∘ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ S.⁺-id i ⟧ = ⁺-id i
⟦ S.p-⁺ γ i ⟧ = p-⁺ ⟦ γ ⟧ i
⟦ S.[]ᵀ-p-⁺ B γ i ⟧ = []ᵀ-p-⁺ ⟦ B ⟧ ⟦ γ ⟧ i
⟦ S.q-⁺ γ i ⟧ = q-⁺ ⟦ γ ⟧ i
⟦ S.p-⟨⟩ a i ⟧ = p-⟨⟩ ⟦ a ⟧ i
⟦ S.[]ᵀ-p-⟨⟩ B a i ⟧ = []ᵀ-p-⟨⟩ ⟦ B ⟧ ⟦ a ⟧ i
⟦ S.q-⟨⟩ a i ⟧ = q-⟨⟩ ⟦ a ⟧ i

⟦ S.U ⟧ = U
⟦ S.U-[] γ i ⟧ = U-[] ⟦ γ ⟧ i
⟦ Â S.[ γ ]ᵘ ⟧ = ⟦ Â ⟧ [ ⟦ γ ⟧ ]ᵘ
⟦ S.[]ᵘ-filler  γ i ⟧ = []ᵘ-filler ⟦  ⟧ ⟦ γ ⟧ i
⟦ S.El  ⟧ = El ⟦  ⟧
⟦ S.El-[] Â γ i ⟧ = El-[] ⟦ Â ⟧ ⟦ γ ⟧ i

⟦ S.Π A B ⟧ = Π ⟦ A ⟧ ⟦ B ⟧
⟦ S.Π-[] A B γ i ⟧ = Π-[] ⟦ A ⟧ ⟦ B ⟧ ⟦ γ ⟧ i
⟦ S.app f ⟧ = app ⟦ f ⟧
⟦ S.lam b ⟧ = lam ⟦ b ⟧
⟦ S.lam-[] b γ i ⟧ = lam-[] ⟦ b ⟧ ⟦ γ ⟧ i
⟦ S.Π-β b i ⟧ = Π-β ⟦ b ⟧ i
⟦ S.Π-η f i ⟧ = Π-η ⟦ f ⟧ i

⟦ S.in-X x ⟧ = in-X x
⟦ S.in-Y y ⟧ = in-Y y