proposition: Lemma functor_to_morphism_preserves_one : preserves_one functor_to_algebraic_theory_morphism.
proof: Proof. refine (maponpaths (λ x, _ (_ (x · _) · _)) (φ_adj_after_φ_adj_inv _ _) @ _). refine (maponpaths (λ x, _ (_ x · _)) (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ (x · _)) (φ_adj_natural_postcomp _ _ _ _ _ _) @ _). refine (maponpaths _ (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ · x · _) (functor_comp _ _ _) @ _). refine (maponpaths (λ x, _ · (x · _) · _) F_preserves_φ_adj @ _). refine (assoc' _ _ _ @ !_). refine (maponpaths (λ x, _ (x · _) · _) (φ_adj_after_φ_adj_inv _ _) @ _). refine (maponpaths (λ x, _ x · _) (assoc' _ _ _) @ _). refine (maponpaths (λ x, x · _) (φ_adj_natural_postcomp _ _ _ _ _ _) @ !_). apply z_iso_inv_on_right. do 3 refine (assoc' _ _ _ @ _). apply (maponpaths (λ x, _ · x)). refine (_ @ assoc _ _ _). apply (maponpaths (λ x, φ_adj (pr2 E') (pr (T := L') (● 0 : stn 1)%stn) · x)). apply z_iso_inv_on_right. refine (_ @ assoc' _ _ _). apply z_iso_inv_to_right. apply F_preserves_app_abs_abs. 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