Lemma heterogeneous_substitution_into_bracket {Z : Ptd} (f : Z --> ptd_from_alg T0) : bracket_property H (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T0 (#U f) ((` T0 ∘ #U f : EndC ⟦ `T0 • U Z , `T0 • U (ptd_from_alg T0) ⟧) · prejoin_from_hetsubst T0). Proof. apply whole_from_parts. split. - apply nat_trans_eq_alt. intro c. induction f as [f pt]. simpl. assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)). etrans. 2: { rewrite <- assoc. apply maponpaths. rewrite assoc. apply cancel_postcomposition. exact alg_map_nat. } clear alg_map_nat. etrans. 2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn1Commutes. } simpl. etrans. { apply pathsinv0. apply id_right. } do 2 rewrite <- assoc. apply maponpaths. rewrite assoc. assert (prejoin_ok := prejoin_from_hetsubst_η T0). apply (maponpaths pr1) in prejoin_ok. apply toforallpaths in prejoin_ok. apply prejoin_ok. - rewrite functor_comp. apply nat_trans_eq_alt. intro c. induction f as [f pt]. simpl. assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)). etrans. 2: { rewrite <- assoc. apply maponpaths. rewrite assoc. apply cancel_postcomposition. exact alg_map_nat. } etrans. 2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn2Commutes. } assert (prejoin_ok := prejoin_from_hetsubst_τ T0). apply (maponpaths pr1) in prejoin_ok. apply toforallpaths in prejoin_ok. assert (prejoin_ok_inst := prejoin_ok c). simpl in prejoin_ok_inst. etrans. { repeat rewrite assoc. do 3 apply cancel_postcomposition. apply pathsinv0. assert (theta_nat_2 := θ_nat_2_pointwise _ _ _ H θ `T0 _ _ (f,,pt) c). rewrite horcomp_id_postwhisker in theta_nat_2; try apply homset_property. apply theta_nat_2. } etrans. { repeat rewrite <- assoc. apply maponpaths. rewrite assoc. exact prejoin_ok_inst. } clear prejoin_ok prejoin_ok_inst. repeat 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.