Lemma whole_from_parts (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T) (h : `T • (U Z) --> `T) : bracket_property_parts T f h → bracket_property T f h. Proof. intros [Hyp1 Hyp2]. apply nat_trans_eq_alt. intro c. apply BinCoproductArrow_eq_cor. + clear Hyp2. assert (Hyp1_inst := nat_trans_eq_pointwise Hyp1 c); clear Hyp1. rewrite <- assoc. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite id_left. apply BinCoproductIn1Commutes_right_dir. simpl. simpl in Hyp1_inst. rewrite Hyp1_inst. simpl. apply assoc. + clear Hyp1. assert (Hyp2_inst := nat_trans_eq_pointwise Hyp2 c); clear Hyp2. rewrite <- assoc. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite assoc. eapply pathscomp0. * eapply pathsinv0. exact Hyp2_inst. * clear Hyp2_inst. simpl. do 2 rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_right_dir. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation.