Theorem setquotunivcomm {X : UU} (R : eqrel X) (Y : hSet) (f : X -> Y) (is : iscomprelfun R f) : ∏ x : X, setquotuniv R Y f is (setquotpr R x) = f x. Proof. intros. unfold setquotuniv. unfold setquotpr. simpl. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.