English
The 2-isomorphism normalizeIso p f is natural in f; whiskering before/after interacts compatibly with preinclusion and normalization.
Русский
2-изоморфизм normalizeIso p f естествен по отношению к f; сочетания whisker и normalization согласованы.
LaTeX
$$The naturality condition: (preinclusion B).map ⟨p⟩ ◁ η ≫ (normalizeIso p g).hom = (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom (Discrete.ext (normalizeAux_congr p η)))$$
Lean4
/-- The 2-isomorphism `normalizeIso p f` is natural in `f`. -/
theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
(preinclusion B).map ⟨p⟩ ◁ η ≫ (normalizeIso p g).hom =
(normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom (Discrete.ext (normalizeAux_congr p η))) :=
by
rcases η with ⟨η'⟩; clear η
induction η' with
| id => simp
| vcomp η θ ihf ihg =>
simp only [mk_vcomp, whiskerLeft_comp]
slice_lhs 2 3 => rw [ihg]
slice_lhs 1 2 => rw [ihf]
simp
-- p ≠ nil required! See the docstring of `normalizeAux`.
| whisker_left _ _ ih =>
dsimp
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
simp
| whisker_right h η' ih =>
dsimp
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
dsimp at this; simp [this]
| _ =>
simp
-- Not `@[simp]` because it is not in `simp`-normal form.
