A dependently-typed lambda calculus based on MLTT and inspired by Agda.
Currently, it features dependent product types, non-cumulative universes, built-in naturals, and intensional equality, along with their corresponding elimination rules (pattern matching) and primitive recursion, and generalized inductive datatypes coming soon.
It also has indexed inductive datatypes with elimination based on simple unification à la Agda.
Eventually it would be nice to add some form of meta-variable solving to support implicit arguments.
Another possible extension could be multiple-argument recursion, either via straightforward sugaring or more involved termination checking.