Definition. Direct categories
A well-founded order is a set with a proposition-valued transitive relation admitting no infinite descent: every element is accessible. Write for .
A direct structure on a category over is a functor
into the well-founded order viewed as a poset category. The functor organizes two pieces of data at once: an ordering on the objects, and the invariant that morphisms respect it β forces .
A direct structure equips the objects with a well-founded strict relation
Intuitively, direct categories are the right generalization of well-foundedness to the categorical setting: a direct category is essentially one whose underlying graph is a directed acyclic graph, layered by degree, so that data at an object may be defined by recursion from data at all objects strictly below it.
The degrees order the objects, while the morphisms of say how an object sits over its predecessors.