proposition: 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: 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.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total