English
There is a canonical 2-isomorphism between a partially normalized 1-morphism and its fully normalized form in the free bicategory constructed from a quiver B.
Русский
Существует каноническое 2-изоморфизм между частично нормализованной и полностью нормализованной формой 1-морфизма в свободной би kategorии, построенной над кворьем B.
LaTeX
$$$\\text{ normalizeIso } : (p : Path a b) \\to \\left( f : FreeBicategory.Hom b c \\right) \\to (preinclusion B).map⟨p⟩ ≅ (preinclusion B).map⟨\\text{normalizeAux } p f\\rangle$$$
Lean4
/-- A 2-isomorphism between a partially-normalized 1-morphism in the free bicategory to the
fully-normalized 1-morphism.
-/
@[simp]
def normalizeIso {a : B} :
∀ {b c : B} (p : Path a b) (f : Hom b c), (preinclusion B).map ⟨p⟩ ≫ f ≅ (preinclusion B).map ⟨normalizeAux p f⟩
| _, _, _, Hom.of _ => Iso.refl _
| _, _, _, Hom.id b => ρ_ _
| _, _, p, Hom.comp f g =>
(α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIso p f) g ≪≫ normalizeIso (normalizeAux p f) g
