coq - 宇宙不一致(因为严格的正性限制？)

Question

我有以下代码片段。

Set Implicit Arguments.

Inductive Simple (A: Type) := simple : Simple A.
Inductive Wrap (A: Type) :=
| wrap : A -> Wrap A
| funWrap : forall X, Simple X -> (X -> Wrap A) -> Wrap A.

Definition anotherWrap A : Wrap A :=
  funWrap (simple A) (fun x => wrap x).

Fail Definition specialWrap1 A : Wrap (Wrap A) :=
  funWrap (simple (Wrap A)) (fun x => wrap x).

Fail Definition specialWrap A : Wrap A :=
  funWrap (simple (Wrap A)) (fun x => x).

我的第一个想法是 funWrap 中的 X 不能用 Wrap A 实例化，因为归纳类型有严格的正性限制。是这种情况还是存在不一致的其他原因(可能是定义函数 specialWrap 的不同方法)？

编辑:第二个定义的解释在所选答案的评论中给出。

Answer 1

我认为您第一个定义的问题在于缺乏全域多态性。如果启用 Set Universe Polymorphism。 它将通过。

这是因为常规归纳定义是“宇宙单态的”，因此在这种情况下，由于共享宇宙级别，您会遇到宇宙问题。