Lemma ad_is_coalgebra_mor (n : nat) : a · # F ad · inv_from_z_iso α · limOut CC n = an n. Proof. destruct n as [|n]. - now apply TerminalArrowUnique. - rewrite unfold_inv_from_z_iso_α. eapply pathscomp0. { rewrite assoc'. apply maponpaths. apply (limArrowCommutes shiftLimCone). } simpl; rewrite assoc', <- functor_comp. apply cancel_precomposition, maponpaths, (limArrowCommutes 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.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.