Definition pullback_glue_pullback {a b c e : C} {f : b --> a} {g : c --> a} {h : e --> b} (pbr : Pullback f g) (pbl : Pullback h (PullbackPr1 pbr)) : Pullback (h · f) g. Proof. use make_Pullback. + exact pbl. + exact (PullbackPr1 pbl). + exact ((PullbackPr2 pbl) · (PullbackPr2 pbr)). + abstract (use glueSquares; [ exact (PullbackPr1 pbr) | use (PullbackSqrCommutes pbr) | use PullbackSqrCommutes ]). + use (isPullbackGluedSquare _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (isPullback_Pullback pbr) (isPullback_Pullback pbl)). 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.