Skip to content

Instantly share code, notes, and snippets.

@11Kilobytes

11Kilobytes/Dependent_PHOAS.agda

Forked from GallagherCommaJack/Dependent_PHOAS.agda
Created January 20, 2016 19:52
Show Gist options
  • Save 11Kilobytes/decc1319e452da61f608 to your computer and use it in GitHub Desktop.
Save 11Kilobytes/decc1319e452da61f608 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment