Theorem setquotfun2comm {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> X -> Y) (is : iscomprelrelfun2 RX RY f) : ∏ (x x' : X), setquotfun2 RX RY f is (setquotpr RX x) (setquotpr RX x') = setquotpr RY (f x x'). Proof. intros. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.