Lemma qequnivandpr {X : UU} (Y : hSet) (R : hrel X) (f : compfun R Y) (x : X) : paths (qequniv Y R f (toqeq R x)) (f x). Proof. intros. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.