proposition: Lemma limCoAlgIsTerminal_subproof (Aa : CoAlg_category F) (Fa' : coalgebra_mor F Aa α_alg) : Fa' = ad_mor Aa.
proof: 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.
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