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

deg:π’žοΈ€β†’(𝐷,≀)

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 degπ‘₯≀deg𝑦.

A direct structure equips the objects with a well-founded strict relation

π‘₯β‰Ίπ‘¦βŸΊdegπ‘₯<deg𝑦.

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.

direct-category definition entries/category/direct-category.hel