When we define an inductive type, `rec`

,`rect`

,`ind`

and `sind`

get made as well, right?

These are induction principles tailored for Set, Type, Prop and SProp, isn't it?

Why were seperate lemmas needed for Set and Type? Couldn't `rect`

stand in for `rec`

as well?

Was just looking for use cases where rec is needed.

```
Check nat_rec.
(*
nat_rec
: forall P : nat -> Set,
P 0 ->
(forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)
Check nat_rect.
(*
nat_rect
: forall P : nat -> Type,
P 0 ->
(forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)
```

The type of P is the only thing that differs between ind, sind, rec and rect, right?

Or is that only in the case of not-so-complex types?

with -impredicative-set it's possible to define types that have _rec but not _rect

Last updated: Jun 14 2024 at 19:02 UTC