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

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

import TT.Groupoid.Syntax X Y as G
open import TT.Set.Syntax X Y

module S where
  private variable
    Γ Δ Θ : Con
    A : Ty Γ

  []ᵀ-⁺-∘ :
    (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    PathP (λ i → Ty (Θ ▹ []ᵀ-∘ A γ δ i))
      (B [ (γ ∘ δ) ⁺ ]ᵀ)
      (B [ γ ⁺ ]ᵀ [ δ ⁺ ]ᵀ)
  []ᵀ-⁺-∘ {A} {Θ} B γ δ = λ i → filler i1 i
    module []ᵀ-⁺-∘ where
    filler : I → (i : I) → Ty (Θ ▹ []ᵀ-∘ A γ δ i)
    filler j i =
      hfill
        (λ where
          j (i = i0) → B [ (γ ∘ δ) ⁺ ]ᵀ
          j (i = i1) → []ᵀ-∘ B (γ ⁺) (δ ⁺) j)
        (inS (B [ ⁺-∘ γ δ i ]ᵀ))
        j

  []ᵀ-⁺-id :
    (B : Ty (Γ ▹ A)) → PathP (λ i → Ty (Γ ▹ []ᵀ-id A i)) (B [ id ⁺ ]ᵀ) B
  []ᵀ-⁺-id {Γ} {A} B = λ i → filler i1 i
    module []ᵀ-⁺-id where
    filler : I → (i : I) → Ty (Γ ▹ []ᵀ-id A i)
    filler j i =
      hfill
        (λ where
          j (i = i0) → B [ id ⁺ ]ᵀ
          j (i = i1) → []ᵀ-id B j)
        (inS (B [ ⁺-id i ]ᵀ))
        j

  []ᵘ-∘ :
    (Â : Tm Γ U) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → Â [ γ ∘ δ ]ᵘ ≡ Â [ γ ]ᵘ [ δ ]ᵘ
  []ᵘ-∘ {Θ} Â γ δ i =
    comp
      (λ j →
        Tm Θ
          (isSet→isSet' (isSetTy Θ)
            ([]ᵀ-∘ U γ δ)
            refl
            (U-[] (γ ∘ δ))
            (cong _[ δ ]ᵀ (U-[] γ) ∙ U-[] δ)
            j i))
      (λ where
        j (i = i0) → []ᵘ-filler  (γ ∘ δ) j
        j (i = i1) →
          comp
            (λ i → Tm Θ (compPath-filler (cong _[ δ ]ᵀ (U-[] γ)) (U-[] δ) i j))
            (λ where
              i (j = i0) → Â [ γ ]ᵗ [ δ ]ᵗ
              i (j = i1) → []ᵘ-filler (Â [ γ ]ᵘ) δ i)
            ([]ᵘ-filler  γ j [ δ ]ᵗ))
      ([]ᵗ-∘ Â γ δ i)

  []ᵘ-id : (Â : Tm Γ U) → Â [ id ]ᵘ ≡ Â
  []ᵘ-id {Γ} Â i =
    comp
      (λ j → Tm Γ (isSet→isSet' (isSetTy Γ) ([]ᵀ-id U) refl (U-[] id) refl j i))
      (λ where
        j (i = i0) → []ᵘ-filler  id j
        j (i = i1) → Â)
      ([]ᵗ-id  i)

open S

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

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

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

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

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

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

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

⟦ G.⁺-∘ γ δ i ⟧ = ⁺-∘ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ G.[]ᵀ-⁺-∘ B γ δ i ⟧ = []ᵀ-⁺-∘ ⟦ B ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ G.[]ᵀ-⁺-∘-filler B γ δ j i ⟧ = []ᵀ-⁺-∘.filler ⟦ B ⟧ ⟦ γ ⟧ ⟦ δ ⟧ j i
⟦ G.⁺-id i ⟧ = ⁺-id i
⟦ G.[]ᵀ-⁺-id B i ⟧ = []ᵀ-⁺-id ⟦ B ⟧ i
⟦ G.[]ᵀ-⁺-id-filler B j i ⟧ = []ᵀ-⁺-id.filler ⟦ B ⟧ j i

⟦ G.p-⁺ γ i ⟧ = p-⁺ ⟦ γ ⟧ i
⟦ G.[]ᵀ-p-⁺ B γ i ⟧ = []ᵀ-p-⁺ ⟦ B ⟧ ⟦ γ ⟧ i
⟦ G.[]ᵀ-p-⁺-filler B γ j i ⟧ =
  isSet→isSet' (isSetTy _)
    (cong (⟦ B ⟧ [_]ᵀ) (p-⁺ ⟦ γ ⟧))
    ([]ᵀ-p-⁺ ⟦ B ⟧ ⟦ γ ⟧)
    ([]ᵀ-∘ ⟦ B ⟧ p (⟦ γ ⟧ ⁺))
    ([]ᵀ-∘ ⟦ B ⟧ ⟦ γ ⟧ p)
    j i
⟦ G.q-⁺ γ i ⟧ = q-⁺ ⟦ γ ⟧ i

⟦ G.p-⟨⟩ a i ⟧ = p-⟨⟩ ⟦ a ⟧ i
⟦ G.[]ᵀ-p-⟨⟩ B a i ⟧ = []ᵀ-p-⟨⟩ ⟦ B ⟧ ⟦ a ⟧ i
⟦ G.[]ᵀ-p-⟨⟩-filler B a j i ⟧ =
  isSet→isSet' (isSetTy _)
    (cong (⟦ B ⟧ [_]ᵀ) (p-⟨⟩ ⟦ a ⟧))
    ([]ᵀ-p-⟨⟩ ⟦ B ⟧ ⟦ a ⟧)
    ([]ᵀ-∘ ⟦ B ⟧ p ⟨ ⟦ a ⟧ ⟩)
    ([]ᵀ-id ⟦ B ⟧)
    j i
⟦ G.q-⟨⟩ a i ⟧ = q-⟨⟩ ⟦ a ⟧ i

⟦ G.U ⟧ = U
⟦ G.U-[] γ i ⟧ = U-[] ⟦ γ ⟧ i
⟦ G.U-[]-∘ γ δ j i ⟧ =
  isSet→isSet' (isSetTy _)
    ([]ᵀ-∘ U ⟦ γ ⟧ ⟦ δ ⟧)
    refl
    (U-[] (⟦ γ ⟧ ∘ ⟦ δ ⟧))
    (compPathP' {A = Unit} {p = refl} {q = refl}
      (cong _[ ⟦ δ ⟧ ]ᵀ (U-[] ⟦ γ ⟧))
      (U-[] ⟦ δ ⟧))
    j i
⟦ G.U-[]-id j i ⟧ = isSet→isSet' (isSetTy _) ([]ᵀ-id U) refl (U-[] id) refl j i

⟦ Â G.[ γ ]ᵘ ⟧ = ⟦ Â ⟧ [ ⟦ γ ⟧ ]ᵘ
⟦ G.[]ᵘ-filler  γ i ⟧ = []ᵘ-filler ⟦  ⟧ ⟦ γ ⟧ i
⟦ G.[]ᵘ-∘ Â γ δ i ⟧ = []ᵘ-∘ ⟦ Â ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i
⟦ G.[]ᵘ-id  i ⟧ = []ᵘ-id ⟦  ⟧ i

⟦ G.El  ⟧ = El ⟦  ⟧
⟦ G.El-[] Â γ i ⟧ = El-[] ⟦ Â ⟧ ⟦ γ ⟧ i
⟦ G.El-[]-∘ Â γ δ i j ⟧ =
  isSet→isSet' (isSetTy _)
    ([]ᵀ-∘ (El ⟦ Â ⟧) ⟦ γ ⟧ ⟦ δ ⟧)
    (cong El ([]ᵘ-∘ ⟦ Â ⟧ ⟦ γ ⟧ ⟦ δ ⟧))
    (El-[] ⟦ Â ⟧ (⟦ γ ⟧ ∘ ⟦ δ ⟧))
    (compPathP' {A = Unit} {p = refl} {q = refl}
      (cong _[ ⟦ δ ⟧ ]ᵀ (El-[] ⟦ Â ⟧ ⟦ γ ⟧))
      (El-[] (⟦ Â ⟧ [ ⟦ γ ⟧ ]ᵘ) ⟦ δ ⟧))
    i j
⟦ G.El-[]-id  i j ⟧ =
  isSet→isSet' (isSetTy _)
    ([]ᵀ-id (El ⟦ Â ⟧))
    (cong El ([]ᵘ-id ⟦ Â ⟧))
    (El-[] ⟦ Â ⟧ id)
    refl
    i j

⟦ G.Π A B ⟧ = Π ⟦ A ⟧ ⟦ B ⟧
⟦ G.Π-[] A B γ i ⟧ = Π-[] ⟦ A ⟧ ⟦ B ⟧ ⟦ γ ⟧ i
⟦ G.Π-[]-∘ A B γ δ i j ⟧ =
  isSet→isSet' (isSetTy _)
    ([]ᵀ-∘ (Π ⟦ A ⟧ ⟦ B ⟧) ⟦ γ ⟧ ⟦ δ ⟧)
    (cong₂ Π ([]ᵀ-∘ ⟦ A ⟧ ⟦ γ ⟧ ⟦ δ ⟧) ([]ᵀ-⁺-∘ ⟦ B ⟧ ⟦ γ ⟧ ⟦ δ ⟧))
    (Π-[] ⟦ A ⟧ ⟦ B ⟧ (⟦ γ ⟧ ∘ ⟦ δ ⟧))
    (compPathP' {A = Unit} {p = refl} {q = refl}
      (cong _[ ⟦ δ ⟧ ]ᵀ (Π-[] ⟦ A ⟧ ⟦ B ⟧ ⟦ γ ⟧))
      (Π-[] (⟦ A ⟧ [ ⟦ γ ⟧ ]ᵀ) (⟦B⟧ [ ⟦ γ ⟧ ⁺ ]ᵀ) ⟦ δ ⟧))
    i j
  where
  ⟦B⟧ : Ty (_ ▹ _)
  ⟦B⟧ = ⟦ B ⟧
⟦ G.Π-[]-id A B i j ⟧ =
  isSet→isSet' (isSetTy _)
    ([]ᵀ-id (Π ⟦ A ⟧ ⟦ B ⟧))
    (cong₂ Π ([]ᵀ-id ⟦ A ⟧) ([]ᵀ-⁺-id ⟦ B ⟧))
    (Π-[] ⟦ A ⟧ ⟦ B ⟧ id)
    refl
    i j

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

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