English
For A1,A2,A3 exponentiable, and f:A1⟶A2, g:A2⟶A3, we have pre (f ≫ g) = pre g ≫ pre f.
Русский
Для A1,A2,A3 экспоненцируемых и f:A1⟶A2, g:A2⟶A3 имеем pre (f ≫ g) = pre g ≫ pre f.
LaTeX
$$$ {A_1 A_2 A_3 : C} [Exponentiable A_1] [Exponentiable A_2] [Exponentiable A_3] (f : A_1 ⟶ A_2) (g : A_2 ⟶ A_3) :\n \operatorname{pre} (f \gg g) = \operatorname{pre} g \gg \operatorname{pre} f$$$
Lean4
theorem coev_expComparison (A B : C) :
F.map ((exp.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
(exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B)) :=
by
convert unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3
apply IsIso.inv_eq_of_hom_inv_id
simp