Definition pointedfunctors_disp_tensor_data : disp_bifunctor_data (monoidal_of_endofunctors C) pointedfunctors_disp_cat pointedfunctors_disp_cat pointedfunctors_disp_cat. Proof. use tpair. - intros F G ptF ptG. exact (# (post_comp_functor (functor_identity C)) ptF · # (pre_comp_functor F) ptG). - split. + intros F G1 G2 β ptF ptG1 ptG2 Hβ. cbn. intro c. rewrite <- Hβ. apply assoc'. + intros F1 F2 G α ptF1 ptF2 ptG Hα. cbn. intro c. rewrite <- Hα. do 2 rewrite <- assoc. apply maponpaths. etrans. { apply pathsinv0, (nat_trans_ax ptG). } 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.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal. Require Import UniMath.CategoryTheory.coslicecat. Import MonoidalNotations.