proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation