Definition maps_pb_squares_to_pb_squares := ∏ (a b c d : C) (f : C ⟦b, a⟧) (g : C ⟦c, a⟧) (h : C⟦d, b⟧) (k : C⟦d,c⟧) (H : h · f = k · g), maps_pb_square_to_pb_square H. End functor_on_square. Section pullbacks_pointwise. Context {C D : category}. Let CD := [C, D]. Context {F G H J : CD} {a : CD ⟦G, F⟧} {b : CD ⟦H, F⟧} {c : CD⟦J,G⟧} {d : CD⟦J, H⟧} (Hcomm : c · a = d · b). Arguments make_Pullback {_ _ _ _ _ _ _ _ _ _ } _ . Let Hcommx x := nat_trans_eq_pointwise Hcomm x. Local Definition g (T : ∏ x, isPullback (Hcommx x)) (E : CD) (h : CD ⟦ E, G ⟧) (k : CD ⟦ E, H ⟧) (Hhk : h · a = k · b) : ∏ x, D ⟦ pr1 E x, pr1 J x ⟧. Proof. intro x; apply (PullbackArrow (make_Pullback (T x)) _ (pr1 h x) (pr1 k x)). abstract (apply (nat_trans_eq_pointwise Hhk)). 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.