proposition: Lemma functor_to_is_algebraic_theory_morphism : is_algebraic_theory_morphism functor_to_algebraic_theory_morphism_data.
proof: Proof. use make_is_algebraic_theory_morphism. - intros n i. refine (maponpaths (λ x, _ · x · _) (F_preserves_power_pr _) @ _). apply z_iso_inv_to_right. apply z_iso_inv_on_right. apply assoc'. - intros m n f g. refine (assoc' _ _ _ @ _). apply z_iso_inv_on_right. do 2 refine (_ @ assoc' _ _ _). refine (_ @ maponpaths (λ x, x · _) (assoc' _ _ _)). apply (maponpaths (λ x, x · _)). refine (functor_comp _ _ _ @ _). apply (maponpaths (λ x, x · _)). refine (F_preserves_product_arrow _ _ @ _). apply (maponpaths (λ x, x · _)). apply ProductArrow_eq. intro i. refine (ProductPrCommutes _ _ _ _ _ _ _ @ !_). refine (assoc' _ _ _ @ _). refine (maponpaths _ (ProductPrCommutes _ _ _ _ _ _ _) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc _ _ _) @ _). refine (maponpaths (λ x, x · _ · _) (z_iso_inv_after_z_iso _) @ _). exact (maponpaths (λ x, x · _) (id_left _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples