HomotopyCat

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

Statistics

Metric	Count
Definitions `OneTruncation₂`, `HoRel₂`, `map`, `nerveEquiv`, `nerveHomEquiv`, `ofNerve₂`, `natIso`, `reflQuiver`, `homMk`, `instUniqueOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk`, `isTerminal`, `mk`, `mkNatIso`, `mkNatTrans`, `morphismPropertyHomMk`, `quotientFunctor`, `ev01₂`, `ev02₂`, `ev0₂`, `ev12₂`, `ev1₂`, `ev2₂`, `hoFunctor₂`, `instCategoryHomotopyCategory`, `mapHomotopyCategory`, `δ0₂`, `δ1₂`, `δ2₂`, `ι0₂`, `ι1₂`, `ι2₂`, `hoFunctor`, `equiv`, `terminalIso`, `instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk`, `instUniqueHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk`, `instUniqueOneTruncation₂DeltaZero`, `isTerminalHoFunctorDeltaZero`, `oneTruncation₂`	39
Theorems `ext`, `mk`, `homOfEq_edge`, `hom_ext`, `hom_ext_iff`, `id_edge`, `map_map`, `map_obj`, `nerveEquiv_apply`, `nerveEquiv_symm_apply_map`, `nerveEquiv_symm_apply_obj`, `nerveHomEquiv_apply`, `nerveHomEquiv_id`, `nerve_hom_ext`, `natIso_hom_app_map`, `natIso_hom_app_obj`, `natIso_inv_app_map`, `natIso_inv_app_obj_map`, `natIso_inv_app_obj_obj`, `reflQuiver_Hom`, `reflQuiver_id`, `cases_on`, `congr_arrowMk_homMk`, `ext`, `functor_ext`, `homMk_comp_homMk`, `homMk_comp_homMk_assoc`, `homMk_id`, `instFullFreeReflOneTruncation₂QuotientFunctor`, `instSubsingletonOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk`, `lift_map_homMk`, `lift_obj_mk`, `lift_unique'`, `mkNatIso_hom_app_mk`, `mkNatIso_inv_app_mk`, `mkNatTrans_app_mk`, `mk_surjective`, `morphismPropertyHomMk_eq_strictMap`, `morphismPropertyHomMk_of_edge`, `morphismProperty_eq_top`, `multiplicativeClosure_morphismPropertyHomMk`, `subsingleton_hom`, `hoFunctor₂_naturality`, `mapHomotopyCategory_homMk`, `mapHomotopyCategory_obj`, `preservesTerminal`, `preservesTerminal'`, `instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk`, `oneTruncation₂_map`, `oneTruncation₂_obj`	50
Total	89

CategoryTheory.toNerve₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`SSet.OneTruncation₂.map` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve`	—	—	`SSet.OneTruncation₂.nerve_hom_ext`

SSet

Definitions

Name	Category	Theorems
`OneTruncation₂` 📖	CompOp	19 math math: `OneTruncation₂.nerveEquiv_apply`, `oneTruncation₂_obj`, `OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `OneTruncation₂.nerveHomEquiv_id`, `OneTruncation₂.homOfEq_edge`, `OneTruncation₂.reflQuiver_id`, `OneTruncation₂.HoRel₂.mk`, `Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor`, `OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `OneTruncation₂.nerveEquiv_symm_apply_map`, `Truncated.hoFunctor₂_naturality`, `OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `OneTruncation₂.nerveEquiv_symm_apply_obj`, `OneTruncation₂.reflQuiver_Hom`, `OneTruncation₂.nerveHomEquiv_apply`, `Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap`, `OneTruncation₂.map_map`, `OneTruncation₂.map_obj`, `OneTruncation₂.id_edge`
`hoFunctor` 📖	CompOp	12 math math: `hoFunctor.preservesTerminal'`, `hoFunctor.unitHomEquiv_eq`, `CategoryTheory.hoFunctor.preservesFiniteProducts`, `CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor`, `hoFunctor.preservesTerminal`, `CategoryTheory.hoFunctor.preservesBinaryProducts`, `CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex`, `CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve`, `CategoryTheory.hoFunctor.preservesBinaryProduct`, `CategoryTheory.hoFunctor.isIso_prodComparison`, `CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf`, `CategoryTheory.nerveAdjunction.isIso_counit`
`instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk` 📖	CompOp	—
`instUniqueHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk` 📖	CompOp	—
`instUniqueOneTruncation₂DeltaZero` 📖	CompOp	—
`isTerminalHoFunctorDeltaZero` 📖	CompOp	—
`oneTruncation₂` 📖	CompOp	8 math math: `oneTruncation₂_obj`, `OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `oneTruncation₂_map`, `OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `Truncated.hoFunctor₂_naturality`, `OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk` 📖	mathematical	—	`CategoryTheory.IsDiscrete` `Truncated.HomotopyCategory` `CategoryTheory.Functor.obj` `SSet` `largeCategory` `Truncated` `Truncated.largeCategory` `truncation` `SimplexCategory` `SimplexCategory.smallCategory` `stdSimplex` `Truncated.instCategoryHomotopyCategory`	—	`CategoryTheory.Quotient.instSubsingletonHom` `CategoryTheory.Cat.FreeRefl.instSubsingletonHomOfUnique` `Unique.instSubsingleton`
`oneTruncation₂_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Truncated` `Truncated.largeCategory` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `oneTruncation₂` `OneTruncation₂.map`	—	—
`oneTruncation₂_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Truncated` `Truncated.largeCategory` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `oneTruncation₂` `CategoryTheory.ReflQuiv.of` `OneTruncation₂` `OneTruncation₂.reflQuiver`	—	—

