dedekind::category::IsFunctor Concept Reference

The textbook functor (#633): an IsArrow whose Domain and Codomain are (small) categories — a 1-morphism in Cat, Mac Lane §I.3 — carrying a morphism map. More...

Concept definition

template<typename F>
concept dedekind::category::IsFunctor = 
    IsArrow<F> && IsSmallCategory<Dom<F>> && IsSmallCategory<Cod<F>> &&
    requires(const F& f, typename Dom<F>::Arrow a) {
      
      
      
      { f(a) } -> IsArrow;
    } && is_functorial_v<F>

Detailed Description

The textbook functor (#633): an IsArrow whose Domain and Codomain are (small) categories — a 1-morphism in Cat, Mac Lane §I.3 — carrying a morphism map.

This is the superinterface extracted from IsShapedFunctor: it drops the container-flavoured Shape object map but keeps the categorical signature \(F\colon\Sigma\to\mathrm{T}\) (with IsSmallCategory Domain and Codomain) and the morphism action, required as the call on an arrow, F(f), beside the call on the source category, its action on objects, as the textbook writes both. IsShapedFunctor (the type-constructor functor: maybe_functor, tuple_functor, complex-/dual-style functors) refines it with Shape, so IsShapedFunctor ⟹ IsFunctor by construction. Functor variance branches off IsFunctor directly.

Note

What does not land here yet: the carrier-lattice embed_*_*_ family are functors Set<source> → Set<codomain> at the Mac Lane §I.3 level, but are presented as bare arrows whose Domain/Codomain are the carriers (e.g. QuadraticReal<2>, Complex<R>), NOT reified small categories — so IsFunctor is false on them. The is_embedding_functor_v trait remains the bridge; reifying the carriers' arrows as a small category (so an embedding \(A\hookrightarrow C\langle A \rangle\) satisfies IsFunctor directly) is the remaining #633 step.