The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

You can name the Type:

Definition typ := Type.
Inductive u : typ := ...

or

Universe U.
Inductive u : Type@{U} := ...

or

Inductive u@{U} : Type@{U} := ...
(* in this case if the inductive has more universes involved you will get error 
"universe ... is unbound",
   eg "Inductive u@{u} (A:Type) : Type@{U} := ..."
   either name those universes or use "Inductive u@{u +} ..." *)

Gaëtan Gilbert

On 15/01/2024 12:48, Nicolas Magaud wrote:
> Dear Coq-club members,
>
> In some recent experiments with Coq 8.18.0, I try and define an inductive 
> definition in Type. Unexpectedly, when printing the defined object, it has 
> type Set rather that Type.
>
> Here are some simple examples where I would expect objects to belong to Type 
> (as stated in the definition) but they actually belongs to Set or Prop.
>
> Is there any way to force them to live in Type ?
>
> Inductive u : Type := c.
> Print u.
> (* Inductive u : Prop :=  c : u. *)
>
> Inductive t : Type := d : nat -> t.
> Print t.
> (* Inductive t : Set :=  d : nat -> t. *)
>
> Thanks in advance for any explanation you can provide.
>
> Best regards,
>
> Nicolas Magaud