# 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_obj (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] (X : (C × D) × E) :
().obj X = (X.1.1, X.1.2, X.2)
@[simp]
theorem CategoryTheory.prod.associator_map (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
∀ (x x_1 : (C × D) × E) (f : x x_1), ().map f = (f.1.1, f.1.2, f.2)
def CategoryTheory.prod.associator (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
CategoryTheory.Functor ((C × D) × E) (C × D × E)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.prod.inverseAssociator_map (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
∀ (x x_1 : C × D × E) (f : x x_1), .map f = ((f.1, f.2.1), f.2.2)
@[simp]
theorem CategoryTheory.prod.inverseAssociator_obj (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] (X : C × D × E) :
.obj X = ((X.1, X.2.1), X.2.2)
def CategoryTheory.prod.inverseAssociator (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
CategoryTheory.Functor (C × D × E) ((C × D) × E)

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
def CategoryTheory.prod.associativity (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
(C × D) × E C × D × E

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
instance CategoryTheory.prod.associatorIsEquivalence (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
().IsEquivalence
Equations
• =
instance CategoryTheory.prod.inverseAssociatorIsEquivalence (C : Type u₁) [] (D : Type u₂) [] (E : Type u₃) [] :
.IsEquivalence
Equations
• =