O que é diferente entre Set e Type in Coq? [fechadas]

Os tipos AFAIU podem ser a Setcujos elementos são programas ou a propositioncujos elementos são Provas. Então, com base neste entendimento:

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

O código a seguir deve ser compilado, mas isso não ocorre devido ao seguinte erro. Se eu mudar Setcom Typeou o outro Typecom Setele compila bem. Alguém pode me ajudar a entender o que significa o seguinte erro? Estou tentando me ensinar Coq usando o livro Software Foundations.

Erro:

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

Coq possui 3 tipos "grandes":

• Prop$p_1, p_2 : P$$p_1 = p_2$
• Set$1 = 2$Set
• Type é um supertipo de ambos, permitindo escrever código uma vez que funcione com

Tenho certeza de que seu erro é porque você está definindo um Setcujos parâmetros podem ser Type, o que significa que podem ser Prop, o que não é permitido. Se você mudar para isso:

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

seu código deve funcionar.