proposition: Lemma LNWFS_colim_comul_monad_ax : disp_Comonad_laws (L_monad_data (colim Finf) LNWFS_colim_comul).
proof: Proof. repeat split; intro f. - apply arrow_mor_eq; [etrans; [apply assoc'|]; etrans; [apply id_left|]; apply id_left|]. apply pathsinv0. apply colim_endo_is_identity. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. apply (colimOfArrowsIn). etrans. apply assoc4. etrans. apply cancel_postcomposition, cancel_precomposition. apply (colimOfArrowsIn). etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes). set (law1v := @Comonad_law1 _ (L_monad _ _ (pr22 (dob d v))) f). etrans. apply assoc'. etrans. apply cancel_precomposition. exact (LNWFS_colim_comul_data_subproof1 f v). etrans. apply assoc. etrans. apply cancel_postcomposition. exact (pr2 (pathsdirprodweq (base_paths _ _ law1v))). apply id_left. - apply arrow_mor_eq; [etrans; [apply assoc'|]; etrans; [apply id_left|]; apply id_left|]. apply pathsinv0. apply colim_endo_is_identity. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. apply (colimOfArrowsIn). etrans. apply assoc4. etrans. apply cancel_postcomposition, cancel_precomposition. { set (ccmor := (CC g (mapdiagram (PrecategoryBinProduct.pr2_functor C C) (mapdiagram (pr1_category (arrow_disp C)) (LNWFS_diagram_pointwise_comul_mor f))))). apply (colimOfArrowsIn _ _ ccmor). } etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_precomposition. { set (ccmor := (CCFf_pt_ob1 CC dbase (make_dirprod (three_ob0 (f,, ColimFf_ob CC dbase v0 f)) (colim (CCFf_pt_ob1 CC dbase f)),, pr12 ((pr11 (dob d v0)) f) · colimIn (CCFf_pt_ob1 CC dbase f) v0))). apply (colimOfArrowsIn _ _ ccmor). } etrans. apply assoc. apply pathsinv0. etrans. apply (pathsinv0 (id_left _)). apply cancel_postcomposition. set (law2v := @Comonad_law2 _ (L_monad _ _ (pr22 (dob d v))) f). etrans. exact (pathsinv0 (pr2 (pathsdirprodweq (base_paths _ _ law2v)))). apply pathsinv0. etrans. apply assoc'. apply cancel_precomposition. etrans. apply pr1_section_disp_on_morphisms_comp. apply section_disp_on_eq_morphisms; [apply id_left|]. apply (colimArrowCommutes (CCFf_pt_ob1 CC dbase f)). - apply arrow_mor_eq; [reflexivity|]. use colimArrowUnique'. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. apply (colimOfArrowsIn _ _ (CCFf_pt_ob1 CC dbase f)). etrans. apply assoc'. etrans. apply assoc'. etrans. apply cancel_precomposition. { etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimOfArrowsIn). etrans. apply assoc'. apply cancel_precomposition. set (ccinf := CCFf_pt_ob1 CC dbase (fact_L (colim Finf) f)). apply (colimArrowCommutes ccinf). } apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. apply (colimOfArrowsIn _ _ (CCFf_pt_ob1 CC dbase f)). etrans. apply assoc'. etrans. apply assoc'. etrans. apply cancel_precomposition. { etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimOfArrowsIn). etrans. apply assoc'. apply cancel_precomposition. set (ccinf := CCFf_pt_ob1 CC dbase (fact_L (colim Finf) f)). etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes ccinf). etrans. apply assoc'. apply cancel_precomposition. apply (colimOfArrowsIn). } etrans. apply assoc. etrans. apply assoc. etrans. apply assoc. apply pathsinv0. etrans. apply assoc. etrans. apply assoc. apply cancel_postcomposition. exact (LNWFS_colim_comul_monad_ax_subproof f v). 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.FunctorCategory 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.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure