Lemma isPullback_image_square : isPullback (functor_on_square H). Proof. intros e x y Hxy. apply (squash_to_prop (Fes e)). apply isapropiscontr. intros [e' i]. set (e'c := invmap (FF _ _ ) (i ·y)). set (e'b := invmap (FF _ _ ) (i ·x)). set (Pb := make_Pullback _ X). assert (XX : e'b · f = e'c · g). { apply (invmaponpathsweq (FF _ _ )). cbn. unfold e'b. unfold e'c. repeat rewrite functor_comp. set (T:=homotweqinvweq (FF e' b)). cbn in T. rewrite T; clear T. set (T:=homotweqinvweq (FF e' c)). cbn in T. rewrite T; clear T. repeat rewrite <- assoc. rewrite Hxy. apply idpath. } set (umor := PullbackArrow Pb _ e'b e'c XX). set (umorPr1 := PullbackArrow_PullbackPr1 Pb _ _ _ XX). set (umorPr2 := PullbackArrow_PullbackPr2 Pb _ _ _ XX). cbn in *. use tpair. - exists (inv_from_z_iso i · #F umor ). split. + rewrite <- assoc. apply z_iso_inv_on_right. rewrite <- functor_comp. apply (invmaponpathsweq (invweq (FF _ _ ))). cbn. set (TX:= homotinvweqweq (FF e' b)). cbn in TX. rewrite TX; clear TX. unfold umor; rewrite umorPr1. apply idpath. + rewrite <- assoc. apply z_iso_inv_on_right. rewrite <- functor_comp. apply (invmaponpathsweq (invweq (FF _ _ ))). cbn. set (TX:= homotinvweqweq (FF e' c)). cbn in TX. rewrite TX; clear TX. unfold umor; rewrite umorPr2. apply idpath. - cbn. intro t. apply subtypePath ; [ intro; apply isapropdirprod; apply D | cbn ]. destruct t as [t [Htx Hty]]; cbn. apply (pre_comp_with_z_iso_is_inj i). rewrite assoc. rewrite z_iso_inv_after_z_iso. rewrite id_left. apply (invmaponpathsweq (invweq (FF _ _ ))). cbn. set (TX:= homotinvweqweq (FF e' d)). cbn in TX. rewrite TX; clear TX. apply PullbackArrowUnique. + apply (invmaponpathsweq (FF _ _ )). set (TX:= homotweqinvweq (FF e' d)). cbn in *. rewrite functor_comp, TX; clear TX. rewrite <- assoc. rewrite Htx. unfold e'b. set (TX:= homotweqinvweq (FF e' b)). cbn in *. rewrite TX. apply idpath. + apply (invmaponpathsweq (FF _ _ )). set (TX:= homotweqinvweq (FF e' d)). cbn in *. rewrite functor_comp, TX; clear TX. rewrite <- assoc. rewrite Hty. unfold e'c. set (TX:= homotweqinvweq (FF e' c)). cbn in *. rewrite TX. apply idpath. Qed.
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.