proposition: Theorem setquot2univcomm {X : UU} (R : hrel X) (Y : hSet) (F : X -> Y) (iscomp : iscomprelfun R F) (x : X) : setquot2univ _ _ F iscomp (setquot2pr R x) = F x.
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.Foundations.Propositions