SSet.OneTruncation₂

Definitions

Name	Category	Theorems
`HoRel₂` 📖	CompData	1 math math: `HoRel₂.mk`
`map` 📖	CompOp	3 math math: `SSet.oneTruncation₂_map`, `map_map`, `map_obj`
`nerveEquiv` 📖	CompOp	8 math math: `nerveEquiv_apply`, `ofNerve₂.natIso_hom_app_map`, `nerveHomEquiv_id`, `ofNerve₂.natIso_hom_app_obj`, `nerveEquiv_symm_apply_map`, `ofNerve₂.natIso_inv_app_map`, `nerveEquiv_symm_apply_obj`, `nerveHomEquiv_apply`
`nerveHomEquiv` 📖	CompOp	4 math math: `ofNerve₂.natIso_hom_app_map`, `nerveHomEquiv_id`, `ofNerve₂.natIso_inv_app_map`, `nerveHomEquiv_apply`
`ofNerve₂` 📖	CompOp	—
`reflQuiver` 📖	CompOp	15 math math: `SSet.oneTruncation₂_obj`, `ofNerve₂.natIso_hom_app_map`, `nerveHomEquiv_id`, `homOfEq_edge`, `reflQuiver_id`, `HoRel₂.mk`, `SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor`, `SSet.Truncated.hoFunctor₂_naturality`, `ofNerve₂.natIso_inv_app_map`, `reflQuiver_Hom`, `nerveHomEquiv_apply`, `SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap`, `map_map`, `map_obj`, `id_edge`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homOfEq_edge` 📖	mathematical	—	`SSet.Truncated.Edge.edge` `Quiver.homOfEq` `SSet.OneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver`	—	—
`hom_ext` 📖	—	`SSet.Truncated.Edge.edge`	—	—	`SSet.Truncated.Edge.ext`
`hom_ext_iff` 📖	mathematical	—	`SSet.Truncated.Edge.edge`	—	`hom_ext`
`id_edge` 📖	mathematical	—	`SSet.Truncated.Edge.edge` `CategoryTheory.ReflQuiver.id` `SSet.OneTruncation₂` `reflQuiver` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.Truncated.σ₂`	—	—
`map_map` 📖	mathematical	—	`Prefunctor.map` `SSet.OneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver` `CategoryTheory.ReflPrefunctor.toPrefunctor` `map` `SSet.Truncated.Edge.map`	—	—
`map_obj` 📖	mathematical	—	`Prefunctor.obj` `SSet.OneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver` `CategoryTheory.ReflPrefunctor.toPrefunctor` `map` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op`	—	—
`nerveEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SSet.OneTruncation₂` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `EquivLike.toFunLike` `Equiv.instEquivLike` `nerveEquiv` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	—
`nerveEquiv_symm_apply_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `DFunLike.coe` `Equiv` `SSet.OneTruncation₂` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `nerveEquiv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`nerveEquiv_symm_apply_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `DFunLike.coe` `Equiv` `SSet.OneTruncation₂` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `nerveEquiv`	—	—
`nerveHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SSet.OneTruncation₂` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver` `CategoryTheory.catToReflQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `nerveEquiv` `nerveHomEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ComposableArrows.left` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.smallCategory` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `Opposite.op` `CategoryTheory.Functor.map` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `SimplexCategory.Truncated.δ₂` `SSet.Truncated.Edge.edge` `CategoryTheory.eqToHom` `CategoryTheory.ComposableArrows` `SSet.Truncated.Edge.src_eq` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `SSet.Truncated.Edge.tgt_eq`	—	—
`nerveHomEquiv_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SSet.OneTruncation₂` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver` `CategoryTheory.catToReflQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `nerveEquiv` `nerveHomEquiv` `CategoryTheory.ReflQuiver.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.nerve.homEquiv_id`
`nerve_hom_ext` 📖	—	`map` `CategoryTheory.Functor.obj` `SSet` `SSet.largeCategory` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.truncation` `CategoryTheory.nerve`	—	—	`SSet.Truncated.IsStrictSegal.hom_ext` `SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal` `CategoryTheory.Nerve.isStrictSegal` `SSet.Truncated.Edge.exists_of_simplex` `CategoryTheory.ReflPrefunctor.congr_obj` `homOfEq_edge` `CategoryTheory.ReflPrefunctor.congr_hom`
`reflQuiver_Hom` 📖	mathematical	—	`Quiver.Hom` `SSet.OneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `reflQuiver` `SSet.Truncated.Edge`	—	—
`reflQuiver_id` 📖	mathematical	—	`CategoryTheory.ReflQuiver.id` `SSet.OneTruncation₂` `reflQuiver` `SSet.Truncated.Edge.id`	—	—

SSet.OneTruncation₂.HoRel₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	—	`SSet.OneTruncation₂.HoRel₂` `CategoryTheory.Functor.obj` `CategoryTheory.Paths` `SSet.OneTruncation₂` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.ReflQuiver.toQuiver` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeRefl` `CategoryTheory.Cat.FreeRefl.instCategory` `CategoryTheory.Cat.FreeRefl.quotientFunctor` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom.toPath`	—	—

