Lemma is_omega_cocont_BinProduct_of_Signatures (S1 S2 : Signature C D D') (h1 : is_omega_cocont S1) (h2 : is_omega_cocont S2) (PC: BinProducts D') (hE : ∏ x, is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C D PD) x)) : is_omega_cocont (BinProduct_of_Signatures S1 S2). Proof. apply is_omega_cocont_BinProduct_of_functors; try assumption. apply (BinProducts_functor_precat _ _ PC). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials.