我本着这篇文章的精神实现了依赖类型的 lambda 演算：http ://www.andres-loeh.de/LambdaPi/LambdaPi.pdf 演算，有效，我用它做了实验，并扩展了几件事：许多宇宙，硬编码归纳公理。但是，我想添加归纳类型来做更复杂的事情。
我正在考虑两种方法
这两种方式我都不喜欢。第一个太低级，需要大量的努力才能从高级语言转换为核心语言。第二种方式工作量很大，而且容易出错，因为复杂归纳类型的递归原理的生成有很多极端情况，即正/负出现。
如何做到这一点？这些类型如何在 Coq、Agda 和 Idris 等现有系统中实现？
Sorry, but I don't know about Idris.
For Agda, I recommend Ulf Norell Phd Thesis as a starting point, but the system evolved since.
Coq introduces a third bullet in your list: automatically generated predicates.
Each inductive type comes with 3 (1 in some special cases) induction schemes that are automatically defined for the user, and named your_type_rect, your_type_rec and your_type_ind (only the latter one in the special cases). These are actual terms of the languages, generated automatically for the user, and used by the induction tactic (I'm not 100% sure about that last one), and not axioms.
In fact you can shut down this automatic generation and write your induction schemes yourself.
Some documentation about induction can be found here. I advises that you ask your question on the Coq mailing-list, where devs might give you more insight about the internals of Coq.
Best, V.