Lemma isConeOverCoalg {u v : nat} (e : S v = u) : an u · dmor Fcochain e = an v. Proof. destruct e. induction v as [| n IHn]. - apply TerminalArrowUnique. - simpl ; rewrite assoc' ; apply cancel_precomposition. etrans. 2: { apply maponpaths ; exact IHn. } rewrite functor_comp. simpl. do 2 rewrite functor_comp. apply maponpaths. unfold dmor. cbn. rewrite ! id_left. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Cochains.