proposition: Lemma ad_is_coalgebra_mor (n : nat) : a · # F ad · inv_from_z_iso α · limOut CC n = an n.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCoalgebras UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Cochains