proposition: Lemma isaprop_iscotrans {X : UU} (rel : hrel X) : isaprop (iscotrans rel).
proof: Proof. apply impred_isaprop ; intro x. apply impred_isaprop ; intro y. apply impred_isaprop ; intro z. apply isapropimpl. now apply pr2. Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets