A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally exposes a type-level object map Shape and the action on arrows, F(f). More...

Concept definition

template<typename F>
concept dedekind::category::IsShapedFunctor =  IsFunctor<F> && requires {
  typename F::Σ_cat;
  typename F::Τ_cat;
  requires IsSmallCategory<typename F::Σ_cat>;
  requires IsSmallCategory<typename F::Τ_cat>;
 
  
  typename F::template Shape<int>;
} && requires(F f, typename F::Σ_cat::Arrow f_c) {
  
  { f(f_c >> f_c) } -> IsArrow;
 
  requires std::same_as<
      typename decltype(f(f_c))::Domain,
      typename F::template Shape<typename F::Σ_cat::Arrow::Domain>>;
 
  requires std::same_as<
      typename decltype(f(f_c))::Codomain,
      typename F::template Shape<typename F::Σ_cat::Arrow::Codomain>>;
 
  
  
  
  requires requires(typename F::Σ_cat::Arrow::Domain c) {
    
    { f(F::Σ_cat::id_c(c)) } -> IsArrow;
 
    requires std::same_as<
        typename decltype(f(F::Σ_cat::id_c(c)))::Domain,
        typename F::template Shape<typename F::Σ_cat::Arrow::Domain>>;
 
    requires std::same_as<
        typename decltype(f(F::Σ_cat::id_c(c)))::Codomain,
        typename F::template Shape<typename F::Σ_cat::Arrow::Domain>>;
  };
}

Detailed Description

A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally exposes a type-level object map Shape and the action on arrows, F(f).

Mapping: F(f: A->B) -> F(f): F(A)->F(B)
Identity Law: F(id_c) = id_{F(c)}
Composition Law: F(f >> g) = F(f) >> F(g)

Because IsSmallCategory in this project is single-species, the object witness for c is always recovered by first forming the identity arrow id_c(c). Functorial object mapping is therefore observed indirectly through the arrow F(id_c(c)), whose domain recovers the image object F(c).

IsShapedFunctor ⟹ IsFunctor (it opens with IsFunctor<F>). Canonical functor models provided in this partition are listed in IsFunctor_Models.