dedekind::category::IsSmallCategory Concept Reference

A point-free, morphism-only reification of a Category. More...

Concept definition

template<typename Cat>
concept dedekind::category::IsSmallCategory =  IsLocallySmallCategory<Cat> && requires {
  
  typename Cat::Species;
  
  
  
  requires std::same_as<typename Cat::Species, Dom<typename Cat::Arrow>>;
 
  
  typename Cat::Id;
  requires IsArrow<typename Cat::Id>;
  requires std::convertible_to<typename Cat::Id, typename Cat::Arrow>;
 
  
  requires requires(typename Cat::Species x) {
    { Cat::id_c(x) } -> std::same_as<typename Cat::Id>;
  };
 
  
  requires requires(typename Cat::Arrow f, typename Cat::Arrow g) {
    { f >> g } -> IsArrow;
    
    
    requires std::same_as<Dom<decltype(f >> g)>, Dom<typename Cat::Arrow>>;
    requires std::same_as<Cod<decltype(f >> g)>, Cod<typename Cat::Arrow>>;
  };
 
  
}

Detailed Description

A point-free, morphism-only reification of a Category.

In this structuralist approach, we bypass the traditional object-morphism dichotomy. A category is defined solely by its arrows and their composition laws. Objects are not distinct entities but are identified with their identity morphisms (Id). This "singly-typed" view allows functors and natural transformations to be treated as arrows within higher-dimensional structures.

In this codebase we use a further specialization: a category fixes a single Species type, and Cat::Arrow::Domain is required to coincide with that object label type. This is stricter than the textbook many-object view, and it gives a canonical type-/label-level representative of an object via the identity arrow Cat::id_c(x), allowing object-level reasoning to be re-entered through composition. Recovering the original value-level label x from that identity arrow, however, is not required by IsSmallCategory; that would need an additional guarantee that identity arrows carry or expose such a witness.

small__What_Smallness_Pins

In CT jargon, IsSmallCategory pins exactly the smallness reading of "small category" — the cardinality reading: the collection of objects (the value-set of Species) and the collection of arrows (the value-set of Arrow) are each sets in the metatheory. This is forced by representing both as C++ types: a C++ type's values form a set (not a proper class), so Ob(𝒞) and the total Hom-collection are sets.

IsSmallCategory deliberately does not pin the second, ontological reading of "small" — concreteness — under which each object is itself a set (equivalently: there is a faithful forgetful functor U : 𝒞 → Set). Whether each object is a set or a tag depends on what Species is bound to at the call site (Set<T> binds to sets; an enum-style Species binds to tags). Concreteness as a structural commitment is layered downstream in :concrete — IsConcrete<C> = IsSmallCategory<C> ∧ IsSpecies<C::Species> — and further refined in :etcs, whose ETCS axiomatization picks out Set specifically among concrete categories via the topos structure (well-pointedness, NNO, choice).

Other refinements of "category" — discrete, locally-finite, intensional / extensional, lazy / strict — are also intentionally out of scope here; they are named (or named-able) at downstream partitions where they have semantic content. The intensional / extensional split in particular is reified at :sets:expressions (intensional, Kleene) vs :sets:extensional (decidable membership), not at the category layer. Thin categories (hom(a, b) has ≤ 1 morphism — the categorical incarnation of preorders) were lifted from this Sollbruchstelle to their own partition :category::thin in #698, where they sit as row 1 of the lattice Form-chain (IsThinCategory ⊂ IsPosetal ⊂ IsLatticeCategory).

small__The_Locally_Small_Slot

Standard CT distinguishes three slots along the size axis:

Concept	Object collection	Hom-sets
(general) category	proper class	proper class
locally small category	proper class	sets
small category	set	sets

IsSmallCategory pins the third row (small). The locally small row above it is named at the value level by the new IsLocallySmallCategory concept (defined below): when Cat::Arrow is a single C++ type, its value-set is a set in the metatheory, hence the total Hom-collection is a set and so is every Hom_Cat(a, b) (a subset). In the project's value-level encoding, IsSmallCategory = IsLocallySmallCategory + Ob-is-a-set; small implies locally small, making "small @b and locally small" a structurally equivalent gate to IsSmallCategory.

What remains deferred is the higher-kinded reading of locally- small-not-small — the textbook home of Set itself, Cpp, Top, Alg(Σ), where the object-collection is a proper class and Hom<A, B> must be exposed as a type-level slot. Two reasons to defer:

1. No current consumer. No site in the project today requires a category whose object-collection is type-level (a proper class). The slot would be speculative API, and the project's struct-creation posture is "burden of proof on adding a concept, not on omitting one".
2. Implementation cost. A faithful higher-kinded locally- small concept requires a Cat::template Hom<A, B> slot, which is the same template-template territory the codebase otherwise tries to keep at arm's length (in the IsShapedFunctor Shape pattern, etc.). Paying that complexity without a load-bearing consumer would be the wrong trade.

If a future slice introduces an honest Cpp-as-category or Alg(Σ)-as-category construction, that's the natural moment to lift IsLocallySmallCategory from its value-level form to the higher-kinded slot — with a real consumer to pressure-test the API shape rather than guessing it ahead of time.

Axioms:

1. Existence: For every arrow f, there exist unique identity arrows id_dom(f) and id_cod(f).
2. Composition: If cod(f) == dom(g), then f >> g exists.
3. Unitary: id_dom(f) >> f = f = f >> id_cod(f).