Documentation

Mathlib.CategoryTheory.Products.Associator

The associator functor ((C × D) × E) ⥤ (C × (D × E)) and its inverse form an equivalence.

@[simp]
theorem CategoryTheory.prod.associator_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :
∀ (x x_1 : (C × D) × E) (f : x x_1), (CategoryTheory.prod.associator C D E).map f = (f.1.1, f.1.2, f.2)

The associator functor (C × D) × E ⥤ C × (D × E).

Equations
Instances For
    @[simp]

    The inverse associator functor C × (D × E) ⥤ (C × D) × E .

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The equivalence of categories expressing associativity of products of categories.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For