HoFunctorMonoidal

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean

Statistics

Metric	Count
Definitions tensor, tensor, associativity'Iso, associativityIso, curriedInverse, equivalence, functor, functorCompInverseIso, idProdMapHomotopyCategoryCompInverseIso, inverse, inverseCompFunctorIso, inverseCompMapHomotopyCategoryFstIso, inverseCompMapHomotopyCategorySndIso, iso, mapHomotopyCategoryProdIdCompInverseIso, instUniqueObjOppositeTruncatedTensorUnit, isoTerminal, monoidal, instMonoidalOfNatNatCatHoFunctor₂, unitHomEquiv	20
Theorems tensor_simplex_fst, tensor_simplex_snd, id_tensor_id, map_associator_hom, map_fst, map_snd, map_tensorHom, map_whiskerLeft, map_whiskerRight, tensor_edge, tensor_surjective, associativity, associativity'Iso_hom_app, associativityIso_hom_app, functorCompInverseIso_hom_app, functorCompInverseIso_inv_app, functor_comp_inverse, functor_map, functor_obj, id_prod_mapHomotopyCategory_comp_inverse, inverseCompFunctorIso_hom_app, inverseCompFunctorIso_inv_app, inverse_comp_functor, inverse_comp_mapHomotopyCategory_fst, inverse_comp_mapHomotopyCategory_snd, inverse_map_mkHom_homMk_homMk, inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk, inverse_obj, iso_hom_toFunctor, iso_inv_toFunctor, left_unitality, mapHomotopyCategory_prod_id_comp_inverse, right_unitality, square, unitHomEquiv_eq	36
Total	56

SSet.Truncated

Definitions

Name	Category	Theorems
instMonoidalOfNatNatCatHoFunctor₂ 📖	CompOp	—

SSet.Truncated.Edge

Definitions

Name	Category	Theorems
tensor 📖	CompOp	16 math math: SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, map_fst, tensor_surjective, CompStruct.tensor_simplex_snd, id_tensor_id, CompStruct.tensor_simplex_fst, map_associator_hom, map_whiskerLeft, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, map_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, map_tensorHom, tensor_edge, SSet.Truncated.HomotopyCategory.BinaryProduct.square, map_whiskerRight, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_tensor_id 📖	mathematical	—	tensor id CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op	—	—
map_associator_hom 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
map_fst 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.SemiCartesianMonoidalCategory.fst	—	—
map_snd 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
map_tensorHom 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app	—	—
map_whiskerLeft 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app	—	—
map_whiskerRight 📖	mathematical	—	map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app	—	—
tensor_edge 📖	mathematical	—	edge CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op tensor	—	—
tensor_surjective 📖	mathematical	—	tensor	—	—

SSet.Truncated.Edge.CompStruct

Definitions

Name	Category	Theorems
tensor 📖	CompOp	2 math math: tensor_simplex_snd, tensor_simplex_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_simplex_fst 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op simplex CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.Edge.tensor tensor	—	—
tensor_simplex_snd 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op simplex CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.Edge.tensor tensor	—	—

SSet.Truncated.HomotopyCategory

Definitions

Name	Category	Theorems
instUniqueObjOppositeTruncatedTensorUnit 📖	CompOp	—
isoTerminal 📖	CompOp	2 math math: BinaryProduct.left_unitality, BinaryProduct.right_unitality

SSet.Truncated.HomotopyCategory.BinaryProduct

Definitions

