Lemma ad_is_algebra_mor : is_algebra_mor _ α_alg Aa ad. Proof. apply pathsinv0, z_iso_inv_to_left, colimArrowUnique; simpl; intro n. destruct n as [|n]. - now apply InitialArrowUnique. - rewrite assoc, unfold_inv_from_z_iso_α. eapply pathscomp0; [apply cancel_postcomposition, (colimArrowCommutes shiftColimCocone)|]. simpl; rewrite assoc, <- functor_comp. apply cancel_postcomposition, maponpaths, (colimArrowCommutes CC). 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.