Lemma isPullbackGluedSquare : isPullback (i · f) g m (j · k) glueSquares. 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.
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.