Name	Category	Theorems
associativity'Iso 📖	CompOp	1 math math: associativity'Iso_hom_app
associativityIso 📖	CompOp	1 math math: associativityIso_hom_app
curriedInverse 📖	CompOp	—
equivalence 📖	CompOp	—
functor 📖	CompOp	9 math math: functorCompInverseIso_inv_app, functorCompInverseIso_hom_app, inverseCompFunctorIso_inv_app, iso_hom_toFunctor, functor_comp_inverse, inverse_comp_functor, functor_obj, inverseCompFunctorIso_hom_app, functor_map
functorCompInverseIso 📖	CompOp	2 math math: functorCompInverseIso_inv_app, functorCompInverseIso_hom_app
idProdMapHomotopyCategoryCompInverseIso 📖	CompOp	—
inverse 📖	CompOp	20 math math: iso_inv_toFunctor, inverse_map_mkHom_id_homMk, functorCompInverseIso_inv_app, functorCompInverseIso_hom_app, inverse_comp_mapHomotopyCategory_fst, inverse_comp_mapHomotopyCategory_snd, left_unitality, inverseCompFunctorIso_inv_app, inverse_map_mkHom_homMk_id, mapHomotopyCategory_prod_id_comp_inverse, functor_comp_inverse, inverse_map_mkHom_homMk_homMk, inverse_comp_functor, associativity'Iso_hom_app, inverseCompFunctorIso_hom_app, associativity, right_unitality, associativityIso_hom_app, id_prod_mapHomotopyCategory_comp_inverse, inverse_obj
inverseCompFunctorIso 📖	CompOp	2 math math: inverseCompFunctorIso_inv_app, inverseCompFunctorIso_hom_app
inverseCompMapHomotopyCategoryFstIso 📖	CompOp	—
inverseCompMapHomotopyCategorySndIso 📖	CompOp	—
iso 📖	CompOp	2 math math: iso_inv_toFunctor, iso_hom_toFunctor
mapHomotopyCategoryProdIdCompInverseIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associativity 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.prod' CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.prod inverse CategoryTheory.Functor.id SSet.Truncated.mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Equivalence.functor CategoryTheory.prod.associativity	—	CategoryTheory.Functor.ext_of_iso associativityIso_hom_app
associativity'Iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.prod' SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.prod.associativity CategoryTheory.Functor.prod CategoryTheory.uniformProd inverse CategoryTheory.Functor.id SSet.Truncated.mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor CategoryTheory.Functor.category associativity'Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
associativityIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.prod' CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.comp CategoryTheory.Functor.prod inverse CategoryTheory.Functor.id SSet.Truncated.mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Equivalence.functor CategoryTheory.prod.associativity CategoryTheory.Functor CategoryTheory.Functor.category associativityIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	associativity'Iso_hom_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.prod_id
functorCompInverseIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.comp CategoryTheory.uniformProd functor inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category functorCompInverseIso CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functorCompInverseIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.uniformProd functor inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category functorCompInverseIso CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functor_comp_inverse 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.uniformProd functor inverse CategoryTheory.Functor.id	—	CategoryTheory.Functor.ext_of_iso
functor_map 📖	mathematical	—	CategoryTheory.Functor.map SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.uniformProd functor CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.HomotopyCategory.homMk SSet.Truncated.Edge.tensor Quiver.Hom CategoryTheory.ReflQuiver.toQuiver CategoryTheory.catToReflQuiver	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.uniformProd functor Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op	—	—
id_prod_mapHomotopyCategory_comp_inverse 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.prod' SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.prod CategoryTheory.Functor.id SSet.Truncated.mapHomotopyCategory inverse CategoryTheory.uniformProd CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Functor.ext_of_iso
inverseCompFunctorIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category inverseCompFunctorIso CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
inverseCompFunctorIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inverseCompFunctorIso CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
inverse_comp_functor 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse functor CategoryTheory.Functor.id	—	CategoryTheory.Functor.ext_of_iso
inverse_comp_mapHomotopyCategory_fst 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse SSet.Truncated.mapHomotopyCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Prod.fst	—	CategoryTheory.Functor.ext_of_iso
inverse_comp_mapHomotopyCategory_snd 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse SSet.Truncated.mapHomotopyCategory CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Prod.snd	—	CategoryTheory.Functor.ext_of_iso
inverse_map_mkHom_homMk_homMk 📖	mathematical	—	CategoryTheory.Functor.map SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct SSet.Truncated.HomotopyCategory.homMk CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Edge.tensor	—	SSet.Truncated.HomotopyCategory.homMk_comp_homMk
inverse_map_mkHom_homMk_id 📖	mathematical	—	CategoryTheory.Functor.map SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct SSet.Truncated.HomotopyCategory.homMk CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Edge.tensor SSet.Truncated.Edge.id	—	—
inverse_map_mkHom_id_homMk 📖	mathematical	—	CategoryTheory.Functor.map SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id SSet.Truncated.HomotopyCategory.homMk CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Edge.tensor SSet.Truncated.Edge.id	—	—
inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op	—	—
iso_hom_toFunctor 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.uniformProd CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.category iso functor	—	—
iso_inv_toFunctor 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of SSet.Truncated.HomotopyCategory CategoryTheory.uniformProd SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.category iso inverse	—	—
left_unitality 📖	mathematical	—	CategoryTheory.Prod.snd CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.chosenTerminal CategoryTheory.Cat.str SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.comp CategoryTheory.prod' CategoryTheory.Cat.of CategoryTheory.Functor.prod CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated.HomotopyCategory.isoTerminal CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse SSet.Truncated.mapHomotopyCategory CategoryTheory.SemiCartesianMonoidalCategory.snd	—	inverse_comp_mapHomotopyCategory_snd
mapHomotopyCategory_prod_id_comp_inverse 📖	mathematical	—	CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory CategoryTheory.prod' SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Functor.prod SSet.Truncated.mapHomotopyCategory CategoryTheory.Functor.id inverse CategoryTheory.uniformProd CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Functor.ext_of_iso
right_unitality 📖	mathematical	—	CategoryTheory.Prod.fst SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.chosenTerminal CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.prod' CategoryTheory.Cat.of CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated.HomotopyCategory.isoTerminal CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory inverse SSet.Truncated.mapHomotopyCategory CategoryTheory.SemiCartesianMonoidalCategory.fst	—	inverse_comp_mapHomotopyCategory_fst
square 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet.Truncated.HomotopyCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.Truncated.instCartesianMonoidalCategory CategoryTheory.Category.toCategoryStruct SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.HomotopyCategory.homMk SSet.Truncated.Edge.tensor SSet.Truncated.Edge.id	—	SSet.Truncated.HomotopyCategory.homMk_comp_homMk

SSet.Truncated.hoFunctor

Definitions

Name	Category	Theorems
monoidal 📖	CompOp	1 math math: SSet.hoFunctor.unitHomEquiv_eq

SSet.hoFunctor

Definitions

Name	Category	Theorems
unitHomEquiv 📖	CompOp	1 math math: unitHomEquiv_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
unitHomEquiv_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.ReflQuiver.toQuiver CategoryTheory.catToReflQuiver SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.chosenTerminal CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category SSet.hoFunctor EquivLike.toFunLike Equiv.instEquivLike unitHomEquiv CategoryTheory.Functor.comp CategoryTheory.Cat.instCartesianMonoidalCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal SSet.Truncated.hoFunctor.monoidal CategoryTheory.Functor.map	—	—

---

← Back to Index