Lemma setquotl0 {X : UU} (R : eqrel X) (c : setquot R) (x : c) : setquotpr R (pr1 x) = c. 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.
Require Import UniMath.Foundations.UnivalenceAxiom.