Basic

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Basic.lean

Statistics

Metric	Count
Definitions AugmentedSimplexCategory, equivAugmentedCosimplicialObjecFunctorCompPointIso, equivAugmentedCosimplicialObject, equivAugmentedCosimplicialObjectFunctorCompDropIso, equivAugmentedCosimplicialObjectFunctorCompPointIso, equivAugmentedCosimplicialObjectFunctorCompToArrowIso, equivAugmentedSimplicialObject, equivAugmentedSimplicialObjectFunctorCompDropIso, equivAugmentedSimplicialObjectFunctorCompPointIso, equivAugmentedSimplicialObjectFunctorCompToArrowIso, inclusion	11
Theorems equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, equivAugmentedCosimplicialObject_counitIso_inv_app_left, equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, equivAugmentedCosimplicialObject_functor_map_left, equivAugmentedCosimplicialObject_functor_map_right_app, equivAugmentedCosimplicialObject_functor_obj_hom_app, equivAugmentedCosimplicialObject_functor_obj_left, equivAugmentedCosimplicialObject_functor_obj_right_map, equivAugmentedCosimplicialObject_functor_obj_right_obj, equivAugmentedCosimplicialObject_inverse_map_app, equivAugmentedCosimplicialObject_inverse_obj_map, equivAugmentedCosimplicialObject_inverse_obj_obj, equivAugmentedCosimplicialObject_unitIso_hom_app_app, equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, equivAugmentedSimplicialObject_counitIso_hom_app_left_app, equivAugmentedSimplicialObject_counitIso_hom_app_right, equivAugmentedSimplicialObject_counitIso_inv_app_left_app, equivAugmentedSimplicialObject_counitIso_inv_app_right, equivAugmentedSimplicialObject_functor_map_left_app, equivAugmentedSimplicialObject_functor_map_right, equivAugmentedSimplicialObject_functor_obj_hom_app, equivAugmentedSimplicialObject_functor_obj_left_map, equivAugmentedSimplicialObject_functor_obj_left_obj, equivAugmentedSimplicialObject_functor_obj_right, equivAugmentedSimplicialObject_inverse_map_app, equivAugmentedSimplicialObject_inverse_obj_map, equivAugmentedSimplicialObject_inverse_obj_obj, equivAugmentedSimplicialObject_unitIso_hom_app_app, equivAugmentedSimplicialObject_unitIso_inv_app_app, inclusion_map, inclusion_obj, instFaithfulSimplexCategoryInclusion, instFullSimplexCategoryInclusion, instHasInitial	51
Total	62

AugmentedSimplexCategory

Definitions

