Categorical doctrines
CAP defines and allows defining hierarchies of categorical doctrines, some of which are well-known, others are less known, or even new. There are several CAP-based packages that define various categorical doctrines:
doctrine (either selfdual doctrine or doctrine / dual doctrine ) |
package |
|---|---|
IsEnrichedOverCommutativeRegularSemigroup |
CAP |
IsAbCategory |
CAP |
IsCategoryWithTerminalObject / IsCategoryWithInitialObject |
CAP |
IsCartesianCategory / IsCocartesianCategory |
CartesianCategories |
IsBicartesianCategory |
CartesianCategories |
IsCategoryWithZeroObject |
CAP |
IsAdditiveCategory |
CAP |
IsCategoryWithCoequalizers / IsCategoryWithEqualizers |
CAP |
IsFiniteCocompleteCategory / IsFiniteCompleteCategory |
CartesianCategories |
IsFiniteBicompleteCategory |
CartesianCategories |
IsPreAbelianCategory |
CAP |
IsAbelianCategory |
CAP |
IsAbelianCategoryWithEnoughInjectives / IsAbelianCategoryWithEnoughProjectives |
CAP |
IsCartesianClosedCategory / IsCocartesianCoclosedCategory |
CartesianCategories |
IsDistributiveCategory / IsCodistributiveCategory |
CartesianCategories |
IsBicartesianClosedCategory / IsBicartesianCoclosedCategory |
CartesianCategories |
IsThinCategory |
Locales |
IsCartesianProset / IsCocartesianProset |
Locales |
IsBicartesianProset |
Locales |
IsDistributiveBicartesianProset |
Locales |
IsCoHeytingAlgebroid / IsHeytingAlgebroid |
Locales |
IsBiHeytingAlgebroid |
Locales |
IsPosetCategory |
Locales |
IsJoinSemiLattice / IsMeetSemiLattice |
Locales |
IsLattice |
Locales |
IsDistributiveLattice |
Locales |
IsCoHeytingAlgebra / IsHeytingAlgebra |
Locales |
IsBiHeytingAlgebra |
Locales |
IsBooleanAlgebroid |
Locales |
IsBooleanAlgebra |
Locales |
IsMonoidalCategory |
MonoidalCategories |
IsSymmetricMonoidalCategory |
MonoidalCategories |
IsCategoryWithDecidableColifts / IsCategoryWithDecidableLifts |
CAP |
IsClosedMonoidalCategory / IsCoclosedMonoidalCategory |
MonoidalCategories |
IsMonoidalProset |
Locales |
IsClosedMonoidalProset / IsCoclosedMonoidalProset |
Locales |
IsMonoidalPoset |
Locales |
IsClosedMonoidalPoset / IsCoclosedMonoidalPoset |
Locales |
IsMonoidalLattice |
Locales |
IsClosedMonoidalLattice / IsCoclosedMonoidalLattice |
Locales |
IsElementaryTopos / not supported yet |
Toposes |
IsEquippedWithHomomorphismStructure |
CAP |
IsObjectFiniteCategory |
ToolsForCategoricalTowers |
IsFinitelyPresentedCategory |
FpCategories |
IsFiniteCategory |
ToolsForCategoricalTowers |
IsLeftClosedMonoidalCategory / IsLeftCoclosedMonoidalCategory |
MonoidalCategories |
IsLinearCategoryOverCommutativeRing |
CAP |
IsLinearCategoryOverCommutativeRingWithFinitelyGeneratedFreeExternalHoms |
CAP |
IsSymmetricClosedMonoidalCategory / IsSymmetricCoclosedMonoidalCategory |
MonoidalCategories |
IsRigidSymmetricClosedMonoidalCategory / IsRigidSymmetricCoclosedMonoidalCategory |
MonoidalCategories |
IsSymmetricMonoidalProset |
Locales |
IsSymmetricClosedMonoidalProset / IsSymmetricCoclosedMonoidalProset |
Locales |
IsSymmetricMonoidalPoset |
Locales |
IsSymmetricClosedMonoidalPoset / IsSymmetricCoclosedMonoidalPoset |
Locales |
IsSymmetricMonoidalLattice |
Locales |
IsSymmetricClosedMonoidalLattice / IsSymmetricCoclosedMonoidalLattice |
Locales |
IsTriangulatedCategory1 |
TriangulatedCategories |
1 “triangulated category” is strictly speaking not a doctrine due to the nonfunctoriality of the cone. ↩