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

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

open import TT.Groupoid.Syntax X Y

private variable
  Γ Δ Θ : Con
  A B : Ty Γ

record DModel : Type₁ where
  no-eta-equality

  infixl  _[_]ᵀᴹ
  field
    Tyᴹ : (Γ : Con) → Ty Γ → Type
    isSetTyᴹ : (Γ : Con) (A : Ty Γ) → isSet (Tyᴹ Γ A)

    _[_]ᵀᴹ : Tyᴹ Γ A → (γ : Sub Δ Γ) → Tyᴹ Δ (A [ γ ]ᵀ)
    []ᵀ-∘ᴹ :
      (Aᴹ : Tyᴹ Γ A) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
      PathP (λ i → Tyᴹ Θ ([]ᵀ-∘ A γ δ i))
        (Aᴹ [ γ ∘ δ ]ᵀᴹ)
        (Aᴹ [ γ ]ᵀᴹ [ δ ]ᵀᴹ)
    []ᵀ-idᴹ :
      (Aᴹ : Tyᴹ Γ A) → PathP (λ i → Tyᴹ Γ ([]ᵀ-id A i)) (Aᴹ [ id ]ᵀᴹ) Aᴹ

    Uᴹ : Tyᴹ Γ U
    U-[]ᴹ : (γ : Sub Δ Γ) → PathP (λ i → Tyᴹ Δ (U-[] γ i)) (Uᴹ [ γ ]ᵀᴹ) Uᴹ

    Elᴹ : (Â : Tm Γ U) → Tyᴹ Γ (El Â)
    El-[]ᴹ :
      (Â : Tm Γ U) (γ : Sub Δ Γ) →
      PathP (λ i → Tyᴹ Δ (El-[] Â γ i)) (Elᴹ Â [ γ ]ᵀᴹ) (Elᴹ (Â [ γ ]ᵘ))

    Πᴹ : Tyᴹ Γ A → Tyᴹ (Γ ▹ A) B → Tyᴹ Γ (Π A B)
    Π-[]ᴹ :
      (Aᴹ : Tyᴹ Γ A) (Bᴹ : Tyᴹ (Γ ▹ A) B) (γ : Sub Δ Γ) →
      PathP (λ i → Tyᴹ Δ (Π-[] A B γ i))
        (Πᴹ Aᴹ Bᴹ [ γ ]ᵀᴹ)
        (Πᴹ (Aᴹ [ γ ]ᵀᴹ) (Bᴹ [ γ ⁺ ]ᵀᴹ))

  []ᵀ-⁺-∘ᴹ-filler :
    (Bᴹ : Tyᴹ (Γ ▹ A) B) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    (j i : I) → Tyᴹ (Θ ▹ []ᵀ-∘ A γ δ i) ([]ᵀ-⁺-∘-filler B γ δ j i)
  []ᵀ-⁺-∘ᴹ-filler Bᴹ γ δ j i =
    fill (λ j → Tyᴹ _ ([]ᵀ-⁺-∘-filler _ γ δ j i))
      (λ where
        j (i = i0) → Bᴹ [ (γ ∘ δ) ⁺ ]ᵀᴹ
        j (i = i1) → []ᵀ-∘ᴹ Bᴹ (γ ⁺) (δ ⁺) j)
      (inS (Bᴹ [ ⁺-∘ γ δ i ]ᵀᴹ))
      j

  []ᵀ-⁺-idᴹ-filler :
    (Bᴹ : Tyᴹ (Γ ▹ A) B) →
    (j i : I) → Tyᴹ (Γ ▹ []ᵀ-id A i) ([]ᵀ-⁺-id-filler B j i)
  []ᵀ-⁺-idᴹ-filler Bᴹ j i =
    fill (λ j → Tyᴹ _ ([]ᵀ-⁺-id-filler _ j i))
      (λ where
        j (i = i0) → Bᴹ [ id ⁺ ]ᵀᴹ
        j (i = i1) → []ᵀ-idᴹ Bᴹ j)
      (inS (Bᴹ [ ⁺-id i ]ᵀᴹ))
      j

  []ᵀ-p-⁺ᴹ-filler :
    (Bᴹ : Tyᴹ Γ B) (γ : Sub Δ Γ) →
    (j i : I) → Tyᴹ (Δ ▹ A [ γ ]ᵀ) ([]ᵀ-p-⁺-filler B γ j i)
  []ᵀ-p-⁺ᴹ-filler Bᴹ γ j i =
    fill (λ j → Tyᴹ _ ([]ᵀ-p-⁺-filler _ γ j i))
      (λ where
        j (i = i0) → []ᵀ-∘ᴹ Bᴹ p (γ ⁺) j
        j (i = i1) → []ᵀ-∘ᴹ Bᴹ γ p j)
      (inS (Bᴹ [ p-⁺ γ i ]ᵀᴹ))
      j

  []ᵀ-p-⟨⟩ᴹ-filler :
    (Bᴹ : Tyᴹ Γ B) (a : Tm Γ A) (j i : I) → Tyᴹ Γ ([]ᵀ-p-⟨⟩-filler B a j i)
  []ᵀ-p-⟨⟩ᴹ-filler Bᴹ a j i =
    fill (λ j → Tyᴹ _ ([]ᵀ-p-⟨⟩-filler _ a j i))
      (λ where
        j (i = i0) → []ᵀ-∘ᴹ Bᴹ p ⟨ a ⟩ j
        j (i = i1) → []ᵀ-idᴹ Bᴹ j)
      (inS (Bᴹ [ p-⟨⟩ a i ]ᵀᴹ))
      j

