English
Let F be a functor Cᵒᵖ ⥤ Dᵒᵖ. Then the unop of the right unitor of F equals a certain composite built from F.unop and whiskering on the left, i.e. NatIso.unop F.rightUnitor = F.unop.rightUnitor.symm ≪≫ isoWhiskerLeft F.unop (Functor.unopId D).symm ≪≫ (Functor.unopComp _ _).symm.
Русский
Пусть F — функтор из Cᵒᵖ в Dᵒᵖ. Тогда обратный правого уколера F равен композиции, включающей F.unop и ослабляющие перемножения слева, то есть NatIso.unop F.rightUnitor = F.unop.rightUnitor.symm ≪≫ isoWhiskerLeft F.unop (Functor.unopId D).symm ≪≫ (Functor.unopComp _ _).symm.
LaTeX
$$$\mathrm{NatIso.unop} F.rightUnitor = F.unop.rightUnitor.symm \llcorner\!\!\!\circ \mathrm{isoWhiskerLeft} F.unop (\mathrm{Functor.unopId} D).symm \llcorner\!\!\!\circ (\mathrm{Functor.unopComp} _ _).symm$$$
Lean4
theorem unop_rightUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} :
NatIso.unop F.rightUnitor =
F.unop.rightUnitor.symm ≪≫ isoWhiskerLeft F.unop (Functor.unopId D).symm ≪≫ (Functor.unopComp _ _).symm :=
by cat_disch
