English
There is an isomorphism of corepresentable-by structures corresponding to the associator for Day convolution; the two ways of regrouping F, G, H are canonically isomorphic via a natural isomorphism.
Русский
Существует изоморфизм структур corepresentable-by, соответствующий ассоциатору Day-конволюции; два способа группировки F, G, H канонически изоморфны через естественный изоморфизм.
LaTeX
$$$\\cong: ((F ⊠ G) ⊗ H) \\cong (F ⊠ G ⊠ H)$ via associatorCorepresentingIso$$
Lean4
/-- The `CorepresentableBy` structure asserting that the Type-valued functor
`Y ↦ (F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ Y)` is corepresented by
`F ⊛ G ⊛ H`. -/
@[simps]
def corepresentableBy₂ :
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ coyoneda.obj (.op <| F ⊠ G ⊠ H) |>.CorepresentableBy
(F ⊛ G ⊛ H)
where
homEquiv :=
(corepresentableBy F (G ⊛ H)).homEquiv.trans <|
Functor.homEquivOfIsLeftKanExtension _ (extensionUnitRight (G ⊛ H) (unit G H) F) _
homEquiv_comp := by aesop
