# 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. – jmite Sep 1 '17 at 19:05
• This question has some answers here. – Anton Trunov Sep 1 '17 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. – Gilles 'SO- stop being evil' Sep 2 '17 at 19:39

Coq has 3 "big" types:

• Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$. This allows terms that are only used for proof to be erased in any code generated by Coq.
• 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.


• Coq does not have proof irrelevance for Prop unless you add it as an axiom. – Geoff Mar 15 '19 at 23:27