Lemma isPullback_preimage_square : isPullback H. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monics. Definition UnivProductFromPullback (c d a : C) (f : a --> c) (g : a --> d): exists (UnivProductFromPullback c d a f g). Definition BinProductsFromPullbacks : BinProducts C := BinProduct_Pullback.