English
The inverse of the backward direction of the functor equivalence, whiskered on the left with inr, is naturally isomorphic to the second projection.
Русский
Обратная сторона направления эквивалентности функторов через правый инъектор вместе с whiskerLeftInr естественным образом изоморфна второй проекции.
LaTeX
$$((\mathrm{functorEquiv} A A' B).inverse.comp ((\mathrm{whiskeringLeft} A' (Sum A A') B).obj (Sum.inr A A'))) ≅ \mathrm{Prod.snd}(A ⥤ B)(A' ⥤ B)$$
Lean4
/-- `functorEquiv A A' B` transforms `Swap.equivalence` into `Prod.braiding`. -/
@[simps! hom_app_fst hom_app_snd inv_app_fst inv_app_snd]
def equivalenceFunctorEquivFunctorIso :
((equivalence A A').congrLeft.trans <| functorEquiv A' A B).functor ≅
((functorEquiv A A' B).trans <| Prod.braiding (A ⥤ B) (A' ⥤ B)).functor :=
NatIso.ofComponents
(fun E ↦
Iso.prod ((Functor.associator _ _ E).symm ≪≫ isoWhiskerRight (Sum.swapCompInl A' A) _)
((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (Sum.swapCompInr A' A) _))