SSet.OneTruncation₂.ofNerve₂

Definitions

Name	Category	Theorems
`natIso` 📖	CompOp	5 math math: `natIso_hom_app_map`, `natIso_inv_app_obj_obj`, `natIso_hom_app_obj`, `natIso_inv_app_map`, `natIso_inv_app_obj_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natIso_hom_app_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.Bundled.α` `CategoryTheory.ReflQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `CategoryTheory.Functor.comp` `SSet.Truncated` `SSet.Truncated.largeCategory` `CategoryTheory.Nerve.nerveFunctor₂` `SSet.oneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.ReflQuiv.instReflQuiverα` `CategoryTheory.ReflQuiv.forget` `CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `natIso` `DFunLike.coe` `Equiv` `Quiver.Hom` `SSet.OneTruncation₂` `SSet` `SSet.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `CategoryTheory.Category` `CategoryTheory.Cat.str` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.catToReflQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `SSet.OneTruncation₂.nerveEquiv` `SSet.OneTruncation₂.nerveHomEquiv`	—	—
`natIso_hom_app_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.ReflQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `CategoryTheory.Functor.comp` `SSet.Truncated` `SSet.Truncated.largeCategory` `CategoryTheory.Nerve.nerveFunctor₂` `SSet.oneTruncation₂` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.ReflQuiv.instReflQuiverα` `CategoryTheory.ReflQuiv.forget` `CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `natIso` `DFunLike.coe` `Equiv` `SSet.OneTruncation₂` `SSet` `SSet.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `CategoryTheory.Category` `CategoryTheory.Cat.str` `EquivLike.toFunLike` `Equiv.instEquivLike` `SSet.OneTruncation₂.nerveEquiv`	—	—
`natIso_inv_app_map` 📖	mathematical	—	`Prefunctor.map` `CategoryTheory.Bundled.α` `CategoryTheory.ReflQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `CategoryTheory.ReflQuiv.forget` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.ReflQuiv.instReflQuiverα` `CategoryTheory.Functor.comp` `SSet.Truncated` `SSet.Truncated.largeCategory` `CategoryTheory.Nerve.nerveFunctor₂` `SSet.oneTruncation₂` `CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `natIso` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Category` `CategoryTheory.catToReflQuiver` `CategoryTheory.Cat.str` `SSet.OneTruncation₂` `SSet` `SSet.largeCategory` `SSet.truncation` `CategoryTheory.nerve` `EquivLike.toFunLike` `Equiv.instEquivLike` `SSet.OneTruncation₂.nerveEquiv` `Equiv.symm` `SSet.OneTruncation₂.reflQuiver` `SSet.OneTruncation₂.nerveHomEquiv`	—	—
`natIso_inv_app_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.smallCategory` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Cat.str` `Prefunctor.obj` `CategoryTheory.ReflQuiver` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `CategoryTheory.ReflQuiv.forget` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.ReflQuiv.instReflQuiverα` `CategoryTheory.Functor.comp` `SSet.Truncated` `SSet.Truncated.largeCategory` `CategoryTheory.Nerve.nerveFunctor₂` `SSet.oneTruncation₂` `CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `natIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`natIso_inv_app_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.smallCategory` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Cat.str` `Prefunctor.obj` `CategoryTheory.ReflQuiver` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `CategoryTheory.ReflQuiv.forget` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.ReflQuiv.instReflQuiverα` `CategoryTheory.Functor.comp` `SSet.Truncated` `SSet.Truncated.largeCategory` `CategoryTheory.Nerve.nerveFunctor₂` `SSet.oneTruncation₂` `CategoryTheory.ReflPrefunctor.toPrefunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `natIso`	—	—

