Inductive PBox : Prop :=
| wrap : forall P:Prop, P -> PBox.

Inductive TBox : Type :=
| wrap_t : forall T:Type, T -> TBox.

Check (wrap PBox).

Fail Check (wrap_t TBox).
(*
The command has indeed failed with message:
The term "TBox" has type
 "Type@{max(Prop, Top.8+1)}"
while it is expected to have type
 "Type@{Top.8}"
(universe inconsistency: Cannot enforce Top.8 <
Top.8 because Top.8 = Top.8).
*)