Definition binproducts_in_iso_comma (HC₁ : BinProducts C₁) (HC₂ : BinProducts C₂) : BinProducts (iso_comma F G). Proof. intros x y. pose (FP := make_BinProduct _ _ _ _ _ _ (HF (pr11 x) (pr11 y) _ (BinProductPr1 _ (HC₁ (pr11 x) (pr11 y))) (BinProductPr2 _ (HC₁ (pr11 x) (pr11 y))) (isBinProduct_BinProduct _ (HC₁ (pr11 x) (pr11 y))))). pose (GP := make_BinProduct _ _ _ _ _ _ (HG (pr21 x) (pr21 y) _ (BinProductPr1 _ (HC₂ (pr21 x) (pr21 y))) (BinProductPr2 _ (HC₂ (pr21 x) (pr21 y))) (isBinProduct_BinProduct _ (HC₂ (pr21 x) (pr21 y))))). use make_BinProduct. - simple refine ((_ ,, _) ,, _). + exact (BinProductObject _ (HC₁ (pr11 x) (pr11 y))). + exact (BinProductObject _ (HC₂ (pr21 x) (pr21 y))). + exact (binproduct_of_z_iso FP GP (pr2 x) (pr2 y)). - simple refine ((_ ,, _) ,, _). + exact (BinProductPr1 _ (HC₁ (pr11 x) (pr11 y))). + exact (BinProductPr1 _ (HC₂ (pr21 x) (pr21 y))). + exact (!(BinProductOfArrowsPr1 _ GP FP (pr12 x) (pr12 y))). - simple refine ((_ ,, _) ,, _). + exact (BinProductPr2 _ (HC₁ (pr11 x) (pr11 y))). + exact (BinProductPr2 _ (HC₂ (pr21 x) (pr21 y))). + exact (!(BinProductOfArrowsPr2 _ GP FP (pr12 x) (pr12 y))). - use isBinProduct_in_iso_comma. + apply isBinProduct_BinProduct. + apply isBinProduct_BinProduct. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.