Name	Category	Theorems
equivAugmentedCosimplicialObjecFunctorCompPointIso 📖	CompOp	—
equivAugmentedCosimplicialObject 📖	CompOp	23 math math: equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivAugmentedCosimplicialObject_inverse_map_app, equivAugmentedCosimplicialObject_functor_obj_left, equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, equivAugmentedCosimplicialObject_inverse_obj_map, equivAugmentedCosimplicialObject_inverse_obj_obj, equivAugmentedCosimplicialObject_functor_map_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, equivAugmentedCosimplicialObject_functor_obj_right_map, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, equivAugmentedCosimplicialObject_functor_map_right_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, equivAugmentedCosimplicialObject_functor_obj_hom_app, equivAugmentedCosimplicialObject_functor_obj_right_obj, equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, equivAugmentedCosimplicialObject_counitIso_inv_app_left, equivAugmentedCosimplicialObject_unitIso_hom_app_app
equivAugmentedCosimplicialObjectFunctorCompDropIso 📖	CompOp	2 math math: equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app
equivAugmentedCosimplicialObjectFunctorCompPointIso 📖	CompOp	2 math math: equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app
equivAugmentedCosimplicialObjectFunctorCompToArrowIso 📖	CompOp	4 math math: equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right
equivAugmentedSimplicialObject 📖	CompOp	23 math math: equivAugmentedSimplicialObject_inverse_map_app, equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, equivAugmentedSimplicialObject_inverse_obj_obj, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, equivAugmentedSimplicialObject_counitIso_inv_app_left_app, equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedSimplicialObject_functor_map_right, equivAugmentedSimplicialObject_functor_map_left_app, equivAugmentedSimplicialObject_counitIso_hom_app_right, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedSimplicialObject_counitIso_hom_app_left_app, equivAugmentedSimplicialObject_functor_obj_hom_app, equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, equivAugmentedSimplicialObject_unitIso_hom_app_app, equivAugmentedSimplicialObject_counitIso_inv_app_right, equivAugmentedSimplicialObject_unitIso_inv_app_app, equivAugmentedSimplicialObject_functor_obj_right, equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, equivAugmentedSimplicialObject_functor_obj_left_map, equivAugmentedSimplicialObject_inverse_obj_map, equivAugmentedSimplicialObject_functor_obj_left_obj
equivAugmentedSimplicialObjectFunctorCompDropIso 📖	CompOp	2 math math: equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app
equivAugmentedSimplicialObjectFunctorCompPointIso 📖	CompOp	2 math math: equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app
equivAugmentedSimplicialObjectFunctorCompToArrowIso 📖	CompOp	4 math math: equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right
inclusion 📖	CompOp	8 math math: inclusion_obj, instFullSimplexCategoryInclusion, equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, instFaithfulSimplexCategoryInclusion, inclusion_map, equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.drop CategoryTheory.Iso.hom CategoryTheory.Functor.whiskeringLeft inclusion equivAugmentedCosimplicialObjectFunctorCompDropIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial CategoryTheory.WithInitial.incl	—	—
equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.drop CategoryTheory.Iso.inv CategoryTheory.Functor.whiskeringLeft inclusion equivAugmentedCosimplicialObjectFunctorCompDropIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial CategoryTheory.WithInitial.incl	—	—
equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.point CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.WithInitial.star equivAugmentedCosimplicialObjectFunctorCompPointIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial	—	—
equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.point CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.WithInitial.star equivAugmentedCosimplicialObjectFunctorCompPointIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial	—	—
equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation CategoryTheory.WithInitial.star CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.homTo equivAugmentedCosimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation CategoryTheory.WithInitial.star CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.homTo equivAugmentedCosimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation CategoryTheory.WithInitial.star CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.homTo equivAugmentedCosimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedCosimplicialObject CategoryTheory.CosimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation CategoryTheory.WithInitial.star CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.homTo equivAugmentedCosimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivAugmentedCosimplicialObject_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
equivAugmentedCosimplicialObject_counitIso_hom_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.incl CategoryTheory.Comma.left	—	—
equivAugmentedCosimplicialObject_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
equivAugmentedCosimplicialObject_counitIso_inv_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.incl CategoryTheory.Comma.left	—	—
equivAugmentedCosimplicialObject_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.WithInitial.mkCommaObject CategoryTheory.Functor.map CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.NatTrans.app CategoryTheory.WithInitial.star	—	—
equivAugmentedCosimplicialObject_functor_map_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.incl CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.WithInitial.mkCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.Functor.obj	—	—
equivAugmentedCosimplicialObject_functor_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.star CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.Functor.map CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.WithInitial.of	—	—
equivAugmentedCosimplicialObject_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.WithInitial.star	—	—
equivAugmentedCosimplicialObject_functor_obj_right_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.WithInitial.incl	—	—
equivAugmentedCosimplicialObject_functor_obj_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.WithInitial.incl	—	—
equivAugmentedCosimplicialObject_inverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.WithInitial.ofCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.right CategoryTheory.CommaMorphism.left	—	—
equivAugmentedCosimplicialObject_inverse_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.WithInitial.down CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
equivAugmentedCosimplicialObject_inverse_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.Comma.right CategoryTheory.Comma.left	—	—
equivAugmentedCosimplicialObject_unitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.const CategoryTheory.commaCategory CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
equivAugmentedCosimplicialObject_unitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.WithInitial.mkCommaObject CategoryTheory.WithInitial.mkCommaMorphism CategoryTheory.WithInitial.ofCommaObject CategoryTheory.WithInitial.ofCommaMorphism CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso AugmentedSimplexCategory CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented equivAugmentedCosimplicialObject CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.drop CategoryTheory.Iso.hom CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op inclusion equivAugmentedSimplicialObjectFunctorCompDropIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.drop CategoryTheory.Iso.inv CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op inclusion equivAugmentedSimplicialObjectFunctorCompDropIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.point CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial.star equivAugmentedSimplicialObjectFunctorCompPointIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial	—	—
equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.point CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial.star equivAugmentedSimplicialObjectFunctorCompPointIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial	—	—
equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.homTo equivAugmentedSimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl CategoryTheory.WithInitial.of Opposite.unop	—	—
equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.homTo equivAugmentedSimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id	—	—
equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.homTo equivAugmentedSimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl CategoryTheory.WithInitial.of Opposite.unop	—	—
equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Functor Opposite AugmentedSimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor equivAugmentedSimplicialObject CategoryTheory.SimplicialObject.Augmented.toArrow CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor.mapArrowFunctor CategoryTheory.evaluation Opposite.op CategoryTheory.WithInitial CategoryTheory.WithInitial.incl CategoryTheory.WithInitial.star Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.homTo equivAugmentedSimplicialObjectFunctorCompToArrowIso CategoryTheory.CategoryStruct.id	—	—
equivAugmentedSimplicialObject_counitIso_hom_app_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Equivalence.functor CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory equivAugmentedSimplicialObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.const CategoryTheory.Comma.right Opposite.unop CategoryTheory.WithTerminal.incl Opposite.op CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.WithTerminal.of CategoryTheory.WithTerminal.star CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Functor.map CategoryTheory.WithTerminal.down CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Equivalence.invFunIdAssoc_hom_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
equivAugmentedSimplicialObject_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.const	—	CategoryTheory.Equivalence.invFunIdAssoc_hom_app CategoryTheory.Category.comp_id
equivAugmentedSimplicialObject_counitIso_inv_app_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Equivalence.functor CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.WithTerminal.incl CategoryTheory.Functor.const CategoryTheory.Comma.right Opposite.unop Opposite.op CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.WithTerminal.of CategoryTheory.WithTerminal.star CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Functor.map CategoryTheory.WithTerminal.down CategoryTheory.Comma.hom	—	CategoryTheory.Equivalence.invFunIdAssoc_inv_app CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
equivAugmentedSimplicialObject_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.inverse CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.const	—	CategoryTheory.Equivalence.invFunIdAssoc_inv_app CategoryTheory.Category.comp_id
equivAugmentedSimplicialObject_functor_map_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.WithTerminal.equivComma CategoryTheory.Functor.map AugmentedSimplexCategory equivAugmentedSimplicialObject Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObject_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.WithTerminal Opposite SimplexCategory CategoryTheory.WithTerminal.instCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor CategoryTheory.WithTerminal.equivComma CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Functor.map AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.NatTrans.app Opposite.op CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObject_functor_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.Functor.const CategoryTheory.WithTerminal.star CategoryTheory.Comma.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.Functor.map Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal CategoryTheory.WithTerminal.of CategoryTheory.WithInitial.down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite	—	—
equivAugmentedSimplicialObject_functor_obj_left_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite	—	—
equivAugmentedSimplicialObject_functor_obj_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.incl Opposite.op CategoryTheory.WithInitial.of Opposite.unop CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObject_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Equivalence.functor AugmentedSimplexCategory equivAugmentedSimplicialObject Opposite.op CategoryTheory.WithInitial.star	—	—
equivAugmentedSimplicialObject_inverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.WithTerminal.equivComma CategoryTheory.Functor.map AugmentedSimplexCategory equivAugmentedSimplicialObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right	—	—
equivAugmentedSimplicialObject_inverse_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse AugmentedSimplexCategory equivAugmentedSimplicialObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right CategoryTheory.WithTerminal Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.instCategory Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal CategoryTheory.CategoryStruct.id CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	—
equivAugmentedSimplicialObject_inverse_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.WithTerminal Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right	—	—
equivAugmentedSimplicialObject_unitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.WithTerminal.incl CategoryTheory.Functor.map CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Iso.app	—	CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
equivAugmentedSimplicialObject_unitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithInitial SimplexCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.congrLeft CategoryTheory.WithInitial.opEquiv CategoryTheory.WithTerminal.equivComma CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso AugmentedSimplexCategory equivAugmentedSimplicialObject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.incl CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Equivalence.funInvIdAssoc_hom_app
inclusion_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory inclusion	—	—
inclusion_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory inclusion CategoryTheory.WithInitial.of	—	—
instFaithfulSimplexCategoryInclusion 📖	mathematical	—	CategoryTheory.Functor.Faithful SimplexCategory SimplexCategory.smallCategory AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory inclusion	—	CategoryTheory.WithInitial.instFaithfulIncl
instFullSimplexCategoryInclusion 📖	mathematical	—	CategoryTheory.Functor.Full SimplexCategory SimplexCategory.smallCategory AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory inclusion	—	CategoryTheory.WithInitial.instFullIncl
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory	—	CategoryTheory.WithInitial.instHasInitial

(root)

Definitions

Name	Category	Theorems
AugmentedSimplexCategory 📖	CompOp	67 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, AugmentedSimplexCategory.inr_comp_associator, AugmentedSimplexCategory.inclusion_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, AugmentedSimplexCategory.whiskerLeft_id_star, AugmentedSimplexCategory.inr_comp_inl_comp_associator, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.instHasInitial, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, AugmentedSimplexCategory.tensorObj_hom_ext_iff, AugmentedSimplexCategory.inr_comp_associator_assoc, AugmentedSimplexCategory.instFullSimplexCategoryInclusion, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.inl_comp_tensorHom, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.inl_comp_inl_comp_associator, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion, AugmentedSimplexCategory.tensor_id, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, AugmentedSimplexCategory.inclusion_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.id_tensorHom, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, AugmentedSimplexCategory.inr_comp_tensorHom, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, AugmentedSimplexCategory.inl_comp_tensorHom_assoc, AugmentedSimplexCategory.inr_comp_tensorHom_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, AugmentedSimplexCategory.tensorHom_comp_tensorHom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app

---

← Back to Index