Make contexts contain type-families to support higher-order arguments
Russoul opened this issue · 0 comments
Russoul commented
For example then we can type a dependent version of function elimination:
Γ (f : (x : A) → B) ⊦ C type
Γ ((x : A) ⊦ f : B) ⊦ F : C(x ↦ f)
Γ ⊦ f : (x : A) → B
----------------------------------
Γ ⊦ Π-elim f.C f(x).F f : C(f)