Comments

• LambdaPi paper doesn't tell why values are divided into neutral terms and a lambda abstraction. Frank Pfenning's lecture notes give another explation. Values (neutral terms) (Value ~ ValueIntro) are introduced, or they meet with elimination forms (ValueElim) which are extracted from a hypothesis. https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch3-seqcalc.pdf
• In LambdaPi paper only \(Term\uparrow\) (inferred) are substituted. Therefore we have Scope TermInf. However binding forms close over \(Term\downarrow\), we wrap them in TermChkT, and use Bound.ScopeT to make all that look simple. Noteworthy is the fact, that TermChk is not a Monad, but TermChkT is a Bound.
• Language.PTS.Smart defines small DSL to write terms in Haskell (Haskell as a meta-language!). We rely on FunctionalDependencies to make combinators work for Term and Value. Similar idea is used in the lucid_ package.