I am surprised to see the following behavior:
Check ((True : Prop) : Set).
=============================================
(True : Prop) : Set
: Set
It however does not work the other way around:
Check ((True : Set) : Prop).
=============================================
Error:
The term "True : Set" has type "Set" while it is expected to have type
"Prop" (universe inconsistency: Cannot enforce Set <= Prop).
It very much looks like Prop <: Set, but I have never seen that stated explicitly anywhere. My doubts are backed by the differences between those two universes, as each seems so have features which the other lacks. I also have not heard that Coq has any sort of subtyping to be honest.
How is it then? Is Prop a true subtype of Set or is there some other magic going on behind the scenes?
Since I currently don't have enough reputation to comment on your question, here's a short answer: Yes, Prop is indeed a subtype of Set. Check out https://coq.inria.fr/distrib/current/refman/language/cic.html#subtyping-rules, rule #4.
Intuitively, Set is the sort of all "small" data types, while Prop intends to be the sort of all logical propositions. You can convert from Prop to Set but not the other way around.