Lemma isCoconeOverAlg n Sn (e : edge n Sn) : dmor Fchain e · an Sn = an n. Proof. destruct e. induction n as [|n IHn]. - now apply InitialArrowUnique. - simpl; rewrite assoc. apply cancel_postcomposition, pathsinv0. eapply pathscomp0; [|simpl; apply functor_comp]. now apply maponpaths, pathsinv0, IHn. 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.