dedekind::category::IsLocallySmallCategory Concept Reference

Value-level locally-small witness: the Hom-collection of Cat is a set in the metatheory. More...

Concept definition

template<typename Cat>
concept dedekind::category::IsLocallySmallCategory =  requires {
  
  
  typename Cat::Arrow;
  
  
  
  requires IsArrow<typename Cat::Arrow>;
}

Detailed Description

Value-level locally-small witness: the Hom-collection of Cat is a set in the metatheory.

Forced by representing arrows as values of a single C++ type Cat::Arrow — a C++ type's value-set is a set (not a proper class), so the total arrow-collection is a set; for any fixed pair of objects (a, b), Hom_Cat(a, b) is the subset of Cat::Arrow values with Dom = a and Cod = b, hence itself a set (subset of a set).

This is the value-level reading of "locally small". The higher-kinded reading — where objects are a proper class and Hom<A, B> is exposed as a type-level slot — is deliberately not navigated by the project (cf. small__The_Locally_Small_Slot below).

small__LocallySmall_Implies_Small

IsSmallCategory = IsLocallySmallCategory + Ob-is-a-set, so any IsSmallCategory carrier is automatically IsLocallySmallCategory; the conjunction "small @b and locally small" is structurally equivalent to IsSmallCategory in this encoding. Paper §2.3 step 1 cites IsSmallCategory as the concept that enforces both readings.

Note

U : 𝒞 → Set ∧ faithful(U) ⟹ ∀ a, b ∈ Ob(𝒞). Hom_𝒞(a, b) ↣ U(b)^U(a) ∈ Ob(Set) ⟹ 𝒞 ∈ Ob(LocSmall).

∴ Concrete ⊆ LocSmall.

[Trans: "Concreteness gives locally-smallness for free: a faithful forgetful @c U @c : @c 𝒞 @c → @c Set monically injects each Hom-set of @c 𝒞 into a function-set of @c Set, and a subset of a set is a set."] — Claude (Anthropic AI assistant), conversation log, PR #639 review (2026-05-10).