Definition iscotranslogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iscotrans L) : iscotrans R. Proof. intros. intros x1 x2 x3 r13. set (int := isl x1 x2 x3 (pr2 (lg _ _) r13)). generalize int. clear int. simpl. apply hinhfun. apply (coprodf (pr1 (lg x1 x2)) (pr1 (lg x2 x3))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.