proposition: 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: Proof. intros. apply idpath. Defined.
imports: UniMath.Foundations.Propositions