English
The left associativity relation for actLeft and μ on P, Q is given by a specific equality involving α and associativity constraints.
Русский
Левая ассоциативность для actLeft и μ на P, Q задаётся равенством с участием α и ассоциаторов.
LaTeX
$$$(\mu \; ⊵ _ ) \; ≫ \mathrm{actLeft} \; P \; Q = (\alpha_{R.X R.X _}).\mathrm{hom} \; ≫ (R.X \; ◁ \; \mathrm{actLeft} P Q) \; ≫ \mathrm{actLeft} P Q$$$
Lean4
theorem one_act_left' : (η ▷ _) ≫ actLeft P Q = (λ_ _).hom :=
by
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp [X]
slice_lhs 1 2 => rw [whisker_exchange]
slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
slice_lhs 1 2 => rw [associator_inv_naturality_left]
slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]
slice_rhs 1 2 => rw [leftUnitor_naturality]
monoidal