module Elim (M : DModel) where
  open DModel M

  ⟦_⟧ : (A : Ty Γ) → Tyᴹ Γ A
  ⟦ isGroupoidTy Γ A₀ A₁ P₀ P₁ S₀ S₁ i j k ⟧ =
    isGroupoid→CubeP (λ i j k → Tyᴹ Γ (isGroupoidTy Γ A₀ A₁ P₀ P₁ S₀ S₁ i j k))
      (λ j k → ⟦ S₀ j k ⟧)
      (λ j k → ⟦ S₁ j k ⟧)
      (λ i k → ⟦ P₀ k ⟧)
      (λ i k → ⟦ P₁ k ⟧)
      (λ i j → ⟦ A₀ ⟧)
      (λ i j → ⟦ A₁ ⟧)
      (isSet→isGroupoid (isSetTyᴹ Γ A₁))
      i j k
  ⟦ A [ γ ]ᵀ ⟧ = ⟦ A ⟧ [ γ ]ᵀᴹ

  ⟦ []ᵀ-∘ A γ δ i ⟧ = []ᵀ-∘ᴹ ⟦ A ⟧ γ δ i
  ⟦ []ᵀ-id A i ⟧ = []ᵀ-idᴹ ⟦ A ⟧ i

  ⟦ []ᵀ-⁺-∘ B γ δ i ⟧ = []ᵀ-⁺-∘ᴹ-filler ⟦ B ⟧ γ δ i1 i
  ⟦ []ᵀ-⁺-∘-filler B γ δ j i ⟧ = []ᵀ-⁺-∘ᴹ-filler ⟦ B ⟧ γ δ j i

  ⟦ []ᵀ-⁺-id B i ⟧ = []ᵀ-⁺-idᴹ-filler ⟦ B ⟧ i1 i
  ⟦ []ᵀ-⁺-id-filler B j i ⟧ = []ᵀ-⁺-idᴹ-filler ⟦ B ⟧ j i

  ⟦ []ᵀ-p-⁺ B γ i ⟧ = []ᵀ-p-⁺ᴹ-filler ⟦ B ⟧ γ i1 i
  ⟦ []ᵀ-p-⁺-filler B γ j i ⟧ = []ᵀ-p-⁺ᴹ-filler ⟦ B ⟧ γ j i

  ⟦ []ᵀ-p-⟨⟩ B a i ⟧ = []ᵀ-p-⟨⟩ᴹ-filler ⟦ B ⟧ a i1 i
  ⟦ []ᵀ-p-⟨⟩-filler B a j i ⟧ = []ᵀ-p-⟨⟩ᴹ-filler ⟦ B ⟧ a j i

  ⟦ U ⟧ = Uᴹ
  ⟦ U-[] γ i ⟧ = U-[]ᴹ γ i

  ⟦ U-[]-∘ γ δ i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (U-[]-∘ γ δ i j))
      ([]ᵀ-∘ᴹ Uᴹ γ δ)
      refl
      (U-[]ᴹ (γ ∘ δ))
      (compPathP' {B = Tyᴹ _} (λ i → U-[]ᴹ γ i [ δ ]ᵀᴹ) (U-[]ᴹ δ))
      i j
  ⟦ U-[]-id i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (U-[]-id i j))
      ([]ᵀ-idᴹ Uᴹ)
      refl
      (U-[]ᴹ id)
      refl
      i j

  ⟦ El  ⟧ = Elᴹ Â
  ⟦ El-[] Â γ i ⟧ = El-[]ᴹ Â γ i
  ⟦ El-[]-∘ Â γ δ i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (El-[]-∘ Â γ δ i j))
      ([]ᵀ-∘ᴹ (Elᴹ Â) γ δ)
      (λ i → Elᴹ ([]ᵘ-∘ Â γ δ i))
      (El-[]ᴹ Â (γ ∘ δ))
      (compPathP' {B = Tyᴹ _}
        (λ i → El-[]ᴹ Â γ i [ δ ]ᵀᴹ)
        (El-[]ᴹ (Â [ γ ]ᵘ) δ))
      i j
  ⟦ El-[]-id  i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (El-[]-id  i j))
      ([]ᵀ-idᴹ (Elᴹ Â))
      (λ i → Elᴹ ([]ᵘ-id  i))
      (El-[]ᴹ Â id)
      refl
      i j

  ⟦ Π A B ⟧ = Πᴹ ⟦ A ⟧ ⟦ B ⟧
  ⟦ Π-[] A B γ i ⟧ = Π-[]ᴹ ⟦ A ⟧ ⟦ B ⟧ γ i

  ⟦ Π-[]-∘ A B γ δ i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (Π-[]-∘ A B γ δ i j))
      ([]ᵀ-∘ᴹ (Πᴹ ⟦ A ⟧ ⟦ B ⟧) γ δ)
      (λ i → Πᴹ ([]ᵀ-∘ᴹ ⟦ A ⟧ γ δ i) ([]ᵀ-⁺-∘ᴹ-filler ⟦ B ⟧ γ δ i1 i))
      (Π-[]ᴹ ⟦ A ⟧ ⟦ B ⟧ (γ ∘ δ))
      (compPathP' {B = Tyᴹ _}
        (λ i → Π-[]ᴹ ⟦ A ⟧ ⟦ B ⟧ γ i [ δ ]ᵀᴹ)
        (Π-[]ᴹ (⟦ A ⟧ [ γ ]ᵀᴹ) (⟦ B ⟧ [ γ ⁺ ]ᵀᴹ) δ))
      i j
  ⟦ Π-[]-id A B i j ⟧ =
    isSet→SquareP (λ i j → isSetTyᴹ _ (Π-[]-id A B i j))
      ([]ᵀ-idᴹ (Πᴹ ⟦ A ⟧ ⟦ B ⟧))
      (λ i → Πᴹ ([]ᵀ-idᴹ ⟦ A ⟧ i) ([]ᵀ-⁺-idᴹ-filler ⟦ B ⟧ i1 i))
      (Π-[]ᴹ ⟦ A ⟧ ⟦ B ⟧ id)
      refl
      i j