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

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

open import TT.Set.Syntax X Y

private variable
  Γ Δ Θ : Con
  γ δ : Sub Δ Γ
  A B : Ty Γ
  a b : Tm Γ A
  Â : Tm Γ U
  f : Tm Γ (Π A B)

record DModel : Type₁ where
  no-eta-equality

  infixl  _∘ᴹ_ _[_]ᵀᴹ _[_]ᵗᴹ
  infixl  _▹ᴹ_
  infixl  _⁺ᴹ
  field
    Conᴹ : Con → Type
    Subᴹ : Conᴹ Δ → Conᴹ Γ → Sub Δ Γ → Type
    isPropSubᴹ :
      (Δᴹ : Conᴹ Δ) (Γᴹ : Conᴹ Γ) (γ : Sub Δ Γ) → isProp (Subᴹ Δᴹ Γᴹ γ)

    _∘ᴹ_ :
      {Δᴹ : Conᴹ Δ} {Γᴹ : Conᴹ Γ} {Θᴹ : Conᴹ Θ} →
      Subᴹ Δᴹ Γᴹ γ → Subᴹ Θᴹ Δᴹ δ → Subᴹ Θᴹ Γᴹ (γ ∘ δ)
    idᴹ : {Γᴹ : Conᴹ Γ} → Subᴹ Γᴹ Γᴹ id

    Tyᴹ : Conᴹ Γ → Ty Γ → Type
    isPropTyᴹ : (Γᴹ : Conᴹ Γ) (A : Ty Γ) → isProp (Tyᴹ Γᴹ A)
    _[_]ᵀᴹ :
      {Γᴹ : Conᴹ Γ} {Δᴹ : Conᴹ Δ} → Tyᴹ Γᴹ A → Subᴹ Δᴹ Γᴹ γ → Tyᴹ Δᴹ (A [ γ ]ᵀ)

    Tmᴹ : (Γᴹ : Conᴹ Γ) → Tyᴹ Γᴹ A → Tm Γ A → Type
    isPropTmᴹ :
      (Γᴹ : Conᴹ Γ) (Aᴹ : Tyᴹ Γᴹ A) (a : Tm Γ A) → isProp (Tmᴹ Γᴹ Aᴹ a)
    _[_]ᵗᴹ :
      {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} {Δᴹ : Conᴹ Δ} →
      Tmᴹ Γᴹ Aᴹ a → (γᴹ : Subᴹ Δᴹ Γᴹ γ) → Tmᴹ Δᴹ (Aᴹ [ γᴹ ]ᵀᴹ) (a [ γ ]ᵗ)

    ◇ᴹ : Conᴹ ◇
    εᴹ : {Γᴹ : Conᴹ Γ} → Subᴹ Γᴹ ◇ᴹ ε

    _▹ᴹ_ : (Γᴹ : Conᴹ Γ) → Tyᴹ Γᴹ A → Conᴹ (Γ ▹ A)
    pᴹ : {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} → Subᴹ (Γᴹ ▹ᴹ Aᴹ) Γᴹ p
    qᴹ : {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} → Tmᴹ (Γᴹ ▹ᴹ Aᴹ) (Aᴹ [ pᴹ ]ᵀᴹ) q

    _⁺ᴹ :
      {Δᴹ : Conᴹ Δ} {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} →
      (γᴹ : Subᴹ Δᴹ Γᴹ γ) → Subᴹ (Δᴹ ▹ᴹ Aᴹ [ γᴹ ]ᵀᴹ) (Γᴹ ▹ᴹ Aᴹ) (γ ⁺)
    ⟨_⟩ᴹ :
      {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} →
      (aᴹ : Tmᴹ Γᴹ Aᴹ a) → Subᴹ Γᴹ (Γᴹ ▹ᴹ Aᴹ) ⟨ a ⟩

    Uᴹ : {Γᴹ : Conᴹ Γ} → Tyᴹ Γᴹ U
    Elᴹ : {Γᴹ : Conᴹ Γ} → Tmᴹ Γᴹ Uᴹ Â → Tyᴹ Γᴹ (El Â)

    Πᴹ : {Γᴹ : Conᴹ Γ} (Aᴹ : Tyᴹ Γᴹ A) → Tyᴹ (Γᴹ ▹ᴹ Aᴹ) B → Tyᴹ Γᴹ (Π A B)
    appᴹ :
      {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} {Bᴹ : Tyᴹ (Γᴹ ▹ᴹ Aᴹ) B} →
      Tmᴹ Γᴹ (Πᴹ Aᴹ Bᴹ) f → Tmᴹ (Γᴹ ▹ᴹ Aᴹ) Bᴹ (app f)
    lamᴹ :
      {Γᴹ : Conᴹ Γ} {Aᴹ : Tyᴹ Γᴹ A} {Bᴹ : Tyᴹ (Γᴹ ▹ᴹ Aᴹ) B} →
      Tmᴹ (Γᴹ ▹ᴹ Aᴹ) Bᴹ b → Tmᴹ Γᴹ (Πᴹ Aᴹ Bᴹ) (lam b)

    in-Xᴹ : (x : X .fst) → Tmᴹ ◇ᴹ Uᴹ (in-X x)
    in-Yᴹ : {x : X .fst} (y : Y x .fst) → Tmᴹ ◇ᴹ (Elᴹ (in-Xᴹ x)) (in-Y y)

  []ᵀ-∘ᴹ :
    {Γᴹ : Conᴹ Γ} {Δᴹ : Conᴹ Δ} {Θᴹ : Conᴹ Θ}
    (Aᴹ : Tyᴹ Γᴹ A) (γᴹ : Subᴹ Δᴹ Γᴹ γ) (δᴹ : Subᴹ Θᴹ Δᴹ δ) →
    PathP (λ i → Tyᴹ Θᴹ ([]ᵀ-∘ A γ δ i))
      (Aᴹ [ γᴹ ∘ᴹ δᴹ ]ᵀᴹ)
      (Aᴹ [ γᴹ ]ᵀᴹ [ δᴹ ]ᵀᴹ)
  []ᵀ-∘ᴹ Aᴹ γᴹ δᴹ = isProp→PathP (λ i → isPropTyᴹ _ _) _ _

  []ᵀ-idᴹ :
    {Γᴹ : Conᴹ Γ} (Aᴹ : Tyᴹ Γᴹ A) →
    PathP (λ i → Tyᴹ Γᴹ ([]ᵀ-id A i)) (Aᴹ [ idᴹ ]ᵀᴹ) Aᴹ
  []ᵀ-idᴹ Aᴹ = isProp→PathP (λ i → isPropTyᴹ _ _) _ _

  U-[]ᴹ :
    {Δᴹ : Conᴹ Δ} {Γᴹ : Conᴹ Γ} (γᴹ : Subᴹ Δᴹ Γᴹ γ) →
    PathP (λ i → Tyᴹ Δᴹ (U-[] γ i)) (Uᴹ [ γᴹ ]ᵀᴹ) Uᴹ
  U-[]ᴹ γᴹ = isProp→PathP (λ i → isPropTyᴹ _ _) _ _

  infixl  _[_]ᵘᴹ
  _[_]ᵘᴹ :
    {Γᴹ : Conᴹ Γ} {Δᴹ : Conᴹ Δ} →
    Tmᴹ Γᴹ Uᴹ Â → Subᴹ Δᴹ Γᴹ γ → Tmᴹ Δᴹ Uᴹ (Â [ γ ]ᵘ)
  _[_]ᵘᴹ {Â} {γ} Âᴹ γᴹ =
    transport (λ i → Tmᴹ _ (U-[]ᴹ γᴹ i) ([]ᵘ-filler  γ i)) (Âᴹ [ γᴹ ]ᵗᴹ)

  El-[]ᴹ :
    {Γᴹ : Conᴹ Γ} {Δᴹ : Conᴹ Δ} (Âᴹ : Tmᴹ Γᴹ Uᴹ Â) (γᴹ : Subᴹ Δᴹ Γᴹ γ) →
    PathP (λ i → Tyᴹ Δᴹ (El-[] Â γ i)) (Elᴹ Âᴹ [ γᴹ ]ᵀᴹ) (Elᴹ (Âᴹ [ γᴹ ]ᵘᴹ))
  El-[]ᴹ Âᴹ γᴹ = isProp→PathP (λ i → isPropTyᴹ _ _) _ _

  Π-[]ᴹ :
    {Γᴹ : Conᴹ Γ} {Δᴹ : Conᴹ Δ}
    (Aᴹ : Tyᴹ Γᴹ A) (Bᴹ : Tyᴹ (Γᴹ ▹ᴹ Aᴹ) B) (γᴹ : Subᴹ Δᴹ Γᴹ γ) →
    PathP (λ i → Tyᴹ Δᴹ (Π-[] A B γ i))
      (Πᴹ Aᴹ Bᴹ [ γᴹ ]ᵀᴹ)
      (Πᴹ (Aᴹ [ γᴹ ]ᵀᴹ) (Bᴹ [ γᴹ ⁺ᴹ ]ᵀᴹ))
  Π-[]ᴹ Aᴹ Bᴹ γᴹ = isProp→PathP (λ i → isPropTyᴹ _ _) _ _

