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

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

open import TT.Set.Syntax X Y
import TT.Set.ToGroupoid X Y as SetToGroupoid
import TT.Groupoid.SetInterp X Y as GroupoidSetInterp

⟦_⟧ₛ : Sort → Type₁
⟦ S ⟧ₛ = GroupoidSetInterp.⟦ SetToGroupoid.⟦ S ⟧ₛ ⟧ₛ

⟦_⟧ : ∀ {S} → EL S → ⟦ S ⟧ₛ
⟦ s ⟧ = GroupoidSetInterp.⟦ SetToGroupoid.⟦ s ⟧ ⟧