proposition: Theorem setquotuniv2comm {X : UU} (R : eqrel X) (Y : hSet) (f : X -> X -> Y) (is : iscomprelfun2 R f) : ∏ x x' : X, setquotuniv2 R Y f is (setquotpr R x) (setquotpr R x') = f x x'.
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.Foundations.Propositions