proposition: Lemma is_nat_trans_App_θ_data: is_nat_trans _ _ App_θ_data.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.BinSumOfSignatures UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits