Lemma isaprop_iscotrans {X : UU} (rel : hrel X) : isaprop (iscotrans rel). Proof. apply impred_isaprop ; intro x. apply impred_isaprop ; intro y. apply impred_isaprop ; intro z. apply isapropimpl. now apply pr2. Qed.