The homotopy category functor is monoidal

Given 2-truncated simplicial sets X and Y, we introduce ad operation Truncated.Edge.tensor : Edge x x' → Edge y y' → Edge (x, y) (x', y'). We use this in order to construct an equivalence of categories (X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory.

def SSet.Truncated.Edge.tensor {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : Edge (x, y) (x', y')

The external product of edges of 2-truncated simplicial sets.

@[simp]

theorem SSet.Truncated.Edge.tensor_edge {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).edge = (e₁.edge, e₂.edge)

theorem SSet.Truncated.Edge.tensor_surjective {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e : Edge (x, y) (x', y')) : ∃ (e₁ : Edge x x') (e₂ : Edge y y'), e₁.tensor e₂ = e

@[simp]

theorem SSet.Truncated.Edge.id_tensor_id {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })) : (id x).tensor (id y) = id (x, y)

@[simp]

theorem SSet.Truncated.Edge.map_tensorHom {X Y X' Y' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (f : X ⟶ X') (g : Y ⟶ Y') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (e₁.map f).tensor (e₂.map g)

@[simp]

theorem SSet.Truncated.Edge.map_whiskerRight {X Y X' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (f : X ⟶ X') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = (e₁.map f).tensor e₂

@[simp]

theorem SSet.Truncated.Edge.map_whiskerLeft {X Y Y' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (g : Y ⟶ Y') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) = e₁.tensor (e₂.map g)

@[simp]

theorem SSet.Truncated.Edge.map_associator_hom {X Y Z : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') {z z' : Z.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₃ : Edge z z') : ((e₁.tensor e₂).tensor e₃).map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = e₁.tensor (e₂.tensor e₃)

@[simp]

theorem SSet.Truncated.Edge.map_fst {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) = e₁

@[simp]

theorem SSet.Truncated.Edge.map_snd {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) = e₂

def SSet.Truncated.Edge.CompStruct.tensor {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (e₀₁.tensor e'₀₁).CompStruct (e₁₂.tensor e'₁₂) (e₀₂.tensor e'₀₂)

The external product of CompStruct between edges of 2-truncated simplicial sets.

@[simp]

theorem SSet.Truncated.Edge.CompStruct.tensor_simplex_fst {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (hx.tensor hy).simplex.1 = hx.simplex

@[simp]

theorem SSet.Truncated.Edge.CompStruct.tensor_simplex_snd {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (hx.tensor hy).simplex.2 = hy.simplex

@[implicit_reducible]

instance SSet.Truncated.HomotopyCategory.instUniqueObjOppositeTruncatedTensorUnit {n : ℕ} (d : (SimplexCategory.Truncated n)ᵒᵖ) : Unique ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (Truncated n)).obj d)

def SSet.Truncated.HomotopyCategory.isoTerminal (X : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := isoTerminal._proof_1 }))] : CategoryTheory.Cat.of X.HomotopyCategory ≅ CategoryTheory.Cat.chosenTerminal

