dedekind::category::IsDiscreteCategory Concept Reference

Concept definition

template<typename Cat>
concept dedekind::category::IsDiscreteCategory = 
    IsSmallCategory<Cat> && std::same_as<typename Cat::Arrow, typename Cat::Id>

Detailed Description

discrete__Discrete_Categories

A Discrete Category is a Small Category where the only morphisms are identities.

discrete__Set_to_Cat_Embedding

The discrete-category construction realises the canonical embedding Set ↪ Cat: every set S lifts to the discrete category Disc(S) whose objects are the elements of S and whose only arrows are identities. In categorical terms, Disc is the (unique up to natural iso) left adjoint to the underlying-objects functor U : Cat → Set; the adjunction Disc ⊣ U is the textbook spelling of "every set IS a discrete category". The DiscreteCategory<T> realisation below witnesses the lift on primitive carrier types; a generic IsSet-aware lift for the project's set DSL is tracked as a follow-up (the IsSet concept lives in category:etcs but the DSL sets live further downstream, so a lift-aware partition would have to live downstream of both).