proposition: Lemma isPullback_image_square : isPullback (functor_on_square H).
proof: 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.
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