dedekind::category::IsConcrete Concept Reference

A small category C is concrete when its objects are themselves sets — equivalently, when there is a faithful functor U : C → Set. More...

Concept definition

template<typename C>
concept dedekind::category::IsConcrete =  IsSmallCategory<C> && IsSpecies<typename C::Species>

Detailed Description

A small category C is concrete when its objects are themselves sets — equivalently, when there is a faithful functor U : C → Set.

Concept-as-predicate / &&-as-set-intersection framing: IsConcrete narrows IsSmallCategory by intersecting with the constraint that the category's object-collection is set-shaped (its Species type is registered in the species atlas). In the project's Juliet posture, where Species is a C++ type whose values are the objects, registration in the species atlas (via SpeciesTraits) is exactly the structural witness that those objects can be viewed as elements of Set.

Position in the size-and-structure lattice (read top-down as narrowing intersections; cf. paper §2.3):

IsSmallCategory<C>
  ∧ IsSpecies<C::Species>   (objects sit in the species atlas)
= IsConcrete<C>

     @c :etcs further narrows by adding the full topos / ETCS axiom
     surface (subobject classifier, NNO, choice, ...): @c IsSet =
     @c IsConcrete + ETCS axioms.

     Examples in the project:
       - @c Set<T> --- the canonical CCC in @c :cartesian; concrete
         for any @c T that satisfies @c IsSpecies (the @c :species
         primary registers integral / floating-point / bool types;
         other types opt in via explicit @c SpeciesTraits
         specialisations).
       - @c DiscreteCategory<S> in @c :discrete --- concrete when
         @c S is a registered species.