Definition setquotfuncomm {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y) (is : iscomprelrelfun RX RY f) : ∏ x : X, setquotfun RX RY f is (setquotpr RX x) = setquotpr RY (f x). Proof. intros. simpl. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.