Library UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal
**********************************************************
Ralph Matthes
2019, change to z_iso as base notion in 2021
**********************************************************
Contents :
- build monoidal category for the endofunctors
Require Import UniMath.Foundations.PartD.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory.
Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
Local Open Scope cat.
Section Endofunctors_as_monoidal_category.
Context (C : category).
Definition monoidal_cat_of_endofunctors: monoidal_cat := monoidal_cat_from_bicat_and_ob(C:=bicat_of_cats) C.
we need this high-level view in order to be able to instantiate montrafotargetbicat_moncat in ActionBasedStrongFunctorsMonoidal