Definition is_univalent_Strong_Functor_category (Mon_V : monoidal_cat) (A : category) (A' : univalent_category) (actn : action Mon_V A) (actn' : action Mon_V A') : is_univalent (Strong_Functor_category Mon_V actn actn'). Proof. apply SIP. - exact (is_univalent_functor_category A _ (pr2 A')). - apply Strong_Functor_category_Pisset. - apply Strong_Functor_category_Hstandard. 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.