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

module TT.Wild.Syntax (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

data Sort : Type
data EL : Sort → Type

Con : Type
Sub : Con → Con → Type
Ty : Con → Type
Tm : (Γ : Con) → Ty Γ → Type

data Sort where
  con : Sort
  sub : Con → Con → Sort
  ty : Con → Sort
  tm : (Γ : Con) → Ty Γ → Sort

Con = EL con
Sub Δ Γ = EL (sub Δ Γ)
Ty Γ = EL (ty Γ)
Tm Γ A = EL (tm Γ A)

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

infixl  _∘_ _[_]ᵀ _[_]ᵗ
infixl  _▹_
infixl  _⁺
infixl  _[_]ᵘ
data EL where
  _∘_ : Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
  assoc : (γ : Sub Δ Γ) (δ : Sub Θ Δ) (θ : Sub Ξ Θ) → γ ∘ (δ ∘ θ) ≡ (γ ∘ δ) ∘ θ

  id : Sub Γ Γ
  idr : (γ : Sub Δ Γ) → γ ∘ id ≡ γ
  idl : (γ : Sub Δ Γ) → id ∘ γ ≡ γ

  _[_]ᵀ : Ty Γ → Sub Δ Γ → Ty Δ
  []ᵀ-∘ :
    (A : Ty Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → A [ γ ∘ δ ]ᵀ ≡ A [ γ ]ᵀ [ δ ]ᵀ
  []ᵀ-id : (A : Ty Γ) → A [ id ]ᵀ ≡ A

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

  ◇ : Con
  ε : Sub Γ ◇
  ε-∘ : (γ : Sub Δ Γ) → ε ∘ γ ≡ ε
  ◇-η : id ≡ ε

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

  _⁺ : (γ : Sub Δ Γ) → Sub (Δ ▹ A [ γ ]ᵀ) (Γ ▹ A)
  ⟨_⟩ : (a : Tm Γ A) → Sub Γ (Γ ▹ A)
  ⟨⟩-∘ : (a : Tm Γ A) (γ : Sub Δ Γ) → ⟨ a ⟩ ∘ γ ≡ γ ⁺ ∘ ⟨ a [ γ ]ᵗ ⟩
  ▹-η : id {Γ ▹ A} ≡ p ⁺ ∘ ⟨ q ⟩

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

  p-⁺ : (γ : Sub Δ Γ) → p {A = A} ∘ γ ⁺ ≡ γ ∘ p
  []ᵀ-p-⁺ :
    (B : Ty Γ) (γ : Sub Δ Γ) → B [ p {A = A} ]ᵀ [ γ ⁺ ]ᵀ ≡ B [ γ ]ᵀ [ p ]ᵀ
  q-⁺ :
    (γ : Sub Δ Γ) →
    PathP (λ i → Tm (Δ ▹ A [ γ ]ᵀ) ([]ᵀ-p-⁺ A γ i)) (q [ γ ⁺ ]ᵗ) q
  {-
  -- limitation of Cubical Agda, this doesn't pass positivity check:
  q-⁺ :
    (γ : Sub Δ Γ) →
    PathP
      (λ i →
        Tm (Δ ▹ A [ γ ]ᵀ)
          ((sym ([]ᵀ-∘ A p (γ ⁺)) ∙ cong (A [_]ᵀ) (p-⁺ γ) ∙ []ᵀ-∘ A γ p) i))
      (q [ γ ⁺ ]ᵗ)
      q
  -}

  p-⟨⟩ : (a : Tm Γ A) → p ∘ ⟨ a ⟩ ≡ id
  []ᵀ-p-⟨⟩ : (B : Ty Γ) (a : Tm Γ A) → B [ p ]ᵀ [ ⟨ a ⟩ ]ᵀ ≡ B
  q-⟨⟩ : (a : Tm Γ A) → PathP (λ i → Tm Γ ([]ᵀ-p-⟨⟩ A a i)) (q [ ⟨ a ⟩ ]ᵗ) a
  {-
  -- limitation of Cubical Agda, this doesn't pass positivity check:
  q-⟨⟩ :
    (a : Tm Γ A) →
    PathP
      (λ i →
        Tm Γ ((sym ([]ᵀ-∘ A p ⟨ a ⟩) ∙ cong (A [_]ᵀ) (p-⟨⟩ a) ∙ []ᵀ-id A) i))
      (q [ ⟨ a ⟩ ]ᵗ)
      a
  -}

  U : Ty Γ
  U-[] : (γ : Sub Δ Γ) → U [ γ ]ᵀ ≡ U

  _[_]ᵘ : Tm Γ U → Sub Δ Γ → Tm Δ U
  []ᵘ-filler :
    (Â : Tm Γ U) (γ : Sub Δ Γ) →
    PathP (λ i → Tm Δ (U-[] γ i)) (Â [ γ ]ᵗ) (Â [ γ ]ᵘ)

  El : Tm Γ U → Ty Γ
  El-[] : ( : Tm Γ U) (γ : Sub Δ Γ) → El  [ γ ]ᵀ ≡ El ( [ γ ]ᵘ)
  {-
  -- limitation of Cubical Agda, this doesn't pass positivity check:
  El-[] :
    (Â : Tm Γ U) (γ : Sub Δ Γ) →
    El  [ γ ]ᵀ ≡ El (transport (λ i → Tm Δ (U-[] γ i)) ( [ γ ]ᵗ))
  -}

  Π : (A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
  Π-[] :
    (A : Ty Γ) (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) →
    Π A B [ γ ]ᵀ ≡ Π (A [ γ ]ᵀ) (B [ γ ⁺ ]ᵀ)

  app : Tm Γ (Π A B) → Tm (Γ ▹ A) B
  lam : Tm (Γ ▹ A) B → Tm Γ (Π A B)
  lam-[] :
    (b : Tm (Γ ▹ A) B) (γ : Sub Δ Γ) →
    PathP (λ i → Tm Δ (Π-[] A B γ i)) (lam b [ γ ]ᵗ) (lam (b [ γ ⁺ ]ᵗ))

  Π-β : (b : Tm (Γ ▹ A) B) → app (lam b) ≡ b
  Π-η : (f : Tm Γ (Π A B)) → f ≡ lam (app f)

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