TT.Groupoid.Syntax

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

module TT.Groupoid.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 9 _∘_ _[_]ᵀ _[_]ᵗ
infixl 2 _▹_
infixl 10 _⁺
infixl 9 _[_]ᵘ
data EL where
  isSetSub : (Δ Γ : Con) → isSet (Sub Δ Γ)
  _∘_ : Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
  assoc : (γ : Sub Δ Γ) (δ : Sub Θ Δ) (θ : Sub Ξ Θ) → γ ∘ (δ ∘ θ) ≡ (γ ∘ δ) ∘ θ

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

  isGroupoidTy : (Γ : Con) → isGroupoid (Ty Γ)
  _[_]ᵀ : Ty Γ → Sub Δ Γ → Ty Δ

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

  isSetTm : (Γ : Con) (A : Ty Γ) → isSet (Tm Γ 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)) ((γ ∘ δ) ⁺) (γ ⁺ ∘ δ ⁺)
  []ᵀ-⁺-∘ :
    (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    PathP (λ i → Ty (Θ ▹ []ᵀ-∘ A γ δ i))
      (B [ (γ ∘ δ) ⁺ ]ᵀ)
      (B [ γ ⁺ ]ᵀ [ δ ⁺ ]ᵀ)
  []ᵀ-⁺-∘-filler :
    (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    SquareP (λ j i → Ty (Θ ▹ []ᵀ-∘ A γ δ i))
      (λ j → B [ ⁺-∘ γ δ j ]ᵀ)
      ([]ᵀ-⁺-∘ B γ δ)
      refl
      ([]ᵀ-∘ B (γ ⁺) (δ ⁺))

  ⁺-id : PathP (λ i → Sub (Γ ▹ []ᵀ-id A i) (Γ ▹ A)) (id ⁺) id
  []ᵀ-⁺-id :
    (B : Ty (Γ ▹ A)) → PathP (λ i → Ty (Γ ▹ []ᵀ-id A i)) (B [ id ⁺ ]ᵀ) B
  []ᵀ-⁺-id-filler :
    (B : Ty (Γ ▹ A)) →
    SquareP (λ j i → Ty (Γ ▹ []ᵀ-id A i))
      (λ j → B [ ⁺-id j ]ᵀ)
      ([]ᵀ-⁺-id B)
      refl
      ([]ᵀ-id B)

  p-⁺ : (γ : Sub Δ Γ) → p {A = A} ∘ γ ⁺ ≡ γ ∘ p
  []ᵀ-p-⁺ :
    (B : Ty Γ) (γ : Sub Δ Γ) → B [ p {A = A} ]ᵀ [ γ ⁺ ]ᵀ ≡ B [ γ ]ᵀ [ p ]ᵀ
  []ᵀ-p-⁺-filler :
    (B : Ty Γ) (γ : Sub Δ Γ) →
    Square
      (cong (B [_]ᵀ) (p-⁺ {A = A} γ))
      ([]ᵀ-p-⁺ B γ)
      ([]ᵀ-∘ B p (γ ⁺))
      ([]ᵀ-∘ B γ p)
  q-⁺ :
    (γ : Sub Δ Γ) →
    PathP (λ i → Tm (Δ ▹ A [ γ ]ᵀ) ([]ᵀ-p-⁺ A γ i)) (q [ γ ⁺ ]ᵗ) q

  p-⟨⟩ : (a : Tm Γ A) → p ∘ ⟨ a ⟩ ≡ id
  []ᵀ-p-⟨⟩ : (B : Ty Γ) (a : Tm Γ A) → B [ p ]ᵀ [ ⟨ a ⟩ ]ᵀ ≡ B
  []ᵀ-p-⟨⟩-filler :
    (B : Ty Γ) (a : Tm Γ A) →
    Square (cong (B [_]ᵀ) (p-⟨⟩ a)) ([]ᵀ-p-⟨⟩ B a) ([]ᵀ-∘ B p ⟨ a ⟩) ([]ᵀ-id B)
  q-⟨⟩ : (a : Tm Γ A) → PathP (λ i → Tm Γ ([]ᵀ-p-⟨⟩ A a i)) (q [ ⟨ a ⟩ ]ᵗ) a

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

  U-[]-∘ :
    (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    Square ([]ᵀ-∘ U γ δ) refl (U-[] (γ ∘ δ)) (cong _[ δ ]ᵀ (U-[] γ) ∙ U-[] δ)
  U-[]-id : Square ([]ᵀ-id (U {Γ})) refl (U-[] id) refl

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

  []ᵘ-∘ :
    (Â : Tm Γ U) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → Â [ γ ∘ δ ]ᵘ ≡ Â [ γ ]ᵘ [ δ ]ᵘ
  []ᵘ-id : (Â : Tm Γ U) → Â [ id ]ᵘ ≡ Â

  El : Tm Γ U → Ty Γ
  El-[] : (Â : Tm Γ U) (γ : Sub Δ Γ) → El Â [ γ ]ᵀ ≡ El (Â [ γ ]ᵘ)

  El-[]-∘ :
    (Â : Tm Γ U) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    Square
      ([]ᵀ-∘ (El Â) γ δ)
      (cong El ([]ᵘ-∘ Â γ δ))
      (El-[] Â (γ ∘ δ))
      (cong _[ δ ]ᵀ (El-[] Â γ) ∙ El-[] (Â [ γ ]ᵘ) δ)
  El-[]-id :
    (Â : Tm Γ U) → Square ([]ᵀ-id (El Â)) (cong El ([]ᵘ-id Â)) (El-[] Â id) refl

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

  Π-[]-∘ :
    (A : Ty Γ) (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
    Square
      ([]ᵀ-∘ (Π A B) γ δ)
      (cong₂ Π ([]ᵀ-∘ A γ δ) ([]ᵀ-⁺-∘ B γ δ))
      (Π-[] A B (γ ∘ δ))
      (cong _[ δ ]ᵀ (Π-[] A B γ) ∙ Π-[] (A [ γ ]ᵀ) (B [ γ ⁺ ]ᵀ) δ)
  Π-[]-id :
    (A : Ty Γ) (B : Ty (Γ ▹ A)) →
    Square ([]ᵀ-id (Π A B)) (cong₂ Π ([]ᵀ-id A) ([]ᵀ-⁺-id B)) (Π-[] A B id) refl

  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))