What is different between Set and Type in Coq? [closed]

AFAIU types can be a Set whose elements are programs or a proposition whose elements are Proofs. So based on this understanding:

Inductive prod (X Y: Type) : Set :=
| pair: X -> Y -> prod X Y.


Following code should compile but it does not due to the following error. If I change Set with Type or the other Type with Set it compiles fine. Can someone help me understand what the following error means? I am trying to teach myself Coq using Software Foundations book.

Error:

Error: Large non-propositional inductive types must be in Type.

• Theorem provers have always been a grey area for CS.SE, but I'm guessing this is a good candidate for mods to migrate to StackOverflow. Commented Sep 1, 2017 at 19:05
• This question has some answers here. Commented Sep 1, 2017 at 22:41
• @jmite Given that this question is about the calculus of constructions with Coq just serving as the concrete syntax, I think it's on-topic here. Commented Sep 2, 2017 at 19:39

Coq has 4 "big" types:

• Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It is also erased at run-time, meaning you can't pattern match on a Prop value to build a Type value, unless there's only one possibility.
• SProp is like Prop, but with definitional proof irrelevance, meaning that if $$p_1, p_2 : P$$ then $$p_1 = p_2$$.
• Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming $$1 = 2$$. The Set parts remain during code extraction.
• Type is a supertype of both of these, allowing you to write code once that works with either

I'm pretty sure your error is because you're defining a Set whose parameters can be Type, which means they can be Prop, which isn't allowed. If you change to this:

Inductive prod (X Y: Set) : Set :=
| pair: X -> Y -> prod X Y.


your code should work.

EDIT: Updated to include SProp.

• Coq does not have proof irrelevance for Prop unless you add it as an axiom. Commented Mar 15, 2019 at 23:27
• @Geoff My mistake, updated to reflect this. Commented Oct 20, 2021 at 19:34