Lemma isinclpr1qeq {X : UU} (R : hrel X) (Y : hSet) : isincl (@pr1 _ (λ phi : F X Y R, ∏ psi : F X Y R -> Y, paths (psi phi) (Fv R (compfuncomp R (make_compfun R _ (iscompFi R)) psi) phi))). Proof. intros. apply isinclpr1. intro phi. apply impred. intro psi. apply (pr2 Y). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.