mathlib3 documentation

category_theory.products.associator

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations
Instances for category_theory.prod.associator
@[simp]
theorem category_theory.prod.associator_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (_x _x_1 : (C × D) × E) (f : _x _x_1) :
@[simp]
theorem category_theory.prod.inverse_associator_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (_x _x_1 : C × D × E) (f : _x _x_1) :

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

Equations
Instances for category_theory.prod.inverse_associator