Lemma parts_from_whole (T : algebra_ob Id_H) (f : U Z --> `T) (h : `T • (U Z) --> `T) : bracket_property T f h → bracket_property_parts T f h. Proof. intro Hyp. split. + unfold eta_from_alg. apply nat_trans_eq_alt. intro c. simpl. unfold coproduct_nat_trans_in1_data. assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp. apply (maponpaths (λ m, BinCoproductIn1 (CP _ _)· m)) in Hyp_inst. match goal with |[ H1 : _ = ?f |- _ = _ ] => intermediate_path (f) end. * clear Hyp_inst. rewrite <- assoc. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite id_left. apply BinCoproductIn1Commutes_right_in_ctx_dir. rewrite id_left. apply BinCoproductIn1Commutes_right_dir. apply idpath. * rewrite <- Hyp_inst; clear Hyp_inst. rewrite <- assoc. apply idpath. + unfold tau_from_alg. apply nat_trans_eq_alt. intro c. simpl. unfold coproduct_nat_trans_in2_data. assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp. apply (maponpaths (λ m, BinCoproductIn2 (CP _ _)· m)) in Hyp_inst. match goal with |[ H1 : _ = ?f |- _ = _ ] => intermediate_path (f) end. * clear Hyp_inst. do 2 rewrite <- assoc. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite <- assoc. apply maponpaths. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite <- assoc. apply maponpaths. unfold tau_from_alg. apply BinCoproductIn2Commutes_right_dir. apply idpath. * rewrite <- Hyp_inst; clear Hyp_inst. rewrite <- assoc. 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.