concrete.cppm File Reference

Concrete categories: faithful U : 𝒞 → Set, sub-object machinery, lattice operations on χ-classified sets. More...

#include <concepts>
#include <type_traits>
#include <utility>
import dedekind.category:species;

Include dependency graph for concrete.cppm:

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::SetAsProduct
	Set := (Underlying, Classifier) read as a product, in the projection-access sense.
concept	dedekind::category::IsConcrete
	A small category C is concrete when its objects are themselves sets — equivalently, when there is a faithful functor U : C → Set.
concept	dedekind::category::HasTernarySupport
	True when a set object's classifier returns ternary truth values.
concept	dedekind::category::IsCompatibleSetPair
	Two set objects over the same ambient species and same Ω codomain.

Functions
template<typename S> requires IsSubobject<S, typename S::Domain>
constexpr auto	dedekind::category::in (const typename S::Domain &x, const S &s)
	Membership: x ∈ S evaluated via S's structural call (the carrier IS the characteristic morphism).
template<typename S, IsArrow E> requires IsSubobject<S, typename S::Domain> && std::same_as<Cod<E>, typename S::Domain>
constexpr auto	dedekind::category::in_via (const Dom< E > &x, E embedding, const S &s)
	Membership through an embedding arrow e:X→A, then the carrier-as-predicate: x ∈_e S = s(e(x)).
template<IsArrow F, IsArrow G> requires std::same_as<Cod<std::decay_t<F>>, Dom<std::decay_t<G>>>
constexpr auto	dedekind::category::compose_embedding (F f, G g)
	Compose two embedding arrows for pullback naturality path checks.

Detailed Description

Concrete categories: faithful U : 𝒞 → Set, sub-object machinery, lattice operations on χ-classified sets.

@partition :concrete

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

concrete__What_Concreteness_Pins

A category 𝒞 is concrete (in the textbook sense; Mac Lane CWM §IV.6, Pierce §1.6, Awodey ch 6) when there is a faithful functor U : 𝒞 → Set, i.e. each object is a set and each arrow is a set-function preserving the relevant structure. This is the ontological reading of "small category" (every object is a set), complementing the cardinality reading pinned by :small (the object-collection and Hom-collection are themselves sets).

The two readings are independent (Reading 1 / Reading 2 in the :small docstring; cf. paper §2.3):

• Small but not concrete: 𝟚 (the two-arrow category), finite-state- machines-as-categories, posetal categories with abstract tag objects.
• Concrete but not small: Set itself, Grp, Alg(Σ), Top.

:concrete sits between :small and :etcs on the chain Cat → Ddk: IsSmallCategory pins the size axis; IsConcrete pins the concreteness axis (objects are sets); :etcs further axiomatises which concrete category is Set itself via the topos structure (well-pointedness, NNO, choice, ...). :etcs imports :concrete and treats it as the prerequisite layer.

concrete__Std_Namespace_Mappings

• IsSubobject<S, A>: per-object concreteness — S is a Subobject of ambient A.
• IsConcrete<C>: per-category concreteness — C is small AND its objects are sets.
• IsCompatibleSetPair / HasTernarySupport: subobject-pair shape gates.
• in / in_via: membership x ∈ S via χ-evaluation s(x).
• compose_embedding: compose two embedding arrows (pullback path checks).

Membership (in / in_via) is χ-evaluation, category-fundamental, so it lives here. The set-LATTICE operations are the operators operator& / | / ! in dedekind.sets, where the set-builder DSL lives.

Concept-as-predicate framing (cf. #635, #637). The chain ranges over CATEGORIES C: among small categories, the concrete ones (a faithful U: C→Set) contain the category Set itself (all 10 ETCS axioms).

IsSmallCategory<C>      ⊇    IsConcrete<C>      ⊇    C = Set (ETCS)
(size axis: small)        (concreteness)         (full ETCS axiomatisation)

Warning

This is not IsSet ⟹ IsSmallCategory . The concept IsSet is a predicate on a set OBJECT A, not on a category: an individual set is an object of Set (Lawvere), a category only via the discrete embedding Disc: Set ↪ Cat. IsSet requires the categorical axioms of CanonicalSetCCC<A::Domain> (the Set-witness over the carrier), never IsSmallCategory .

Note

"A set is a Many that allows itself to be thought of as a One." — Georg Cantor, letter to Richard Dedekind (1899)