Lemma limCoAlgIsTerminal_subproof (Aa : CoAlg_category F) (Fa' : coalgebra_mor F Aa α_alg) : Fa' = ad_mor Aa. Proof. use total2_paths_f. 2: { apply homset_property. } apply limArrowUnique ; intro n. destruct Fa' as [f hf]; simpl. unfold is_coalgebra_mor in hf; simpl in hf. induction n as [|n IHn]; simpl. - apply TerminalArrowUnique. - rewrite <- IHn, functor_comp, assoc. etrans. 2: { apply cancel_postcomposition ; apply (! hf). } rewrite assoc'. apply maponpaths. apply (z_iso_inv_to_left _ _ _ α). apply (limArrowCommutes shiftLimCone). 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.