Lemma test {X : UU} (R : eqrel X) (Y : hSet) (f : setquot R -> Y) : paths f (setquotuniv R Y (funcomp (setquotpr R) f) (λ x x' : X, λ r : R x x', maponpaths f (iscompsetquotpr R x x' r))).
Require Import UniMath.Foundations.UnivalenceAxiom.