Stream: Coq users

Topic: ✔ Why does the motive in recursion go to set?

view this post on Zulip walker (Sep 25 2023 at 12:57):

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 beU_0why can't we say for instance something like :

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

view this post on Zulip Gaëtan Gilbert (Sep 25 2023 at 12:59):

we have nat_rect for that (the t is for Type I think)

view this post on Zulip walker (Sep 25 2023 at 13:00):

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

view this post on Zulip Notification Bot (Sep 25 2023 at 13:03):

walker has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC