相关疑难解决方法(0)

我可以定义以下归纳类型：

Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.

但随后该命令Check (c1 (T nat))失败并显示以下消息：该术语T nat具有类型，Type@{max(Set, Top.3+1)}而预期具有类型Type@{Top.3}（宇宙不一致）。

我怎样才能调整上面的归纳定义，以便c1 (T nat)不会导致宇宙不一致，并且不设置宇宙多态性？

以下工作，但我更喜欢不添加平等的解决方案：

Inductive T (A : Type) : Type :=
| c1 : A -> T A
| c2' : A = unit -> T A.

Definition c2 : T unit := c2' unit eq_refl.

Check (c1 (T …