Lemma iscomprelrellogeqf2 {X : UU} (R : hrel X) {L L' : hrel X} (lg : hrellogeq L L') (is : iscomprelrel R L) : iscomprelrel R L'. Proof. intros. intros x x' x0 x0' r r0. assert (e : paths (L x x0) (L' x x0)). { apply hPropUnivalence. - apply (pr1 (lg _ _)). - apply (pr2 (lg _ _)). } assert (e' : paths (L x' x0') (L' x' x0')). { apply hPropUnivalence. - apply (pr1 (lg _ _)). - apply (pr2 (lg _ _)). } induction e. induction e'. apply (is _ _ _ _ r r0). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.