Definition cia_characteristic_formula (X : algebra_ob F) {x : C} (e : x --> CP (F x) (alg_carrier _ X)) (h : x --> alg_carrier _ X) : UU := h = e · BinCoproductOfArrows _ (CP _ _) (CP _ _) (#F h) (identity _) · (BinCoproductArrow (CP _ _) (alg_map _ X) (identity _)).
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.