proposition: Lemma U_action_χ_is_nat_z_iso : is_nat_z_iso U_action_χ_nat_trans.
proof: Proof. intro x. pose (k := ob1 (ob1 x)); pose (k' := ob2 (ob1 x)); pose (k'' := ob2 x). use is_z_iso_comp_of_is_z_isos. - exact (pr2 α_A ((k, U k'), U k'')). - use is_z_iso_tensor_z_iso. + use identity_is_z_iso. + exact (strong_monoidal_functor_μ_is_nat_z_iso U (k', k'')). Defined.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal