proposition: Lemma coslice_to_is_algebra_morphism {A B : algebra (free_theory S)} (F : coslice_cat SET S ⟦ coslice_functor A, coslice_functor B ⟧) : ∏ n f a, mor_action_ax (identity _) (coslice_to_algebra_morphism_data F) (@action _ A) (@action _ B) n f a.
proof: Proof. intros n f a. induction f as [i | s]. - refine (maponpaths _ (pr_action _ _ _) @ !_). exact (pr_action _ _ _). - refine (maponpaths _ (comp_action A (inr s) (weqvecfun _ [()]) a) @ !_). refine (comp_action B (inr s) (weqvecfun _ [()]) (λ i, coslicecat_mor_morphism _ _ F (a i)) @ !_). refine (_ @ eqtohomot (coslicecat_mor_comm _ _ F) s @ _). + apply (maponpaths (coslicecat_mor_morphism _ _ F)). apply (maponpaths (action _)). apply funextfun. intro i. apply (fromstn0 i). + apply (maponpaths (action _)). apply funextfun. intro i. apply (fromstn0 i). 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.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraCategory UniMath.AlgebraicTheories.AlgebraCategoryCore UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.Algebras