Definition isInitial_category_binproduct (x : category_binproduct C₁ C₂) (H₁ : isInitial C₁ (pr1 x)) (H₂ : isInitial C₂ (pr2 x)) : isInitial (category_binproduct C₁ C₂) x. Proof. intros w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use pathsdirprod ; [ exact (InitialArrowUnique (_ ,, H₁) _ _ @ !(InitialArrowUnique (_ ,, H₁) _ _)) | exact (InitialArrowUnique (_ ,, H₂) _ _ @ !(InitialArrowUnique (_ ,, H₂) _ _)) ]). - exact (InitialArrow (_ ,, H₁) (pr1 w) ,, InitialArrow (_ ,, H₂) (pr2 w)). 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.PrecategoryBinProduct. 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.