Module functor

Functors between categories.

Abstractly, a functor between categories is a just graph morphism between the underlying graphs that respects composition. In our applications, we are most interested in functors out of finitely generated categories, whose action on arbitrary morphisms is uniquely determined by that on the morphism generators. Thus, in contrast to mappings between sets and graphs, we generally cannot separate evaluation from validation: to evaluate a map on a finitely generated category, we might need access to the domain category, in order to decompose general morphisms into composites of generators, and also to the codomain category, in order to compose images of generating morphisms. The upshot is that you must carry around (references to) more data to evaluate functors than to evaluate functions or graph morphisms.

Structs

FpFunctor

A functor out of a finitely presented (f.p.) category.

FpFunctorData

The data of a functor out of a finitely presented (f.p.) category.

FpFunctorMorMap

Auxiliary struct for the morphism map of a functor out of an f.p. category.

Enums

InvalidFpFunctor

A failure of a map out of an f.p. category to be functorial.

Traits

CategoryMap

A mapping between categories.

FgCategoryMap

A mapping out of a finitely generated category.