Definition preserves_terminal_bindelta_pair_functor {C D₁ D₂ : category} {F : C ⟶ D₁} {G : C ⟶ D₂} (HF : preserves_terminal F) (HG : preserves_terminal G) : preserves_terminal (bindelta_pair_functor F G). Proof. intros x Hx. apply isTerminal_category_binproduct. - apply HF. apply Hx. - apply HG. apply Hx. 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.