Definition istranslogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : istrans L) : istrans R. Proof. intros. intros x1 x2 x3 r12 r23. apply ((pr1 (lg _ _)) (isl _ _ _ ((pr2 (lg _ _)) r12) ((pr2 (lg _ _)) r23))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.