SSet.Truncated

Definitions

Name	Category	Theorems
`ev01₂` 📖	CompOp	—
`ev02₂` 📖	CompOp	—
`ev0₂` 📖	CompOp	—
`ev12₂` 📖	CompOp	—
`ev1₂` 📖	CompOp	—
`ev2₂` 📖	CompOp	—
`hoFunctor₂` 📖	CompOp	—
`instCategoryHomotopyCategory` 📖	CompOp	50 math math: `HomotopyCategory.BinaryProduct.iso_inv_toFunctor`, `HomotopyCategory.descOfTruncation_comp`, `mapHomotopyCategory_homMk`, `SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk`, `HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk`, `HomotopyCategory.mkNatTrans_app_mk`, `HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app`, `HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app`, `HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk`, `HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst`, `HomotopyCategory.lift_obj_mk`, `HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd`, `HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor`, `HomotopyCategory.BinaryProduct.left_unitality`, `HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app`, `HomotopyCategory.homMk_id`, `HomotopyCategory.BinaryProduct.iso_hom_toFunctor`, `HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id`, `HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse`, `HomotopyCategory.BinaryProduct.functor_comp_inverse`, `HomotopyCategory.descOfTruncation_map_homMk`, `HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk`, `hoFunctor₂_naturality`, `HomotopyCategory.mkNatIso_inv_app_mk`, `HomotopyCategory.BinaryProduct.inverse_comp_functor`, `HomotopyCategory.homToNerveMk_app_one`, `HomotopyCategory.congr_arrowMk_homMk`, `mapHomotopyCategory_obj`, `HomotopyCategory.lift_map_homMk`, `HomotopyCategory.BinaryProduct.associativity'Iso_hom_app`, `HomotopyCategory.BinaryProduct.functor_obj`, `HomotopyCategory.mkNatIso_hom_app_mk`, `HomotopyCategory.BinaryProduct.square`, `HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app`, `HomotopyCategory.homToNerveMk_app_edge`, `HomotopyCategory.BinaryProduct.associativity`, `HomotopyCategory.BinaryProduct.right_unitality`, `HomotopyCategory.BinaryProduct.associativityIso_hom_app`, `HomotopyCategory.homMk_comp_homMk_assoc`, `HomotopyCategory.homToNerveMk_app_zero`, `HomotopyCategory.morphismPropertyHomMk_eq_strictMap`, `HomotopyCategory.homMk_comp_homMk`, `HomotopyCategory.homToNerveMk_comp`, `HomotopyCategory.BinaryProduct.functor_map`, `HomotopyCategory.subsingleton_hom`, `HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse`, `HomotopyCategory.descOfTruncation_obj_mk`, `HomotopyCategory.BinaryProduct.inverse_obj`, `HomotopyCategory.homToNerveMk_comp_assoc`, `HomotopyCategory.morphismProperty_eq_top`
`mapHomotopyCategory` 📖	CompOp	13 math math: `HomotopyCategory.descOfTruncation_comp`, `mapHomotopyCategory_homMk`, `HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst`, `HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd`, `HomotopyCategory.BinaryProduct.left_unitality`, `HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse`, `hoFunctor₂_naturality`, `mapHomotopyCategory_obj`, `HomotopyCategory.BinaryProduct.associativity'Iso_hom_app`, `HomotopyCategory.BinaryProduct.associativity`, `HomotopyCategory.BinaryProduct.right_unitality`, `HomotopyCategory.BinaryProduct.associativityIso_hom_app`, `HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse`
`δ0₂` 📖	CompOp	—
`δ1₂` 📖	CompOp	—
`δ2₂` 📖	CompOp	—
`ι0₂` 📖	CompOp	—
`ι1₂` 📖	CompOp	—
`ι2₂` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hoFunctor₂_naturality` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Functor.obj` `SSet.Truncated` `largeCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.ReflQuiv` `CategoryTheory.ReflQuiv.category` `SSet.oneTruncation₂` `CategoryTheory.Cat.freeRefl` `CategoryTheory.Cat.str` `HomotopyCategory` `instCategoryHomotopyCategory` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Functor.map` `HomotopyCategory.quotientFunctor` `CategoryTheory.Cat.FreeRefl` `SSet.OneTruncation₂` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeRefl.instCategory` `mapHomotopyCategory`	—	—
`mapHomotopyCategory_homMk` 📖	mathematical	—	`CategoryTheory.Functor.map` `HomotopyCategory` `instCategoryHomotopyCategory` `mapHomotopyCategory` `HomotopyCategory.homMk` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `Edge.map`	—	—
`mapHomotopyCategory_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `HomotopyCategory` `instCategoryHomotopyCategory` `mapHomotopyCategory` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op`	—	—

