Lemma BinProducts_Signature_category : BinProducts (Signature_category C D D'). Proof. intros Ht1 Ht2. use make_BinProduct. - apply (BinProduct_of_Signatures _ _ _ BD Ht1 Ht2). - apply Signature_category_pr1. - apply Signature_category_pr2. - apply isBinProduct_Signature_category. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures.