Definition Strong_Functor_category_displayed : disp_cat (functor_category A A'). Proof. use disp_cat_from_SIP_data. - intro F. exact (actionbased_strength Mon_V actn actn' F). - intros F1 F2 FF1 FF2 η. exact (∏ a v, Strong_Functor_Category_mor_diagram (F1,,FF1) (F2,,FF2) η a v). - intros F1 F2 FF1 FF2 η. do 2 (apply impred; intro). apply homset_property. - intros F FF a v. apply Strong_Functor_Category_Mor_id_subproof. - intros F G H FF GG HH η η' ηmor η'mor a v. simpl in ηmor, η'mor. exact (Strong_Functor_Category_Mor_comp_subproof (F,,FF) (G,,GG) (H,,HH) η η' ηmor η'mor a v). 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.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength.