English
For every η : f ≅ g, the composite F.map₂ η.inv ≫ F.map₂ η.hom equals the identity on F.map f.
Русский
Для η : f ≅ g выполняется F.map₂ η.inv ≫ F.map₂ η.hom = id_{F.map f}.
LaTeX
$$$F.map₂ \eta.inv ≫ F.map₂ \eta.hom = 𝟙 (F.map f)$$$
Lean4
/-- Composition of lax functors. -/
@[simps]
def comp {D : Type u₃} [Bicategory.{w₃, v₃} D] (F : LaxFunctor B C) (G : LaxFunctor C D) : LaxFunctor B D
where
toPrelaxFunctor := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
mapId := fun a => G.mapId (F.obj a) ≫ G.map₂ (F.mapId a)
mapComp := fun f g => G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)
mapComp_naturality_left := fun η g => by
dsimp
rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, mapComp_naturality_left_assoc]
mapComp_naturality_right := fun f _ _ η => by
dsimp
rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_assoc]
map₂_associator := fun f g h => by
dsimp
slice_rhs 1 3 => rw [Bicategory.whiskerLeft_comp, assoc, ← mapComp_naturality_right, ← map₂_associator_assoc]
slice_rhs 3 5 => rw [← G.map₂_comp, ← G.map₂_comp, ← F.map₂_associator, G.map₂_comp, G.map₂_comp]
slice_lhs 1 3 => rw [comp_whiskerRight, assoc, ← G.mapComp_naturality_left_assoc]
simp only [assoc]
map₂_leftUnitor := fun f => by
dsimp
simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, assoc, mapComp_naturality_left_assoc, comp_whiskerRight]
map₂_rightUnitor := fun f => by
dsimp
simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, assoc, mapComp_naturality_right_assoc,
Bicategory.whiskerLeft_comp]
