proposition: Lemma colimAlgIsInitial_subproof (Aa : category_FunctorAlg F) (Fa' : algebra_mor F α_alg Aa) : Fa' = ad_mor Aa.
proof: Proof. apply algebra_mor_eq; simpl. apply colimArrowUnique; simpl; intro n. destruct Fa' as [f hf]; simpl. unfold is_algebra_mor in hf; simpl in hf. induction n as [|n IHn]; simpl. - now apply InitialArrowUnique. - rewrite <- IHn, functor_comp, <- assoc. eapply pathscomp0; [| eapply maponpaths; apply hf]. rewrite assoc. apply cancel_postcomposition, pathsinv0, (z_iso_inv_to_right _ _ _ _ α). rewrite unfold_inv_from_z_iso_α; apply pathsinv0. now eapply pathscomp0; [apply (colimArrowCommutes shiftColimCocone)|]. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Chains.Chains