proposition: Lemma isPullbackGluedSquare : isPullback (i · f) g m (j · k) glueSquares.
proof: Proof. unfold isPullback. intros y p q. intro Hrt. assert (ex : (p · i) · f = q · g). { rewrite <- Hrt. rewrite assoc; apply idpath. } set (rt := P1 _ (p · i) q ex). set (Ppiq := pr1 (pr1 (rt))). assert (owiej : p · i = Ppiq · h). { apply pathsinv0. apply (pr1 (pr2 (pr1 rt))). } set (rt' := P2 _ p Ppiq owiej). set (awe := pr1 (pr1 rt')). assert (Hawe1 : awe · m = p). { exact (pr1 (pr2 (pr1 rt'))). } assert (Hawe2 : awe · (j · k) = q). { rewrite assoc. set (X := pr2 (pr2 (pr1 rt'))). simpl in X. unfold awe. rewrite X. exact (pr2 (pr2 (pr1 rt))). } exists (tpair _ awe (make_dirprod Hawe1 Hawe2)). abstract ( intro t; apply subtypePath; [ intro a0; apply isapropdirprod; apply C | destruct t as [t [Ht1 Ht2]]; apply PullbackArrowUnique; [ assumption | apply PullbackArrowUnique; [ rewrite <- Ht1; repeat rewrite <- assoc; rewrite H2; apply idpath | rewrite <- assoc; assumption ] ] ]). 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