Lemma iscompFi {X Y : UU} (R : hrel X) : iscomprelfun R (Fi X Y R). Proof. intros. intros x x' r. unfold Fi. apply funextfun. intro f. apply (pr2 f x x' r). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.