The left/right unitor equivalences 1 × C ≌ C and C × 1 ≌ C.

@[simp]

theorem CategoryTheory.prod.leftUnitor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Discrete PUnit.{w + 1} × C) : (CategoryTheory.prod.leftUnitor C).obj X = X.2

@[simp]

theorem CategoryTheory.prod.leftUnitor_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Discrete PUnit.{w + 1} × C} (f : X ⟶ Y), (CategoryTheory.prod.leftUnitor C).map f = f.2

def CategoryTheory.prod.leftUnitor (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} × C) C

The left unitor functor 1 × C ⥤ C

Equations

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

@[simp]

theorem CategoryTheory.prod.rightUnitor_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : C × CategoryTheory.Discrete PUnit.{w + 1} } (f : X ⟶ Y), (CategoryTheory.prod.rightUnitor C).map f = f.1

@[simp]

theorem CategoryTheory.prod.rightUnitor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C × CategoryTheory.Discrete PUnit.{w + 1} ) : (CategoryTheory.prod.rightUnitor C).obj X = X.1

def CategoryTheory.prod.rightUnitor (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (C × CategoryTheory.Discrete PUnit.{w + 1} ) C

The right unitor functor C × 1 ⥤ C

Equations

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

@[simp]

theorem CategoryTheory.prod.leftInverseUnitor_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.prod.leftInverseUnitor C).map f = (CategoryTheory.CategoryStruct.id ((fun (X : C) => ({ as := PUnit.unit }, X)) X).1, f)

@[simp]

theorem CategoryTheory.prod.leftInverseUnitor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)

def CategoryTheory.prod.leftInverseUnitor (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} × C)

The left inverse unitor C ⥤ 1 × C

Equations

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

@[simp]

theorem CategoryTheory.prod.rightInverseUnitor_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.prod.rightInverseUnitor C).map f = (f, CategoryTheory.CategoryStruct.id ((fun (X : C) => (X, { as := PUnit.unit })) X).2)

@[simp]

theorem CategoryTheory.prod.rightInverseUnitor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })

def CategoryTheory.prod.rightInverseUnitor (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (C × CategoryTheory.Discrete PUnit.{w + 1} )

The right inverse unitor C ⥤ C × 1

Equations

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

@[simp]

theorem CategoryTheory.prod.leftUnitorEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).functor = CategoryTheory.prod.leftUnitor C

@[simp]

theorem CategoryTheory.prod.leftUnitorEquivalence_counitIso (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.prod.leftInverseUnitor C).comp (CategoryTheory.prod.leftUnitor C))

@[simp]

theorem CategoryTheory.prod.leftUnitorEquivalence_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).inverse = CategoryTheory.prod.leftInverseUnitor C

@[simp]

theorem CategoryTheory.prod.leftUnitorEquivalence_unitIso (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Discrete PUnit.{w + 1} × C))

def CategoryTheory.prod.leftUnitorEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Discrete PUnit.{w + 1} × C ≌ C

The equivalence of categories expressing left unity of products of categories.

Equations

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

@[simp]

theorem CategoryTheory.prod.rightUnitorEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).functor = CategoryTheory.prod.rightUnitor C

@[simp]

theorem CategoryTheory.prod.rightUnitorEquivalence_counitIso (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.prod.rightInverseUnitor C).comp (CategoryTheory.prod.rightUnitor C))

@[simp]

theorem CategoryTheory.prod.rightUnitorEquivalence_unitIso (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × CategoryTheory.Discrete PUnit.{w + 1} ))

@[simp]

theorem CategoryTheory.prod.rightUnitorEquivalence_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).inverse = CategoryTheory.prod.rightInverseUnitor C

def CategoryTheory.prod.rightUnitorEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] : C × CategoryTheory.Discrete PUnit.{w + 1} ≌ C

The equivalence of categories expressing right unity of products of categories.

Equations

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

instance CategoryTheory.prod.leftUnitor_isEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitor C).IsEquivalence

Equations

• ⋯ = ⋯

instance CategoryTheory.prod.rightUnitor_isEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitor C).IsEquivalence

Equations

• ⋯ = ⋯