English
Let F be a functor from Cᵒᵖ to Dᵒᵖ. Then the unop of the left unitor of F equals a composite built from the unop of F and various whiskered isomorphisms, i.e. NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ isoWhiskerRight (Functor.unopId C).symm F.unop ≪≫ (Functor.unopComp _ _).symm.
Русский
Пусть F — функтор из Cᵒᵖ в Dᵒᵖ. Тогда обратный относительно операции противоположности левого уколера F равен композиции из обратного левого уколера F.unop и различных усечённых изоморфизмов, то есть NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ isoWhiskerRight (Functor.unopId C).symm F.unop ≪≫ (Functor.unopComp _ _).symm.
LaTeX
$$$\mathrm{NatIso.unop} F.leftUnitor = F.unop.leftUnitor^{-1} \circ \mathrm{isoWhiskerRight}(\mathrm{Functor.unopId} C)^{-1} \circ F.unop \circ (\mathrm{Functor.unopComp} \_ \_)^{-1}$$$
Lean4
theorem unop_leftUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} :
NatIso.unop F.leftUnitor =
F.unop.leftUnitor.symm ≪≫ isoWhiskerRight (Functor.unopId C).symm F.unop ≪≫ (Functor.unopComp _ _).symm :=
by cat_disch
