I am trying to find a minimal implementation of dependent type theory that supports
- Pi Types (obviously)
- Modules containing records
- Inductive data types
- Universe Hierarchy
- A notion of equality
- Termination checker
- Type Inference and Resolution
I am aware of implementations based on:
Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207.
But they do not support everything in the list above.
Something even smaller than mini-Agda would be helpful.