Definition BinProductsFromPullbacks : BinProducts C := BinProduct_Pullback. End binproduct_from_pullback. Section pullbacks_functor_category. Context (D C : category) (hpb : @Pullbacks C). Local Lemma FunctorcategoryPullbacks_eq (F G H : functor D C) (α : nat_trans G F) (β : nat_trans H F) (a b : D) (f : D ⟦a, b⟧) : PullbackPr1 (hpb _ _ _ (α a) (β a)) · # G f · α b = PullbackPr2 (hpb _ _ _ (α a) (β a)) · # H f · β b. Proof. set (pba := hpb _ _ _ (α a) (β a)). repeat rewrite <- assoc. rewrite (nat_trans_ax α a b f). rewrite (nat_trans_ax β a b f). repeat rewrite assoc. apply cancel_postcomposition. exact (PullbackSqrCommutes pba). Qed. Local Lemma FunctorcategoryPullbacks_isfunctor (F G H : functor D C) (α : nat_trans G F) (β : nat_trans H F) : is_functor (make_functor_data (λ d : D, hpb (F d) (G d) (H d) (α d) (β d)) (λ (a b : D) (f : D ⟦ a, b ⟧), PullbackArrow (hpb (F b) (G b) (H b) (α b) (β b)) (hpb (F a) (G a) (H a) (α a) (β a)) (PullbackPr1 (hpb (F a) (G a) (H a) (α a) (β a)) · # G f) (PullbackPr2 (hpb (F a) (G a) (H a) (α a) (β a)) · # H f) (FunctorcategoryPullbacks_eq F G H α β a b f))). Proof. split. - intros x. apply pathsinv0. cbn. eapply PullbackArrowUnique. + rewrite functor_id. rewrite id_left. rewrite id_right. apply idpath. + rewrite functor_id. rewrite id_left. rewrite id_right. apply idpath. - intros x y z f g. set (px := hpb (F x) (G x) (H x) (α x) (β x)). set (py := hpb (F y) (G y) (H y) (α y) (β y)). set (pz := hpb (F z) (G z) (H z) (α z) (β z)). set (pz1 := PullbackArrow_PullbackPr1 pz py (PullbackPr1 py · # G g) (PullbackPr2 py · # H g) (FunctorcategoryPullbacks_eq F G H α β y z g)). set (pz2 := PullbackArrow_PullbackPr2 pz py (PullbackPr1 py · # G g) (PullbackPr2 py · # H g) (FunctorcategoryPullbacks_eq F G H α β y z g)). set (py1 := PullbackArrow_PullbackPr1 py px (PullbackPr1 px · # G f) (PullbackPr2 px · # H f) (FunctorcategoryPullbacks_eq F G H α β x y f)). set (py2 := PullbackArrow_PullbackPr2 py px (PullbackPr1 px · # G f) (PullbackPr2 px · # H f) (FunctorcategoryPullbacks_eq F G H α β x y f)). apply pathsinv0. cbn. fold px. fold py. fold pz. eapply PullbackArrowUnique. + rewrite functor_comp. rewrite assoc. rewrite <- assoc. rewrite pz1. rewrite assoc. apply cancel_postcomposition. apply py1. + rewrite functor_comp. rewrite assoc. rewrite <- assoc. rewrite pz2. rewrite assoc. apply cancel_postcomposition. apply py2. Qed. Local Definition FunctorcategoryPullbacks_functor (F G H : functor D C) (α : nat_trans G F) (β : nat_trans H F) : functor D C. Proof. use make_functor. - use make_functor_data. + intros d. exact (PullbackObject (hpb _ _ _ (α d) (β d))). + intros a b f. use (PullbackArrow (hpb _ _ _ (α b) (β b)) _ (PullbackPr1 (hpb _ _ _ (α a) (β a)) · (# G f)) (PullbackPr2 (hpb _ _ _ (α a) (β a)) · (# H f)) (FunctorcategoryPullbacks_eq F G H α β a b f)). - exact (FunctorcategoryPullbacks_isfunctor F G H α β). 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.