English
For a pseudofunctor F and arrows f,g,fg with hfg : f ≫ g = fg, the inverse component of mapComp' interacts with the map on a via naturality: (F.map g).map ((F.map f).map a) ≫ (F.mapComp' f g fg hfg).inv.app Y = (F.map fg).map a ≫ (F.mapComp' f g fg hfg).inv.app X.
Русский
Пусть F — псевдофунктор и стрелки f,g,fg с hfg : f ≫ g = fg. Тогда обратная компонента mapComp' взаимодействует с отображением на a по естественности: (F.map g).map ((F.map f).map a) ≫ (F.mapComp' f g fg hfg).inv.app Y = (F.map fg).map a ≫ (F.mapComp' f g fg hfg).inv.app X.
LaTeX
$$$ (F.map g).map ((F.map f).map a) ≫ (F.mapComp' f g fg hfg).inv.app Y = (F.map fg).map a ≫ (F.mapComp' f g fg hfg).inv.app X $$$
Lean4
@[reassoc]
theorem mapComp'_inv_naturality :
(F.map g).map ((F.map f).map a) ≫ (F.mapComp' f g fg hfg).inv.app Y =
(F.mapComp' f g fg hfg).inv.app X ≫ (F.map fg).map a :=
(F.mapComp' f g fg hfg).inv.naturality a