SSet.Truncated.HomotopyCategory

Definitions

Name	Category	Theorems
`homMk` 📖	CompOp	15 math math: `SSet.Truncated.mapHomotopyCategory_homMk`, `BinaryProduct.inverse_map_mkHom_id_homMk`, `homMk_id`, `BinaryProduct.inverse_map_mkHom_homMk_id`, `descOfTruncation_map_homMk`, `BinaryProduct.inverse_map_mkHom_homMk_homMk`, `homToNerveMk_app_one`, `congr_arrowMk_homMk`, `lift_map_homMk`, `BinaryProduct.square`, `homToNerveMk_app_edge`, `homMk_comp_homMk_assoc`, `homMk_comp_homMk`, `BinaryProduct.functor_map`, `morphismPropertyHomMk_of_edge`
`instUniqueOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk` 📖	CompOp	—
`isTerminal` 📖	CompOp	—
`mk` 📖	CompOp	—
`mkNatIso` 📖	CompOp	2 math math: `mkNatIso_inv_app_mk`, `mkNatIso_hom_app_mk`
`mkNatTrans` 📖	CompOp	1 math math: `mkNatTrans_app_mk`
`morphismPropertyHomMk` 📖	CompOp	3 math math: `multiplicativeClosure_morphismPropertyHomMk`, `morphismPropertyHomMk_eq_strictMap`, `morphismPropertyHomMk_of_edge`
`quotientFunctor` 📖	CompOp	3 math math: `instFullFreeReflOneTruncation₂QuotientFunctor`, `SSet.Truncated.hoFunctor₂_naturality`, `morphismPropertyHomMk_eq_strictMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cases_on` 📖	—	—	—	—	`mk_surjective`
`congr_arrowMk_homMk` 📖	mathematical	`SSet.Truncated.Edge.edge`	`SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `homMk`	—	`SSet.Truncated.Edge.ext` `SSet.Truncated.Edge.tgt_eq` `SSet.Truncated.Edge.src_eq`
`ext` 📖	—	`CategoryTheory.Quotient.as` `CategoryTheory.Paths` `SSet.OneTruncation₂` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.ReflQuiver.toQuiver` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeReflRel` `CategoryTheory.Cat.FreeRefl` `CategoryTheory.Cat.FreeRefl.instCategory` `SSet.OneTruncation₂.HoRel₂`	—	—	`mk_surjective`
`functor_ext` 📖	—	`CategoryTheory.Functor.obj` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `CategoryTheory.Functor.map` `homMk` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	—	`CategoryTheory.Functor.ext_of_iso` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans` `CategoryTheory.Category.comp_id`
`homMk_comp_homMk` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet.Truncated.HomotopyCategory` `CategoryTheory.Category.toCategoryStruct` `SSet.Truncated.instCategoryHomotopyCategory` `homMk`	—	`CategoryTheory.Functor.map_comp` `CategoryTheory.Quotient.sound`
`homMk_comp_homMk_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet.Truncated.HomotopyCategory` `CategoryTheory.Category.toCategoryStruct` `SSet.Truncated.instCategoryHomotopyCategory` `homMk`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homMk_comp_homMk`
`homMk_id` 📖	mathematical	—	`homMk` `SSet.Truncated.Edge.id` `CategoryTheory.CategoryStruct.id` `SSet.Truncated.HomotopyCategory` `CategoryTheory.Category.toCategoryStruct` `SSet.Truncated.instCategoryHomotopyCategory`	—	`homMk.eq_1` `SSet.OneTruncation₂.reflQuiver_id` `CategoryTheory.Cat.FreeRefl.homMk_id` `CategoryTheory.Functor.map_id`
`instFullFreeReflOneTruncation₂QuotientFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Cat.FreeRefl` `SSet.OneTruncation₂` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeRefl.instCategory` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `quotientFunctor`	—	`CategoryTheory.Quotient.full_functor`
`instSubsingletonOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk` 📖	mathematical	—	`SSet.Truncated.HomotopyCategory`	—	`mk_surjective`
`lift_map_homMk` 📖	mathematical	`SSet.Truncated.Edge.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	`CategoryTheory.Functor.map` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `lift` `homMk`	—	`CategoryTheory.Category.id_comp`
`lift_obj_mk` 📖	mathematical	`SSet.Truncated.Edge.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	`CategoryTheory.Functor.obj` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `lift`	—	—
`lift_unique'` 📖	—	`CategoryTheory.Functor.comp` `CategoryTheory.Cat.FreeRefl` `SSet.OneTruncation₂` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeRefl.instCategory` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `quotientFunctor`	—	—	`CategoryTheory.Quotient.lift_unique'`
`mkNatIso_hom_app_mk` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mkNatIso` `CategoryTheory.Functor.obj`	—	—
`mkNatIso_inv_app_mk` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mkNatIso` `CategoryTheory.Functor.obj`	—	—
`mkNatTrans_app_mk` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `mkNatTrans`	—	—
`mk_surjective` 📖	mathematical	—	`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`	—	—
`morphismPropertyHomMk_eq_strictMap` 📖	mathematical	—	`morphismPropertyHomMk` `CategoryTheory.MorphismProperty.strictMap` `CategoryTheory.Cat.FreeRefl` `SSet.OneTruncation₂` `SSet.OneTruncation₂.reflQuiver` `CategoryTheory.Cat.FreeRefl.instCategory` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk` `quotientFunctor`	—	`CategoryTheory.MorphismProperty.ext` `CategoryTheory.MorphismProperty.map_mem_strictMap` `morphismPropertyHomMk_of_edge`
`morphismPropertyHomMk_of_edge` 📖	mathematical	—	`morphismPropertyHomMk` `homMk`	—	`CategoryTheory.MorphismProperty.ofHoms_iff`
`morphismProperty_eq_top` 📖	mathematical	`homMk`	`Top.top` `CategoryTheory.MorphismProperty` `SSet.Truncated.HomotopyCategory` `CategoryTheory.Category.toCategoryStruct` `SSet.Truncated.instCategoryHomotopyCategory` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`le_antisymm` `multiplicativeClosure_morphismPropertyHomMk` `CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff`
`multiplicativeClosure_morphismPropertyHomMk` 📖	mathematical	—	`CategoryTheory.MorphismProperty.multiplicativeClosure` `SSet.Truncated.HomotopyCategory` `SSet.Truncated.instCategoryHomotopyCategory` `morphismPropertyHomMk` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`le_antisymm` `CategoryTheory.Functor.map_surjective` `instFullFreeReflOneTruncation₂QuotientFunctor` `morphismPropertyHomMk_eq_strictMap` `CategoryTheory.MorphismProperty.strictMap_multiplicativeClosure_le` `CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk` `CategoryTheory.MorphismProperty.map_mem_strictMap`
`subsingleton_hom` 📖	mathematical	—	`Quiver.Hom` `SSet.Truncated.HomotopyCategory` `CategoryTheory.ReflQuiver.toQuiver` `CategoryTheory.catToReflQuiver` `SSet.Truncated.instCategoryHomotopyCategory`	—	`CategoryTheory.Quotient.instSubsingletonHom` `CategoryTheory.Cat.FreeRefl.instSubsingletonHomOfUnique` `SSet.Truncated.Edge.instSubsingleton`

SSet.hoFunctor

Definitions

Name	Category	Theorems
`terminalIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesTerminal` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `SSet` `SSet.largeCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `SSet.hoFunctor`	—	`CategoryTheory.Limits.preservesTerminal_of_iso` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `CategoryTheory.Cat.instHasTerminal`
`preservesTerminal'` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `SSet` `SSet.largeCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `SSet.hoFunctor`	—	`CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal` `preservesTerminal`

SSet.hoFunctor.obj

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—

---

← Back to Index