ユニバースの矛盾（厳密な正の制限のため？）

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）？

編集：2番目の定義の説明は、選択した回答のコメントに記載されています。

Answer 1

最初の定義での問題は、宇宙多形性の欠如であると私は思います。 Set Universe Polymorphism.を有効にすると、それは通過します。

これは、規則的帰納的定義が「宇宙単形」であるためです。この場合、共有宇宙レベルのために宇宙の問題が発生します。