Lemma quotrelimpl {X : UU} {R : eqrel X} {L L' : hrel X} (is : iscomprelrel R L) (is' : iscomprelrel R L') (impl : ∏ x x', L x x' -> L' x x') (x x' : setquot R) (ql : quotrel is x x') : quotrel is' x x'. Proof. intros. generalize x x' ql. assert (int : ∏ (x0 x0' : setquot R), isaprop (quotrel is x0 x0' -> quotrel is' x0 x0')). { intros x0 x0'. apply impred. intro. apply (pr2 _). } apply (setquotuniv2prop _ (λ x0 x0', make_hProp _ (int x0 x0'))). intros x0 x0'. change (L x0 x0' -> L' x0 x0'). apply (impl x0 x0'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.