Lemma colimAlgIsInitial_subproof (Aa : category_FunctorAlg F) (Fa' : algebra_mor F α_alg Aa) : Fa' = ad_mor Aa. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Chains.Chains.