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 |
|---|---|
IsInitialCategory |
CartesianCategories |
IsTerminalCategory |
CAP |
IsEquippedWithHomomorphismStructure |
CAP |
IsCategoryWithDecidableLifts / IsCategoryWithDecidableColifts |
CAP |
IsEnrichedOverCommutativeRegularSemigroup |
CAP |
IsLinearCategoryOverCommutativeRing |
CAP |
IsSkeletalCategory |
CAP |
IsAbCategory |
CAP |
IsAdditiveCategory |
CAP |
IsPreAbelianCategory |
CAP |
IsAbelianCategory |
CAP |
IsAbelianCategoryWithEnoughProjectives / IsAbelianCategoryWithEnoughInjectives |
CAP |
IsLocallyOfFiniteProjectiveDimension / IsLocallyOfFiniteInjectiveDimension |
CAP |
IsCartesianCategory / IsCocartesianCategory |
CartesianCategories |
IsStrictCartesianCategory / IsStrictCocartesianCategory |
CartesianCategories |
IsBicartesianCategory |
CartesianCategories |
IsDistributiveCategory / IsCodistributiveCategory |
CartesianCategories |
IsCartesianClosedCategory / IsCocartesianCoclosedCategory |
CartesianCategories |
IsBicartesianClosedCategory / IsBicartesianCoclosedCategory |
CartesianCategories |
IsFiniteCompleteCategory / IsFiniteCocompleteCategory |
CartesianCategories |
IsMonoidalCategory |
MonoidalCategories |
IsStrictMonoidalCategory |
MonoidalCategories |
IsBraidedMonoidalCategory |
MonoidalCategories |
IsSymmetricMonoidalCategory |
MonoidalCategories |
IsClosedMonoidalCategory / IsCoclosedMonoidalCategory |
MonoidalCategories |
IsSymmetricClosedMonoidalCategory / IsSymmetricCoclosedMonoidalCategory |
MonoidalCategories |
IsRigidSymmetricClosedMonoidalCategory / IsRigidSymmetricCoclosedMonoidalCategory |
MonoidalCategories |
IsFinitelyPresentedCategory |
FpCategories |
IsFinitelyPresentedLinearCategory |
Algebroids |
IsLinearClosureOfACategory |
Algebroids |
IsThinCategory |
Locales |
IsDiscreteCategory |
Locales |
IsMonoidalProset |
Locales |
IsClosedMonoidalProset / IsCoclosedMonoidalProset |
Locales |
IsCartesianProset / IsCocartesianProset |
Locales |
IsBicartesianProset |
Locales |
IsDistributiveBicartesianProset |
Locales |
IsHeytingAlgebroid / IsCoHeytingAlgebroid |
Locales |
IsBiHeytingAlgebroid |
Locales |
IsBooleanAlgebroid |
Locales |
IsPosetCategory |
Locales |
IsMonoidalPoset |
Locales |
IsClosedMonoidalPoset / IsCoclosedMonoidalPoset |
Locales |
IsMeetSemiLattice / IsJoinSemiLattice |
Locales |
IsLattice / IsLattice |
Locales |
IsDistributiveLattice / IsDistributiveLattice |
Locales |
IsMonoidalLattice / IsMonoidalLattice |
Locales |
IsClosedMonoidalLattice / IsCoclosedMonoidalLattice |
Locales |
IsHeytingAlgebra / IsCoHeytingAlgebra |
Locales |
IsBiHeytingAlgebra / IsBiHeytingAlgebra |
Locales |
IsTotalOrderCategory / IsTotalOrderCategory |
Locales |
IsBooleanAlgebra / IsBooleanAlgebra |
Locales |
IsStableProset / not supported yet |
Locales |
IsElementaryTopos / not supported yet |
Toposes |
IsTriangulatedCategory1 |
TriangulatedCategories |
1 “triangulated category” is strictly speaking not a doctrine due to the nonfunctoriality of the cone. ↩