Definition cia (X : algebra_ob F) : UU := ∏ (x : C) (e : x --> CP (F x) (alg_carrier _ X)), ∃! h : x --> alg_carrier _ X, cia_characteristic_formula X e h. Section cia_from_final_coalgebra. Context (X : coalgebra_ob F) (isTerminalX : isTerminal (CoAlg_category F) X). Local Definition Xinv : algebra_ob F. Proof. exists (coalg_carrier _ X). exact (inv_from_z_iso (finalcoalgebra_z_iso _ _ _ isTerminalX)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.FunctorCoalgebras.