Definition X_coproduct_νF_coalgebra_morphism_into_νF : (CoAlg_category F ⟦ X_coproduct_νF_coalgebra, νF⟧). Proof. exists (BinCoproductArrow (CP x (pr1 νF)) h (identity (pr1 νF))). exact X_coproduct_νF_coalgebra_morphism_into_νF_aux. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.