proposition: Lemma setquotl0 {X : UU} (R : eqrel X) (c : setquot R) (x : c) : setquotpr R (pr1 x) = c.
proof: Proof. apply (invmaponpathsincl _ (isinclpr1setquot R)). apply funextsec; intro x0. apply hPropUnivalence; intro r. - exact (eqax1 (pr2 c) (pr1 x) x0 r (pr2 x)). - exact (eqax2 (pr2 c) (pr1 x) x0 (pr2 x) r). Defined.
imports: UniMath.Foundations.Propositions