Lemma X_coproduct_νF_coalgebra_morphism_into_νF_aux : pr2 X_coproduct_νF_coalgebra -->[ BinCoproductArrow (CP x (pr1 νF)) h (identity (pr1 νF))] pr2 νF. Proof. cbn. etrans. 1: apply postcompWithBinCoproductArrow. etrans. 2: apply pathsinv0, postcompWithBinCoproductArrow. assert (p0 : ϕ · # F (BinCoproductArrow (CP x (pr1 νF)) h (identity (pr1 νF))) = h · pr2 νF). { unfold h. set (t := pr2 (TerminalArrow (νF,, isTerminalνF) X_coproduct_νF_coalgebra)). cbn in t. etrans. 2: apply assoc. etrans. 2: apply maponpaths, t. etrans. 2: apply assoc'. etrans. 2: apply maponpaths_2, pathsinv0, BinCoproductIn1Commutes. do 2 apply maponpaths. assert (p1 : identity (pr1 νF) = BinCoproductIn2 (CP x (pr1 νF)) · pr1 (TerminalArrow (νF,, isTerminalνF) X_coproduct_νF_coalgebra)). { etrans. 1: apply (base_paths _ _ (TerminalArrowUnique (νF,,isTerminalνF) νF (identity _))). transparent assert (f : ((CoAlg_category F)⟦νF,νF⟧)). { refine (_ · (TerminalArrow (νF,, isTerminalνF) X_coproduct_νF_coalgebra)). exists (BinCoproductIn2 (CP x (pr1 νF))). apply pathsinv0, BinCoproductIn2Commutes. } exact (! base_paths _ _ (TerminalArrowUnique (νF,,isTerminalνF) νF f)). } rewrite p1. apply pathsinv0, BinCoproductArrowEta. } rewrite p0. apply maponpaths. etrans. 1: apply assoc'. etrans. { apply maponpaths. etrans. 1: apply pathsinv0, functor_comp. apply maponpaths. apply BinCoproductIn2Commutes. } etrans. { apply maponpaths. apply functor_id. } exact (id_right _ @ ! id_left _). Qed.
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.