proposition: Lemma isPullback_preimage_square : isPullback H.
proof: Proof. use make_isPullback. intros e x y Hxy. set (T := maponpaths (#F) Hxy). set (T' := !functor_comp _ _ _ @ T @ functor_comp _ _ _ ). set (TH := X _ _ _ T'). set (FxFy := pr1 (pr1 TH)). set (HFxFy := pr2 (pr1 TH)). simpl in HFxFy. set (xy := fully_faithful_inv_hom Fff _ _ FxFy). use tpair. - exists xy. set (t := pr1 HFxFy). set (p := pr2 HFxFy). split. + use (invmaponpathsweq (make_weq _ (Fff _ _ ))). simpl. rewrite functor_comp. assert (XX:=homotweqinvweq (make_weq _ (Fff e d ))). simpl in XX. unfold xy. simpl. eapply pathscomp0. eapply cancel_postcomposition. assert (XXX := XX FxFy). apply XX. exact t. + use (invmaponpathsweq (make_weq _ (Fff _ _ ))). simpl. rewrite functor_comp. assert (XX:=homotweqinvweq (make_weq _ (Fff e d ))). simpl in XX. unfold xy. simpl. eapply pathscomp0. eapply cancel_postcomposition. assert (XXX := XX FxFy). apply XX. exact p. - simpl. intro t. apply subtypePath. + intro kkkk. apply isapropdirprod; apply C. + simpl. use (invmaponpathsweq (make_weq _ (Fff _ _ ))). simpl. unfold xy. assert (XX:=homotweqinvweq (make_weq _ (Fff e d ))). simpl in XX. apply pathsinv0. eapply pathscomp0. apply XX. apply pathsinv0. apply path_to_ctr. destruct (pr2 t) as [H1 H2]. split. * assert (X1:= maponpaths (#F) H1). eapply pathscomp0. apply (!functor_comp _ _ _ ). apply X1. * assert (X2:= maponpaths (#F) H2). eapply pathscomp0. apply (!functor_comp _ _ _). apply X2. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics