prodFunctorToFunctorProdAssociator

English

The associator isomorphism is compatible with the product-to-functor product transformation, via a specified natural isomorphism.

Русский

Изоморфизм ассоциатора совместим с преобразованием prodFunctorToProdFunctor; существует соответствующее естественное изоморфическое отображение.

LaTeX

$$$\text{compatibility with }\text{prodFunctorToProdFunctor}$$$

Lean4

/-- The associator isomorphism is compatible with `prodFunctorToFunctorProd`. -/
@[simps!]
def prodFunctorToFunctorProdAssociator :
    (associativity _ _ _).functor ⋙
        ((𝟭 _).prod (prodFunctorToFunctorProd A D E) ⋙ (prodFunctorToFunctorProd A C (D × E))) ≅
      (prodFunctorToFunctorProd A C D).prod (𝟭 _) ⋙
        (prodFunctorToFunctorProd A (C × D) E) ⋙ (associativity C D E).congrRight.functor :=
  Iso.refl _

Похожие утверждения