Definition acat_to_acti_data : psfunctor_data ACAT ACTI. Proof. use make_psfunctor_data. - exact acat_to_acti_on_ob. - exact (λ a1 a2 f, acat_to_acti_on_mor f). - intros a1 a2 f g α. exists (pr1 α). abstract (intro v; use nat_trans_eq; [apply homset_property | exact (λ c, pr2 α v c)]). - intro a. use tpair. + apply nat_trans_id. + abstract (intro v; use nat_trans_eq; [apply homset_property | ] ; intro c; cbn ; unfold identity_lineator_data ; rewrite ! id_left ; rewrite id_right ; apply (! bifunctor_leftid (_ ,, pr122 a) _ _)). - intros a1 a2 a3 f g. use tpair. { simpl. apply nat_trans_id. } abstract (intro v; use nat_trans_eq; [apply homset_property | intro c; cbn; rewrite (bifunctor_leftid (_ ,, pr122 a3)); rewrite ! id_left; rewrite ! id_right; apply idpath]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActegories. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat. Require Import UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Import BifunctorNotations. Section ActegoryFromObject. End ActegoryFromObject. Section FromActegoriesToActionsInCat. Import MonoidalNotations. End FromActegoriesToActionsInCat. Section FromActionInCatToActegories. End FromActionInCatToActegories.