If X : Truncated 2 has a unique 0-simplex and (at most) one 1-simplex, this is the isomorphism Cat.of X.HomotopyCategory ≅ Cat.chosenTerminal in Cat.

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.square {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (ex : Edge x₀ x₁) {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (ey : Edge y₀ y₁) : CategoryTheory.CategoryStruct.comp (homMk (ex.tensor (Edge.id y₀))) (homMk ((Edge.id x₁).tensor ey)) = CategoryTheory.CategoryStruct.comp (homMk ((Edge.id x₀).tensor ey)) (homMk (ex.tensor (Edge.id y₁)))

def SSet.Truncated.HomotopyCategory.BinaryProduct.functor (X Y : Truncated 2) : CategoryTheory.Functor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory (X.HomotopyCategory × Y.HomotopyCategory)

The functor (X ⊗ Y).HomotopyCategory ⥤ X.HomotopyCategory × Y.HomotopyCategory when X and Y are 2-truncated simplicial sets.

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (functor X Y).obj (mk (x, y)) = (mk x, mk y)

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e : Edge x₀ x₁) {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e' : Edge y₀ y₁) : (functor X Y).map (homMk (e.tensor e')) = (homMk e, homMk e')

def SSet.Truncated.HomotopyCategory.BinaryProduct.curriedInverse (X Y : Truncated 2) : CategoryTheory.Functor X.HomotopyCategory (CategoryTheory.Functor Y.HomotopyCategory (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory)

The functor X.HomotopyCategory ⥤ Y.HomotopyCategory ⥤ (X ⊗ Y).HomotopyCategory when X and Y are 2-truncated simplicial sets.

def SSet.Truncated.HomotopyCategory.BinaryProduct.inverse (X Y : Truncated 2) : CategoryTheory.Functor (X.HomotopyCategory × Y.HomotopyCategory) (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory

The functor X.HomotopyCategory × Y.HomotopyCategory ⥤ (X ⊗ Y).HomotopyCategory when X and Y are 2-truncated simplicial sets.

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (inverse X Y).obj (mk x, mk y) = mk (x, y)

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e : Edge x₀ x₁) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (inverse X Y).map (CategoryTheory.Prod.mkHom (homMk e) (CategoryTheory.CategoryStruct.id (mk y))) = homMk (e.tensor (Edge.id y))

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e : Edge y₀ y₁) : (inverse X Y).map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (mk x)) (homMk e)) = homMk ((Edge.id x).tensor e)

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e : Edge x₀ x₁) {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (e' : Edge y₀ y₁) : (inverse X Y).map (CategoryTheory.Prod.mkHom (homMk e) (homMk e')) = homMk (e.tensor e')

def SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso (X Y : Truncated 2) : (functor X Y).comp (inverse X Y) ≅ CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory

Auxiliary definition for equivalence.

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (functorCompInverseIso X Y).hom.app (mk (x, y)) = CategoryTheory.CategoryStruct.id (((functor X Y).comp (inverse X Y)).obj (mk (x, y)))

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (functorCompInverseIso X Y).inv.app (mk (x, y)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory).obj (mk (x, y)))

def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso (X Y : Truncated 2) : (inverse X Y).comp (functor X Y) ≅ CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)

Auxiliary definition for equivalence.

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (inverseCompFunctorIso X Y).hom.app (mk x, mk y) = CategoryTheory.CategoryStruct.id (((inverse X Y).comp (functor X Y)).obj (mk x, mk y))

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })) : (inverseCompFunctorIso X Y).inv.app (mk x, mk y) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)).obj (mk x, mk y))

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse (X Y : Truncated 2) : (functor X Y).comp (inverse X Y) = CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor (X Y : Truncated 2) : (inverse X Y).comp (functor X Y) = CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)

def SSet.Truncated.HomotopyCategory.BinaryProduct.equivalence (X Y : Truncated 2) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory

