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