Dependent_PHOAS.agda

data Ty : Set
data Tm : Ty → Set

postulate Var : Ty → Set

data Ty where
  pi sg : (A : Ty)(B : Var A → Ty) → Ty

data Subst {A} : (Var A → Ty) → Tm A → Ty → Set where
  -- need to fill this in
  -- should be fairly routine though

data Tm where
  ^_  : ∀{A} → Var A → Tm A
  lam : ∀{A B} → ((v : Var A) → Tm (B v)) → Tm (pi A B)
  deg : ∀{A B} → Tm (pi A B) → Tm A → Tm (sg A B)
  _#_[_] : ∀{A B} → Tm (pi A B) → ∀(a : Tm A){B'} → Subst B a B' → Tm B'
  pi1 : ∀{A B} → Tm (sg A B) → Tm A
  pi2_[_] : ∀{A B B'} (s : Tm (sg A B)) → Subst B (pi1 s) B' → Tm B'
  _,[_]_ : ∀{A B B'} → (a : Tm A) → Subst B a B' → Tm B' → Tm (sg A B)