Definition tensor_pointedfunctor_data: functor_data (Ptd ⊠ Ptd) Ptd. Proof. use make_functor_data. - intros PF1PF2. exact (ptd_compose C (pr1 PF1PF2) (pr2 PF1PF2)). - intros PF1PF2 PF1PF2' α1α2. induction α1α2 as [α1 α2]. induction PF1PF2 as [PF1 PF2]. induction PF1PF2' as [PF1' PF2']. cbn in α1, α2 |- *. set (α1' := pr1 α1). set (α2' := pr1 α2). exists (# (functorial_composition _ _ _) (α1',,α2': [C, C] ⊠ [C, C]⟦(pr1 PF1,,pr1 PF2),(pr1 PF1',,pr1 PF2')⟧)). abstract ( intro c; assert (α1commutes := ptd_mor_commutes _ α1); assert (α2commutes := ptd_mor_commutes _ α2); cbn; etrans; [ apply maponpaths; apply nat_trans_ax | rewrite <- α1commutes; repeat rewrite <- assoc; apply maponpaths; rewrite assoc; unfold α2'; etrans; [apply cancel_postcomposition; apply α2commutes | etrans; [assert (η2'nat := nat_trans_ax (pr2 PF2')); apply pathsinv0, η2'nat | apply idpath]]] ). Defined.
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.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.