Lemma isPullbackGluedSquare : isPullback (i · f) g m (j · k) glueSquares. Proof. apply make_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)). intro t. apply subtypePath. - intro a0. apply isapropdirprod; apply hs. - simpl. destruct t as [t [Ht1 Ht2]]. simpl in *. apply PullbackArrowUnique. + assumption. + apply PullbackArrowUnique. * rewrite <- Ht1. repeat rewrite <- assoc. rewrite H2. apply idpath. * rewrite <- assoc. assumption. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.