Lemma iscomptoqeq {X : UU} (Y : hSet) (R : hrel X) : iscomprelfun R (@toqeq X Y R). Proof. intros. intros x x' r. unfold toqeq. apply (invmaponpathsincl _ (isinclpr1qeq R Y)). apply (@iscompFi X Y R x x' r). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.