I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
The calculus, works and I experimented with it and like it. However, I want to add inductive types to do more complex stuff. What are the options for doing this?
I am thinking about two ways of doing so
- Introduce Fin-N, Product and W-types and represent inductive types with them.
- Generate induction and recursion axioms.
What can you recommend? How inductive types are represented in systems like Coq, Idris and Agda? Which articles can you recommend me?