proposition: Lemma parts_from_whole (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T) (h : `T • (U Z) --> `T) : bracket_property T f h → bracket_property_parts T f h.
proof: 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.
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