What exactly is a Set in COQ : <p>I'm still puzzled what the sort <strong>Set</strong> means in COQ. When do I use <strong>Set</strong> and when do I use <strong>Type</strong>?</p>

<p>In Hott a <strong>Set</strong> is defined as a type, where identity proofs are unique. 
But I think in Coq it has a different interpretation. </p>
