Lemma etaqeq {X : UU} (Y : hSet) (R : hrel X) (psi : qeq R -> Y) (phi : qeq R) : paths (psi phi) (qequniv Y R (compfuncomp R (make_compfun R _ (iscomptoqeq Y R)) psi) phi).
Require Import UniMath.Foundations.UnivalenceAxiom.