The equivalence (X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory ⥤ Y.HomotopyCategory when X and Y are 2-truncated simplicial sets.

def SSet.Truncated.HomotopyCategory.BinaryProduct.iso (X Y : Truncated 2) : CategoryTheory.Cat.of (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory ≅ CategoryTheory.Cat.of (X.HomotopyCategory × Y.HomotopyCategory)

The isomorphism of categories between (X ⊗ Y).HomotopyCategory and X.HomotopyCategory ⥤ Y.HomotopyCategory.

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor (X Y : Truncated 2) : (iso X Y).inv.toFunctor = inverse X Y

@[simp]

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor (X Y : Truncated 2) : (iso X Y).hom.toFunctor = functor X Y

def SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIso {X X' : Truncated 2} (Y : Truncated 2) (f : X ⟶ X') : ((mapHomotopyCategory f).prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp (inverse X' Y) ≅ (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))

The naturality of HomotopyCategory.BinaryProduct.inverse with respect to the first variable.

def SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIso (X : Truncated 2) {Y Y' : Truncated 2} (g : Y ⟶ Y') : ((CategoryTheory.Functor.id X.HomotopyCategory).prod (mapHomotopyCategory g)).comp (inverse X Y') ≅ (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))

The naturality of HomotopyCategory.BinaryProduct.inverse with respect to the second variable.

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse {X X' : Truncated 2} (Y : Truncated 2) (f : X ⟶ X') : ((mapHomotopyCategory f).prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp (inverse X' Y) = (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse (X : Truncated 2) {Y Y' : Truncated 2} (g : Y ⟶ Y') : ((CategoryTheory.Functor.id X.HomotopyCategory).prod (mapHomotopyCategory g)).comp (inverse X Y') = (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))

def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIso (X Y : Truncated 2) : (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ≅ CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory

The compatibility of HomotopyCategory.BinaryProduct.inverse with respect to the first projection.

def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIso (X Y : Truncated 2) : (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ≅ CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory

The compatibility of HomotopyCategory.BinaryProduct.inverse with respect to the second projection.

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst (X Y : Truncated 2) : (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) = CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd (X Y : Truncated 2) : (inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) = CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality (X Y : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := isoTerminal._proof_1 }))] : CategoryTheory.Prod.snd (↑CategoryTheory.Cat.chosenTerminal) Y.HomotopyCategory = ((isoTerminal X).inv.toFunctor.prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp ((inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)))

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality (X Y : Truncated 2) [Unique (Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 }))] [Subsingleton (Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := isoTerminal._proof_1 }))] : CategoryTheory.Prod.fst X.HomotopyCategory ↑CategoryTheory.Cat.chosenTerminal = ((CategoryTheory.Functor.id X.HomotopyCategory).prod (isoTerminal Y).inv.toFunctor).comp ((inverse X Y).comp (mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)))

def SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso (X Y Z : Truncated 2) : (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse.comp (((inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp ((inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))) ≅ ((CategoryTheory.Functor.id X.HomotopyCategory).prod (inverse Y Z)).comp (inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))

Auxiliary definition for associativityIso.

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app {X Y Z : Truncated 2} (xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory) : (associativity'Iso X Y Z).hom.app xyz = CategoryTheory.CategoryStruct.id (((CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse.comp (((inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp ((inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)))).obj xyz)

def SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso (X Y Z : Truncated 2) : ((inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp ((inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) ≅ (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).functor.comp (((CategoryTheory.Functor.id X.HomotopyCategory).prod (inverse Y Z)).comp (inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))

The compatibility of HomotopyCategory.BinaryProduct.inverse with respect to associators.

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app {X Y Z : Truncated 2} (xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory) : (associativityIso X Y Z).hom.app xyz = CategoryTheory.CategoryStruct.id ((((inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp ((inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))).obj xyz)

theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativity (X Y Z : Truncated 2) : ((inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp ((inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp (mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) = (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).functor.comp (((CategoryTheory.Functor.id X.HomotopyCategory).prod (inverse Y Z)).comp (inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))

@[implicit_reducible]

instance SSet.Truncated.instMonoidalOfNatNatCatHoFunctor₂ : hoFunctor₂.Monoidal

@[implicit_reducible]

instance SSet.Truncated.hoFunctor.monoidal : hoFunctor.Monoidal

The homotopy category functor hoFunctor : SSet.{u} ⥤ Cat.{u, u} is (cartesian) monoidal.

def SSet.hoFunctor.unitHomEquiv (X : SSet) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ X) ≃ CategoryTheory.Functor ↑CategoryTheory.Cat.chosenTerminal ↑(hoFunctor.obj X)

An equivalence between the vertices of a simplicial set X and the objects of hoFunctor.obj X.

theorem SSet.hoFunctor.unitHomEquiv_eq (X : SSet) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ X) : (unitHomEquiv X) x = (CategoryTheory.Functor.LaxMonoidal.ε hoFunctor).toFunctor.comp (hoFunctor.map x).toFunctor