Definition H : functor [C, D'] [C, D] := BinProduct_of_functors _ _ PCD H1 H2. Local Definition θ_ob_fun (X : [C, D']) (Z : category_Ptd C) : ∏ c : C, (functor_composite_data (pr1 Z) (BinProduct_of_functors_data C D PD (H1 X) (H2 X))) c --> (BinProduct_of_functors_data C D PD (H1 (functor_composite (pr1 Z) X)) (H2 (functor_composite (pr1 Z) X))) c. Proof. intro c. apply BinProductOfArrows. - exact (pr1 (θ1 (X ⊗ Z)) c). - exact (pr1 (θ2 (X ⊗ Z)) c). 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.