TT.Set.ToFromGroupoid

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

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

open import TT.Set.Syntax X Y
open import TT.Set.ElimProp X Y
import TT.Set.ToGroupoid X Y as SG
import TT.Groupoid.ToSet X Y as GS
open DModel

M : DModel
M .Conᴹ Γ = GS.⟦ SG.⟦ Γ ⟧ ⟧ ≡ Γ
M .Subᴹ Δᴹ Γᴹ γ = PathP (λ i → Sub (Δᴹ i) (Γᴹ i)) GS.⟦ SG.⟦ γ ⟧ ⟧ γ
M .isPropSubᴹ Δᴹ Γᴹ γ = isOfHLevelPathP' 1 (isSetSub _ _) _ _
M ._∘ᴹ_ γᴹ δᴹ i = γᴹ i ∘ δᴹ i
M .idᴹ i = id

M .Tyᴹ Γᴹ A = PathP (λ i → Ty (Γᴹ i)) GS.⟦ SG.⟦ A ⟧ ⟧ A
M .isPropTyᴹ Γᴹ A = isOfHLevelPathP' 1 (isSetTy _) _ _
M ._[_]ᵀᴹ Aᴹ γᴹ i = Aᴹ i [ γᴹ i ]ᵀ
M .Tmᴹ Γᴹ Aᴹ a = PathP (λ i → Tm (Γᴹ i) (Aᴹ i)) GS.⟦ SG.⟦ a ⟧ ⟧ a
M .isPropTmᴹ Γᴹ Aᴹ a = isOfHLevelPathP' 1 (isSetTm _ _) _ _
M ._[_]ᵗᴹ aᴹ γᴹ i = aᴹ i [ γᴹ i ]ᵗ

M .◇ᴹ i = ◇
M .εᴹ i = ε
M ._▹ᴹ_ Γᴹ Aᴹ i = Γᴹ i ▹ Aᴹ i
M .pᴹ i = p
M .qᴹ i = q
M ._⁺ᴹ γᴹ i = γᴹ i ⁺
M .⟨_⟩ᴹ aᴹ i = ⟨ aᴹ i ⟩

M .Uᴹ i = U
M .Elᴹ Âᴹ i = El (Âᴹ i)
M .Πᴹ Aᴹ Bᴹ i = Π (Aᴹ i) (Bᴹ i)
M .appᴹ fᴹ i = app (fᴹ i)
M .lamᴹ bᴹ i = lam (bᴹ i)

M .in-Xᴹ x i = in-X x
M .in-Yᴹ y i = in-Y y

open Elim M public