Lemma quotrellogeq {X : UU} {R : eqrel X} {L L' : hrel X} (is : iscomprelrel R L) (is' : iscomprelrel R L') (lg : ∏ x x', L x x' <-> L' x x') (x x' : setquot R) : (quotrel is x x') <-> (quotrel is' x x'). Proof. intros. split. - apply (quotrelimpl is is' (λ x0 x0', pr1 (lg x0 x0')) x x'). - apply (quotrelimpl is' is (λ x0 x0', pr2 (lg x0 x0')) x x'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.