Module fp_category

Finitely presented categories.

A finitely presented category, or f.p. category for short, is a finite graph together with a finite set of path equations. This data defines a category whose objects are the vertices of the graph and morphisms are paths in the graphs, regarded as equivalent under the congruence relation generated by the path equations. For a detailed description of this congruence relation, see (Spivak 2014, Definition 4.5.2.3).

In general, this congruence relation—the word problem for finitely presented categories—cannot be decided, though in practice it often can be. The data structure in this module uses e-graphs to check for equivalence of paths under the congruence.

Structs

FpCategory

A finitely presented category backed by an e-graph.

Enums

InvalidFpCategory

A failure of a finite presentation of a category to be well defined.

Type Aliases

UstrFpCategory

A finitely presented category with generators of type Ustr.