open import Paths
open import Logic::HLevels
open import Sets::Unit

open data Con : Type
| •
| infix ▷ (Γ : Con) (Ty Γ)

// The ↑ operator in the paper
def ext {Γ Δ : Con} (δ : Γ << Δ) (A : Ty Δ) : Γ ▷ Subst A δ << Δ ▷ A ⇒
  δ ∘ π₁ (id idp) ∷ transport (Tm _) SubAss (π₂ (id idp))

// Incomplete
open data Ty (Γ : Con) : Type
| U
| Π (A : Ty Γ) (B : Ty (Γ ▷ A))
| El (A : Tm Γ U)
| Subst {Δ : Con} (Ty Δ) (s : Γ << Δ)
| SubId {A : Ty Γ} : Subst A (id idp) = A
| SubAss {Δ Θ : Con} {A : Ty Θ} {θ : Γ << Δ} {δ : Δ << Θ}
    : Subst (Subst A δ) θ = Subst A (δ ∘ θ)
| SubU {Δ : Con} (δ : Γ << Δ) : Subst U δ = U
| SubEl {Δ : Con} {δ : Γ << Δ} {a : Tm Δ U}
    : Subst (El a) δ = El (transport (Tm _) (SubU δ) (sub a))
| SubΠ {Δ : Con} (σ : Γ << Δ) {A : Ty Δ} {B : Ty (Δ ▷ A)}
    : Subst (Π A B) σ = Π (Subst A σ) (Subst B (ext σ A))
| TyTrunc : isSet (Ty Γ)

// Tms
open data infix << (Γ : Con) (Δ : Con) : Type
   tighter = looser ▷
| Γ, • ⇒ ε
| _, Δ ▷ A ⇒ infixr ∷ (δ : Γ << Δ) (Tm Γ (Subst A δ)) tighter =
| infix ∘ {Θ : Con} (Θ << Δ) (Γ << Θ) tighter = ∷
| π₁ {A : Ty Δ} (Γ << Δ ▷ A)
| id (Γ = Δ)
| idl• {s : Γ << Δ} : id idp ∘ s = s
| idr• {s : Γ << Δ} : s ∘ id idp = s
| ass {Θ Ξ : Con} {ν : Γ << Ξ} {δ : Ξ << Θ} {σ : Θ << Δ}
    : (σ ∘ δ) ∘ ν = σ ∘ (δ ∘ ν)
| π₁β {δ : Γ << Δ} {A : Ty Δ} (t : Tm Γ (Subst A δ)) : π₁ (δ ∷ t) = δ
| Γ, Δ ▷ A ⇒ πη {δ : Γ << Δ ▷ A} : (π₁ δ ∷ π₂ δ) = δ
| Γ, Δ ▷ A ⇒ ∷∘ {Θ : Con} {σ : Θ << Δ} {δ : Γ << Θ} {t : Tm Θ (Subst A σ)}
    : (σ ∷ t) ∘ δ = (σ ∘ δ) ∷ transport (Tm _) SubAss (sub t)
| Γ, • ⇒ εη {δ : Γ << •} : δ = ε
| TmsTrunc : isSet (Γ << Δ)

// Incomplete
open data Tm (Γ : Con) (A : Ty Γ) : Type
| _, Π A B ⇒ λ (Tm (Γ ▷ A) B)
| Γ' ▷ A, B ⇒ app (Tm Γ' (Π A B))
| _, Subst A δ ⇒ sub (Tm _ A)
| _, Subst A (π₁ δ) ⇒ π₂ (Γ << _ ▷ A)
| _, Subst B δ ⇒ π₂β {Δ : Con} (t : Tm Γ A)
    : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
| _ ▷ _, A ⇒ Πβ (f : Tm Γ A) : app (λ f) = f
| _, Π _ _ ⇒ Πη (f : Tm Γ A) : λ (app f) = f
// Subλ is omitted for its overwhleming complexity
| TmTrunc : isSet (Tm Γ A)