English
If f and g are equal via a 2-morphism η in the free bicategory, then their normalizations remain equal after applying normalizeAux along p.
Русский
Если f и g эквивалентны через 2-морфин η в свободной бикатегории, то их нормализации по p совпадают.
LaTeX
$$$normalizeAux(p, f) = normalizeAux(p, g)$ whenever there is a 2-morphism η : f \\rightarrow g$$
Lean4
/-- Given a 2-morphism between `f` and `g` in the free bicategory, we have the equality
`normalizeAux p f = normalizeAux p g`.
-/
theorem normalizeAux_congr {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
normalizeAux p f = normalizeAux p g := by
rcases η with ⟨η'⟩
apply @congr_fun _ _ fun p => normalizeAux p f
clear p η
induction η' with
| vcomp _ _ _ _ => apply Eq.trans <;> assumption
| whisker_left _ _ ih => funext; apply congr_fun ih
| whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
| _ => funext; rfl
