English
Compatibility of the natural equivalence with precomposition by a morphism in the base category; the equality of two ways of transporting along arrows holds.
Русский
Совместимость естественного эквивалента с предокомпозицией по морфизму в базовой категории; равенство двух путей переноса вдоль стрелок сохраняется.
LaTeX
$$Equality that expresses naturality of functorEnrichedHomCoyonedaObjEquiv with precomposition$$
Lean4
theorem whiskerLeft {G₁ G₂ : Cᵒᵖ ⥤ A} {g : G₁ ⟶ G₂} (hg : J.W g) (F : Cᵒᵖ ⥤ A) : J.W (F ◁ g) := fun H h ↦
by
have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)
rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry) ((ihom.adjunction _).homEquiv _ _).bijective]
rw [←
Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _ ((ihom.adjunction _).homEquiv _ _).bijective] at this
convert this using 1
ext α : 1
dsimp
rw [curry_natural_left]
