proposition: Lemma iso_inv_app_ax : ∏ n f, mor_app_ax iso_inv_data n f.
proof: Proof. intros n f. refine (!_ @ maponpaths (λ x, (x : algebraic_theory_morphism _ _) (S n) _) (z_iso_inv_after_z_iso F) ). apply (maponpaths ((inv_from_z_iso F : algebraic_theory_morphism _ _) (S n))). refine (Happ _ _ @ _). apply maponpaths. exact (maponpaths (λ x, (x : algebraic_theory_morphism _ _) n f) (z_iso_after_z_iso_inv F)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategory UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples