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. intros. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.