Definition pointedfunctors_disp_cat : disp_cat (cat_of_endofunctors C). Proof. use disp_struct. - intro F. exact (functor_identity C ⟹ pr1 F). - intros F G ptF ptG α. exact (∏ c : C, ptF c · pr1 α c = ptG c). - intros F G ptF ptG α. apply impred; intro c. apply C. - intros F ptF c. apply id_right. - abstract (intros F G H α β; cbn; intros ptF ptG ptH Hα Hβ c; rewrite assoc, Hα, Hβ; 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.