proposition: Lemma make_algebra_z_iso_inv_action_ax : ∏ n f a, mor_action_ax (identity T) make_algebra_z_iso_inv_data (@action T A') (@action T A) n f a.
proof: Proof. intros n f a. refine (!_ @ maponpaths (λ x, x _) (z_iso_inv_after_z_iso F)). apply (maponpaths (inv_from_z_iso F)). refine (Haction _ _ _ @ _). apply maponpaths. apply funextfun. intro i. apply (eqtohomot (z_iso_after_z_iso_inv F)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Cartesian UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.AlgebraCategoryCore UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryCategory