Lemma istotalquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : istotal L) : istotal (quotrel is). Proof. intros. unfold istotal. apply (setquotuniv2prop R (λ x1 x2, hdisj _ _)). intros x x'. intros r r'. apply (isl x x' r r'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.