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. intros. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.