dedekind::category::IsEmbeddingFunctor Concept Reference

A functor that is fully faithful + injective on objects (Mac Lane CWM §IV.4 strong reading; the Yoneda-embedding flavour). More...

Concept definition

template<typename F>
concept dedekind::category::IsEmbeddingFunctor = 
    IsArrow<F> && IsMonicArrow<F> && is_embedding_functor_v<F>

Detailed Description

A functor that is fully faithful + injective on objects (Mac Lane CWM §IV.4 strong reading; the Yoneda-embedding flavour).

Embeddings are monic in the categorical sense. This concept therefore mechanically requires IsMonicArrow as the textbook structural prerequisite (in addition to the engineer-asserted is_embedding_functor_v trait that pins the stronger fully-faithful + injective-on-objects claim). The trait is the engineer's commitment to the Mac Lane §IV.4 reading; the IsMonicArrow check is the mechanical verification that the arrow's monic registration is also in place.

Opt-in semantics (#641 review note): the type-system gate here is IsArrow + IsMonicArrow + the is_embedding_functor_v trait. It does not require IsShapedFunctor (which carries the container-flavoured Shape requirement, see functor__Two_Intuition_Pumps), so bare arrows can register as IsEmbeddingFunctor witnesses without first satisfying IsShapedFunctor. This is intentional: the carrier-lattice embed_*_*_ family are functors Set<source> → Set<codomain> at the Mac Lane §I.3 level, but they're presented in the codebase as bare arrows whose Domain/Codomain are the carriers, NOT reified small categories — so even the (Shape-free) textbook IsFunctor is false on them. The #633 superinterface split has now landed (IsFunctor = the Shape-free "arrow between small categories"; IsShapedFunctor refines it with Shape), so IsEmbeddingFunctor could be tightened to require IsFunctor once the remaining #633 step lands: reifying a carrier's arrows as a small category (giving the embedding Σ_cat / Τ_cat = Set<carrier> slots). Until then the is_embedding_functor_v trait stays the engineer's commitment to the reading.

Concrete witnesses (registered in :numbers and adjacent partitions): embed_𝔹_ℕ_ (bool ↪ Cardinality), embed_𝔹_𝕂3_ (bool ↪ Kleene::Ω), embed_uint_ℕ_ (unsigned ↪ Cardinality), embed_sint_ℤ_ (int ↪ SignedCardinality), embed_ℤ_ℚ (machine_integer ↪ Rational). Each is an arrow with IsMonicArrow / IsInjective + a registered is_embedding_functor_v specialisation pinning the functor-level structural claim.

Weaker reading variants (IsFaithfulFunctor only, IsFullFunctor only) can be added as separate concepts when a consumer earns them.