@[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.associator_obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(X : (C × D) × E) :
def
category_theory.prod.associator
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
The associator functor (C × D) × E ⥤ C × (D × E).
@[simp]
theorem
category_theory.prod.inverse_associator_obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(X : C × D × E) :
@[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) :
def
category_theory.prod.inverse_associator
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
The inverse associator functor C × (D × E) ⥤ (C × D) × E.
def
category_theory.prod.associativity
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
The equivalence of categories expressing associativity of products of categories.
Equations
- category_theory.prod.associativity C D E = category_theory.equivalence.mk (category_theory.prod.associator C D E) (category_theory.prod.inverse_associator C D E) (category_theory.nat_iso.of_components (λ (X : (C × D) × E), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : C × D × E), category_theory.eq_to_iso _) _)
@[instance]
def
category_theory.prod.associator_is_equivalence
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
@[instance]
def
category_theory.prod.inverse_associator_is_equivalence
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :