proposition: Lemma lnwfs_mor_comp {F F' F'' : Ff C} {n : lnwfs_over F} {n' : lnwfs_over F'} {n'' : lnwfs_over F''} {τ : F --> F'} {τ' : F' --> F''} (ax : lnwfs_mor_axioms n n' τ) (ax' : lnwfs_mor_axioms n' n'' τ') : lnwfs_mor_axioms n n'' (τ · τ').
proof: Proof. assert (lnwfs_mor n n'' (τ · τ') = nat_trans_comp _ _ _ (lnwfs_L_monad_mor τ ax) (lnwfs_L_monad_mor τ' ax')) as H. { use nat_trans_eq. - exact (homset_property (arrow C)). - intro x. use arrow_mor_eq. * apply pathsinv0. apply id_left. * etrans. use pr1_transportf_const. reflexivity. } unfold lnwfs_mor_axioms. rewrite H. exact ( comonads_category_comp_subproof (lnwfs_L_monad_data n) (pr22 (lnwfs_L_monad n)) (lnwfs_L_monad_data n') (pr22 (lnwfs_L_monad n')) (lnwfs_L_monad_data n'') (pr22 (lnwfs_L_monad n'')) (lnwfs_L_monad_mor τ ax) (lnwfs_L_monad_mor τ' ax') ax ax' ). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.CategoryTheory.DisplayedCats.Examples.MonadAlgebras UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.Helpers