```
Inductive nat : Set :=
| O : nat
| S (n: nat) : nat.
Check nat_rec.
(*
nat_rec
: forall P : nat -> Set,
P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n*)
```

is there a particular reason we cannot have `nat_rec: forall P : nat -> Type, ....`

I know in coq we cannot manually describe universe levels manually, but assuming we can, and assuming `Set`

would be`U_0`

why can't we say for instance something like :

`nat_rec: forall P : nat -> Univ U_1234, ....`

?

we have `nat_rect`

for that (the `t`

is for `Type`

I think)

yup spot on, I thought it was not doable at all, which felt odd. Thanks for clarifications.

walker has marked this topic as resolved.

Last updated: Jun 13 2024 at 21:01 UTC