Lemma istransandirrefltoasymm {X : UU} {R : hrel X} (is1 : istrans R) (is2 : isirrefl R) : isasymm R. Proof. intros. intros a b rab rba. apply (is2 _ (is1 _ _ _ rab rba)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.