Library UniMath.SubstitutionSystems.EquivalenceLaxLineatorsHomogeneousCase

links the homogeneous instance of lax lineators with the linears based on the self action

this is w.r.t. the elementary notion of the monoidal category of endofunctors, not the instance to the bicategory of categories of the general bicategorical constructions

Author: Ralph Matthes 2023

Require Import UniMath.Foundations.PartD.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary.
Require Import UniMath.CategoryTheory.Actegories.Examples.ActionOfEndomorphismsInCATElementary.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Actegories.Actegories.
Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories.
Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories.
Require Import UniMath.CategoryTheory.coslicecat.
Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects.

Import MonoidalNotations.

Local Open Scope cat.

Section FixACategory.

  Context (C : category).

Local Definition endoCAT : category := [C , C ].
Local Definition Mon_endo_CAT : monoidal endoCAT := monendocat_monoidal C.
Local Definition ptdendo_CAT : category := coslice_cat_total endoCAT I_{Mon_endo_CAT }.
Local Definition Mon_ptdendo_CAT : monoidal ptdendo_CAT := monoidal_pointed_objects Mon_endo_CAT.
Local Definition actegoryPtdEndosOnFunctors_CAT (E : category) : actegory Mon_ptdendo_CAT [C ,E ]
   := reindexed_actegory Mon_endo_CAT (actegory_from_precomp_CAT C E) Mon_ptdendo_CAT
        (forget_monoidal_pointed_objects_monoidal Mon_endo_CAT).

Local Lemma action_in_actegoryPtdEndosOnFunctors_CAT_as_actegory_with_canonical_pointed_action :
   actegory_action Mon_ptdendo_CAT (actegoryPtdEndosOnFunctors_CAT C) =
     actegory_action Mon_ptdendo_CAT (actegory_with_canonical_pointed_action Mon_endo_CAT).
Proof.
   use total2_paths_f.
   2: { apply WhiskeredBifunctors.isaprop_is_bifunctor. }
   cbn.
   apply idpath.
Qed.

End FixACategory.