Definition fromsubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R)) (p : P) : setquot (resrel R (funcomp (setquotpr R) P)). Proof. intros. split with (fun rp : carrier (funcomp (setquotpr R) P) => (pr1 p) (pr1 rp)). apply (iseqclassresrel R (funcomp (setquotpr R) P) _ (pr2 (pr1 p))). intros x px. set (e := setquotl0 R _ (make_carrier _ x px)). simpl in e. unfold funcomp. rewrite e. apply (pr2 p). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.