proposition: Lemma colimArrow_arrow_cocone_isColimCocone {d : chain C} {y : C} (ccy : cocone d y) : isColimCocone _ _ (colimArrow_arrow_cocone ccy).
proof: Proof. intros cl cc. assert (Hcin : ∏ v, identity y · arrow_mor11 (coconeIn cc 0) = arrow_mor11 (coconeIn cc v)). { abstract ( intro v; induction v as [|v Hv]; [apply id_left|]; etrans; [exact Hv|]; etrans; [exact (pathsinv0 (arrow_mor11_eq (coconeInCommutes cc _ _ (idpath (S v)))))|]; apply id_left ). } use unique_exists. - use mors_to_arrow_mor. * exact (colimArrow (CC _ _) _ (project_arrow_cocone00 cc)). * exact (colimArrow (cocone_arrow_chain_y_ColimCocone ccy) _ (project_arrow_cocone11 cc)). * abstract ( use colimArrowUnique'; intro v; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply colimArrowCommutes|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply colimArrowCommutes|]; etrans; [|exact (pathsinv0 (arrow_mor_comm (coconeIn cc v)))]; apply cancel_precomposition; induction v as [|v Hv]; [reflexivity|]; etrans; [exact Hv|]; etrans; [exact (pathsinv0 (arrow_mor11_eq (coconeInCommutes cc _ _ (idpath (S v)))))|]; apply id_left ). - abstract ( intro v; use arrow_mor_eq; [apply colimArrowCommutes|]; exact (Hcin v) ). - abstract (intro x; apply impred; intro; apply homset_property). - abstract ( intros x ccx; use arrow_mor_eq; [ use colimArrowUnique; intro v; exact (arrow_mor00_eq (ccx v))| ]; use (colimArrowUnique' (cocone_arrow_chain_y_ColimCocone ccy)); intro v; etrans; [exact (arrow_mor11_eq (ccx v))|]; apply pathsinv0; exact (Hcin v) ). Defined.
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.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.LNWFSHelpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure UniMath.ModelCategories.Generated.LNWFSMonoidalStructure UniMath.ModelCategories.Generated.LNWFSCocomplete