proposition: Lemma LNWFS_comon_structure_whiskercommutes (L L' Λ Λ' : total_category (LNWFS C)) (α : fact_mor (pr1 L) (pr1 L')) (β : fact_mor (pr1 Λ) (pr1 Λ')) (f : arrow C) : arrow_mor11 (lnwfs_mor (pr2 Λ) (pr2 Λ') β (lnwfs_L_monad (pr2 L) f)) · arrow_mor11 (#(lnwfs_L_monad (pr2 Λ')) (lnwfs_mor (pr2 L) (pr2 L') α f)) = arrow_mor11 (#(lnwfs_L_monad (pr2 Λ)) (lnwfs_mor (pr2 L) (pr2 L') α f)) · arrow_mor11 (lnwfs_mor (pr2 Λ) (pr2 Λ') β ((lnwfs_L_monad (pr2 L')) f)).
proof: Proof. set (βnat := nat_trans_ax β _ _ (lnwfs_mor (pr2 L) (pr2 L') α f)). set (βnat11 := base_paths _ _ (fiber_paths βnat)). etrans. exact (pathsinv0 βnat11). etrans. apply pr1_transportf_const. reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure