Definition associator_of_pointedfunctors : associator tensor_pointedfunctors. Proof. use make_nat_z_iso. + use make_nat_trans. * intro PFtriple. induction PFtriple as [[PF1 PF2] PF3]. exists (α_functors (pr1 PF1) (pr1 PF2) (pr1 PF3)). abstract ( intro c; cbn; rewrite id_right; apply pathsinv0, assoc ). * abstract ( intros PFtriple PFtriple' αtriple; apply eq_ptd_mor; apply (nat_trans_eq (homset_property C)); intro c; cbn; rewrite id_right; rewrite id_left; rewrite assoc; apply cancel_postcomposition; apply functor_comp ). + intro PFtriple. cbn. apply ptd_mor_z_iso_from_underlying_mor. intro c. cbn. apply identity_is_z_iso. 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.