Lemma is_nat_trans_App_θ_data: is_nat_trans _ _ App_θ_data. Proof. red. unfold App_θ_data. intros XZ XZ' αβ. apply nat_trans_eq_alt. intro c. simpl. rewrite id_left. rewrite id_right. unfold binproduct_nat_trans_data, BinProduct_of_functors_mor. unfold BinProductOfArrows. etrans; [ apply precompWithBinProductArrow |]. simpl. unfold binproduct_nat_trans_pr1_data. unfold binproduct_nat_trans_pr2_data. simpl. apply BinProductArrowUnique. + rewrite BinProductPr1Commutes. repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinProductPr1Commutes. } apply idpath. + rewrite BinProductPr2Commutes. repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinProductPr2Commutes. } apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.