I want to consider the following three (related?) Coq definitions.
Inductive nat1: Prop :=
| z1 : nat1
| s1 : nat1 -> nat1.
Inductive nat2 : Set :=
| z2 : nat2
| s2 : nat2 -> nat2.
Inductive nat3 : Type :=
| z3 : nat3
| s3 : nat3 -> nat3.
All three types give induction principles to prove a proposition holds.
nat1_ind
: forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P
nat2_ind
: forall P : nat2 -> Prop,
P z2 -> (forall n : nat2, P n -> P (s2 n)) -> forall n : nat2, P n
nat3_ind
: forall P : nat3 -> Prop,
P z3 -> (forall n : nat3, P n -> P (s3 n)) -> forall n : nat3, P n
The set and type versions also contain induction principles for definitions over set and type (rec and rect respectively). This is the extent of my knowledge about the difference between Prop and Set; Prop has a weaker induction.
I have also read that Prop is impredicative while Set is predicative, but this seems like a property rather than a defining quality.
While some practical (moral?) differences between Set and Prop are clear, the exact, defining differences between Set and Prop, as well as where they fit into the universe of types is unclear (running check on Prop and Set gives Type (* (Set) + 1*)), and I'm not exactly sure how to interpret this...