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