module Elim (M : DModel) where
  open DModel M

  ⟦_⟧ₛ : (s : Sort) → EL s → Type
  ⟦_⟧ : {s : Sort} (x : EL s) → ⟦ s ⟧ₛ x

  ⟦ con ⟧ₛ Γ = Conᴹ Γ
  ⟦ sub Δ Γ ⟧ₛ γ = Subᴹ ⟦ Δ ⟧ ⟦ Γ ⟧ γ
  ⟦ ty Γ ⟧ₛ A = Tyᴹ ⟦ Γ ⟧ A
  ⟦ tm Γ A ⟧ₛ a = Tmᴹ ⟦ Γ ⟧ ⟦ A ⟧ a

  ⟦ isSetSub Δ Γ γ₀ γ₁ P₀ P₁ i j ⟧ =
    isProp→SquareP
      (λ i j → isPropSubᴹ ⟦ Δ ⟧ ⟦ Γ ⟧ (isSetSub Δ Γ γ₀ γ₁ P₀ P₁ i j))
      (λ i → ⟦ γ₀ ⟧)
      (λ i → ⟦ γ₁ ⟧)
      (λ j → ⟦ P₀ j ⟧)
      (λ j → ⟦ P₁ j ⟧)
      i j
  ⟦ γ ∘ δ ⟧ = ⟦ γ ⟧ ∘ᴹ ⟦ δ ⟧
  ⟦ assoc γ δ θ i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (assoc γ δ θ i))
      (⟦ γ ⟧ ∘ᴹ (⟦ δ ⟧ ∘ᴹ ⟦ θ ⟧))
      ((⟦ γ ⟧ ∘ᴹ ⟦ δ ⟧) ∘ᴹ ⟦ θ ⟧)
      i

  ⟦ id ⟧ = idᴹ
  ⟦ idr γ i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (idr γ i)) (⟦ γ ⟧ ∘ᴹ idᴹ) ⟦ γ ⟧ i
  ⟦ idl γ i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (idl γ i)) (idᴹ ∘ᴹ ⟦ γ ⟧) ⟦ γ ⟧ i

  ⟦ isSetTy Γ A₀ A₁ P₀ P₁ i j ⟧ =
    isProp→SquareP
      (λ i j → isPropTyᴹ ⟦ Γ ⟧ (isSetTy Γ A₀ A₁ P₀ P₁ i j))
      (λ i → ⟦ A₀ ⟧)
      (λ i → ⟦ A₁ ⟧)
      (λ j → ⟦ P₀ j ⟧)
      (λ j → ⟦ P₁ j ⟧)
      i j
  ⟦ A [ γ ]ᵀ ⟧ = ⟦ A ⟧ [ ⟦ γ ⟧ ]ᵀᴹ
  ⟦ []ᵀ-∘ A γ δ i ⟧ = []ᵀ-∘ᴹ ⟦ A ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i
  ⟦ []ᵀ-id A i ⟧ = []ᵀ-idᴹ ⟦ A ⟧ i

  ⟦ isSetTm Γ A a₀ a₁ P₀ P₁ i j ⟧ =
    isProp→SquareP
      (λ i j → isPropTmᴹ ⟦ Γ ⟧ ⟦ A ⟧ (isSetTm Γ A a₀ a₁ P₀ P₁ i j))
      (λ i → ⟦ a₀ ⟧)
      (λ i → ⟦ a₁ ⟧)
      (λ j → ⟦ P₀ j ⟧)
      (λ j → ⟦ P₁ j ⟧)
      i j
  ⟦ a [ γ ]ᵗ ⟧ = ⟦ a ⟧ [ ⟦ γ ⟧ ]ᵗᴹ

  ⟦ []ᵗ-∘ {A} a γ δ i ⟧ =
    isProp→PathP
      (λ i → isPropTmᴹ _ ([]ᵀ-∘ᴹ ⟦ A ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i) ([]ᵗ-∘ a γ δ i))
      (⟦ a ⟧ [ ⟦ γ ⟧ ∘ᴹ ⟦ δ ⟧ ]ᵗᴹ)
      (⟦ a ⟧ [ ⟦ γ ⟧ ]ᵗᴹ [ ⟦ δ ⟧ ]ᵗᴹ)
      i
  ⟦ []ᵗ-id {A} a i ⟧ =
    isProp→PathP (λ i → isPropTmᴹ _ ([]ᵀ-idᴹ ⟦ A ⟧ i) ([]ᵗ-id a i))
      (⟦ a ⟧ [ idᴹ ]ᵗᴹ)
      ⟦ a ⟧
      i

  ⟦ ◇ ⟧ = ◇ᴹ
  ⟦ ε ⟧ = εᴹ
  ⟦ ε-∘ γ i ⟧ = isProp→PathP (λ i → isPropSubᴹ _ _ (ε-∘ γ i)) (εᴹ ∘ᴹ ⟦ γ ⟧) εᴹ i
  ⟦ ◇-η i ⟧ = isProp→PathP (λ i → isPropSubᴹ _ _ (◇-η i)) idᴹ εᴹ i

  ⟦ Γ ▹ A ⟧ = ⟦ Γ ⟧ ▹ᴹ ⟦ A ⟧
  ⟦ p ⟧ = pᴹ
  ⟦ q ⟧ = qᴹ
  ⟦ γ ⁺ ⟧ = ⟦ γ ⟧ ⁺ᴹ
  ⟦ ⟨ a ⟩ ⟧ = ⟨ ⟦ a ⟧ ⟩ᴹ

  ⟦ ⟨⟩-∘ a γ i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (⟨⟩-∘ a γ i))
      (⟨ ⟦ a ⟧ ⟩ᴹ ∘ᴹ ⟦ γ ⟧)
      (⟦ γ ⟧ ⁺ᴹ ∘ᴹ ⟨ ⟦ a ⟧ [ ⟦ γ ⟧ ]ᵗᴹ ⟩ᴹ)
      i
  ⟦ ▹-η i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (▹-η i)) idᴹ (pᴹ ⁺ᴹ ∘ᴹ ⟨ qᴹ ⟩ᴹ) i

  ⟦ ⁺-∘ {A} γ δ i ⟧ =
    isProp→PathP
      (λ i → isPropSubᴹ (_ ▹ᴹ []ᵀ-∘ᴹ ⟦ A ⟧ ⟦ γ ⟧ ⟦ δ ⟧ i) _ (⁺-∘ γ δ i))
      ((⟦ γ ⟧ ∘ᴹ ⟦ δ ⟧) ⁺ᴹ)
      (⟦ γ ⟧ ⁺ᴹ ∘ᴹ ⟦ δ ⟧ ⁺ᴹ)
      i
  ⟦ ⁺-id {A} i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ (_ ▹ᴹ []ᵀ-idᴹ ⟦ A ⟧ i) _ (⁺-id i))
      (idᴹ ⁺ᴹ)
      idᴹ
      i

  ⟦ p-⁺ γ i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ (_ ▹ᴹ _) _ (p-⁺ γ i))
      (pᴹ ∘ᴹ ⟦ γ ⟧ ⁺ᴹ)
      (⟦ γ ⟧ ∘ᴹ pᴹ)
      i
  ⟦ []ᵀ-p-⁺ B γ i ⟧ =
    isProp→PathP (λ i → isPropTyᴹ (_ ▹ᴹ _) ([]ᵀ-p-⁺ B γ i))
      (⟦ B ⟧ [ pᴹ ]ᵀᴹ [ ⟦ γ ⟧ ⁺ᴹ ]ᵀᴹ)
      (⟦ B ⟧ [ ⟦ γ ⟧ ]ᵀᴹ [ pᴹ ]ᵀᴹ)
      i
  ⟦ q-⁺ {A} γ i ⟧ =
    isProp→PathP
      (λ i →
        isPropTmᴹ _
          (isProp→PathP (λ i → isPropTyᴹ (_ ▹ᴹ _) ([]ᵀ-p-⁺ A γ i))
            (⟦ A ⟧ [ pᴹ ]ᵀᴹ [ ⟦ γ ⟧ ⁺ᴹ ]ᵀᴹ)
            (⟦ A ⟧ [ ⟦ γ ⟧ ]ᵀᴹ [ pᴹ ]ᵀᴹ)
            i)
          (q-⁺ γ i))
      (qᴹ [ ⟦ γ ⟧ ⁺ᴹ ]ᵗᴹ)
      qᴹ
      i

  ⟦ p-⟨⟩ a i ⟧ =
    isProp→PathP (λ i → isPropSubᴹ _ _ (p-⟨⟩ a i)) (pᴹ ∘ᴹ ⟨ ⟦ a ⟧ ⟩ᴹ) idᴹ i
  ⟦ []ᵀ-p-⟨⟩ B a i ⟧ =
    isProp→PathP (λ i → isPropTyᴹ _ ([]ᵀ-p-⟨⟩ B a i))
      (⟦ B ⟧ [ pᴹ ]ᵀᴹ [ ⟨ ⟦ a ⟧ ⟩ᴹ ]ᵀᴹ)
      ⟦ B ⟧
      i
  ⟦ q-⟨⟩ {A} a i ⟧ =
    isProp→PathP
      (λ i →
        isPropTmᴹ _
          (isProp→PathP (λ i → isPropTyᴹ _ ([]ᵀ-p-⟨⟩ A a i))
            (⟦ A ⟧ [ pᴹ ]ᵀᴹ [ ⟨ ⟦ a ⟧ ⟩ᴹ ]ᵀᴹ)
            ⟦ A ⟧
            i)
          (q-⟨⟩ a i))
      (qᴹ [ ⟨ ⟦ a ⟧ ⟩ᴹ ]ᵗᴹ)
      ⟦ a ⟧
      i

  ⟦ U ⟧ = Uᴹ
  ⟦ U-[] γ i ⟧ = U-[]ᴹ ⟦ γ ⟧ i
  ⟦ Â [ γ ]ᵘ ⟧ = ⟦ Â ⟧ [ ⟦ γ ⟧ ]ᵘᴹ
  ⟦ []ᵘ-filler  γ i ⟧ =
    isProp→PathP (λ i → isPropTmᴹ _ (U-[]ᴹ ⟦ γ ⟧ i) ([]ᵘ-filler  γ i))
      (⟦Â⟧ [ ⟦ γ ⟧ ]ᵗᴹ)
      (⟦Â⟧ [ ⟦ γ ⟧ ]ᵘᴹ)
      i
    where
    ⟦Â⟧ : Tmᴹ _ Uᴹ Â
    ⟦Â⟧ = ⟦ Â ⟧

  ⟦ El  ⟧ = Elᴹ ⟦  ⟧
  ⟦ El-[] Â γ i ⟧ = El-[]ᴹ ⟦ Â ⟧ ⟦ γ ⟧ i

  ⟦ Π A B ⟧ = Πᴹ ⟦ A ⟧ ⟦ B ⟧
  ⟦ Π-[] A B γ i ⟧ = Π-[]ᴹ ⟦ A ⟧ ⟦ B ⟧ ⟦ γ ⟧ i
  ⟦ app f ⟧ = appᴹ ⟦ f ⟧
  ⟦ lam b ⟧ = lamᴹ ⟦ b ⟧
  ⟦ lam-[] b γ i ⟧ =
    isProp→PathP (λ i → isPropTmᴹ _ (Π-[]ᴹ _ _ _ i) (lam-[] b γ i))
      (lamᴹ ⟦ b ⟧ [ ⟦ γ ⟧ ]ᵗᴹ)
      (lamᴹ (⟦b⟧ [ ⟦ γ ⟧ ⁺ᴹ ]ᵗᴹ))
      i
    where
    ⟦b⟧ : Tmᴹ (_ ▹ᴹ _) _ b
    ⟦b⟧ = ⟦ b ⟧
  ⟦ Π-β b i ⟧ =
    isProp→PathP (λ i → isPropTmᴹ _ _ (Π-β b i)) (appᴹ (lamᴹ ⟦ b ⟧)) ⟦ b ⟧ i
  ⟦ Π-η f i ⟧ =
    isProp→PathP (λ i → isPropTmᴹ _ _ (Π-η f i)) ⟦ f ⟧ (lamᴹ (appᴹ ⟦ f ⟧)) i

  ⟦ in-X x ⟧ = in-Xᴹ x
  ⟦ in-Y y ⟧ = in-Yᴹ y