proposition: Lemma functor_to_morphism_preserves_app' : preserves_app' functor_to_algebraic_theory_morphism.
proof: Proof. refine (maponpaths _ (φ_adj_inv_natural_precomp _ _ _ _ _ _) @ !_). refine (φ_adj_inv_natural_precomp (pr2 E') _ _ _ _ _ @ !_). refine (maponpaths (λ x, _ · x · _) (functor_comp _ _ _) @ _). apply z_iso_inv_to_right. apply z_iso_inv_on_right. refine (maponpaths (λ x, _ · x) F_preserves_φ_adj_inv @ _). do 2 refine (assoc _ _ _ @ !_). apply (maponpaths (λ x, x · _)). do 2 refine (assoc _ _ _ @ !_). apply (maponpaths (λ x, x · _)). refine (maponpaths (λ x, x · _) (preserves_binproduct_to_preserves_arrow _ F_preserves_binproduct _ (C'_bin_products _ _) _ _) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ · x · _) (z_iso_after_z_iso_inv _) @ _). refine (maponpaths (λ x, x · _) (id_right _) @ _). apply BinProductArrowsEq; do 2 refine (assoc' _ _ _ @ !_). - do 2 refine (maponpaths _ (BinProductOfArrowsPr1 _ _ _ _ _) @ !_). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (BinProductPr1Commutes _ _ _ _ _ _ _) @ _). refine (maponpaths (λ x, x · _) (functor_comp _ _ _) @ _). refine (maponpaths (λ x, x · _ · _) (preserves_binproduct_to_preserves_pr1 _ F_preserves_binproduct _ (C'_bin_products _ _)) @ _). refine (maponpaths (λ x, _ · x · _) (functor_id _ _) @ _). refine (maponpaths (λ x, x · _) (id_right _) @ !_). refine (maponpaths _ (id_right _) @ _). refine (assoc' _ _ _ @ _). refine (maponpaths (λ x, _ · x) (BinProductPr1Commutes _ _ _ _ _ _ _) @ _). exact (assoc _ _ _). - do 2 refine (maponpaths _ (BinProductOfArrowsPr2 _ _ _ _ _) @ !_). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (BinProductPr2Commutes _ _ _ _ _ _ _) @ _). refine (maponpaths (λ x, x · _) (functor_comp _ _ _) @ _). refine (maponpaths (λ x, x · _ · _) (preserves_binproduct_to_preserves_pr2 _ F_preserves_binproduct _ (C'_bin_products _ _)) @ _). refine (maponpaths (λ x, _ · x · _) (preserves_binproduct_to_preserves_pr1 _ F_preserves_binproduct _ (C'_bin_products _ _)) @ _). refine (maponpaths (λ x, x · _) (assoc _ _ _) @ !_). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ · x · _) (BinProductPr2Commutes _ _ _ _ _ _ _) @ _). do 2 refine (maponpaths (λ x, x · _) (assoc _ _ _) @ _). refine (assoc' _ _ _ @ _). refine (maponpaths _ (BinProductOfArrowsPr1 _ _ _ _ _) @ _). exact (assoc _ _ _). 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