I'm wondering what the legit definition of direct categories should be in constructive mathematics. I must admit I don't even know in what literature I should look for the definition. I would appreciate any assistance you can provide.

Let $D$ be a quiver (a category without identities or compositions -- i.e. directed graph). For the purpose of this question, we say $D$ is a *direct* quiver if it satisfies the following equivalent conditions:

- For any objects $x, y \in \operatorname{Ob}(D)$, write $x < y$ if there is a morphism $x \to y$. Then $<$ is a well-founded relation on $\operatorname{Ob}(D)$.
- There exists a function $d\colon \operatorname{Ob}(D) \to \mathrm{Ord}$, where $\mathrm{Ord}$ is the class of all ordinals, satisfying $d(x) < d(y)$ for each morphism $x \to y$.
- There exist a set (or class if $D$ is permitted to be large) $W$, a well-order $<$ on $W$, and a function $d\colon \operatorname{Ob}(D) \to W$ satisfying $d(x) < d(y)$ for each morphism $x\to y$.

If $D$ is a semicategory (i.e. a quiver equipped with associative compositions or a category without the assumption of identities), we consider $D$ to be a *direct* semicategory if $D$ is a direct quiver.

My question is: which of the following, or what else, is (or should be) conventionally used as a *constructive* definition of direct categories? Let $D$ be a category.

- We say $D$ is direct if the quiver obtained by removing all the identity morphisms from $D$ is direct.
- We say $D$ is direct if it is obtained by freely adjoining identities to a direct semicategory.
- (Vague) We say $D$ is direct if the "wide" subquiver of $D$ spanned by all the morphisms distinguished from identities is direct. Here, the distinction of a morphism from identities should be separately defined; it could be an apartness relation satisfying some conditions, but there could be something better.

Conditions 1 and 2 are different in that Condition 2 implies the dichotomy of whether a morphism is identity or not, while Condition 1 doesn't. Which definition should be adopted when referring to direct categories?

My confusion began when I looked up nlab for the definition of direct categories. According to the nlab article for direct category, the followings are both equivalent conditions for the directness of $D$:

- There exists a function $d\colon \operatorname{Ob}(D)\to\mathrm{Ord}$, where $\mathrm{Ord}$ is the class of ordinals, such that every nonidentity morphism of $D$ raises the degree.
- There exists an identity-reflecting functor (that is, it maps a morphism to an identity if and only if the morphism is itself an identity) $d\colon D\to\mathbf{Ord}$, where $\mathbf{Ord}$ is the large poset of ordinals viewed as a category.

Condition 4 is equivalent to Condition 1. Condition 5 needs clarification in the definition of the category $\mathbf{Ord}$, but I guess it is equivalent to the condition 2. In order for the condition 5 to work, the non-identity part of the category $\mathbf{Ord}$ should itself be a well-ordered class. In constructive setting, $x < y \overset{\mathrm{def}}{\iff} x \subsetneq y$ cannot be shown to be a well-order; it should be $x < y \overset{\mathrm{def}}{\iff} x \in y$. If you make it a reflexive poset, the only sensible choice I can think of is $x \leq y \overset{\mathrm{def}}{\iff} x = y \mathrel\vee x \in y$. From this rather unnatural construction of the category $\mathbf{Ord}$, Condition 5 is shown to be equivalent to Condition 2.

We could do inductive argument on $\operatorname{Ob}(D)$ solely with Condition 1, but the dichotomy from Condition 2 is quite useful. The prototypical direct category $\mathbf{Ord}$ in Condition 5 satisfies Condition 2; therefore the additional assumption in Condition 2 might not be too strong, but I'm not sure at all. Furthermore, if you go on to the Reedy category theory along the line of Condition 2, it would demand that the degree-lowering/degree-raising part of the Reedy category should be decidable subsets of the collection of all morphisms, which sounds too strict, but again I'm not sure (I'm just saying it "sounds" strict, I don't know how to test if the definition is too strong).

I'm not familiar with constructive mathematics. In fact, I just need a good definition to write in my paper. It will use *finite* direct categories for syntactical matters. I say a category/semicategory/quiver $C$ is finite if there exists a pair of natural numbers $m,n$ and bijections $\operatorname{Ob}(C)\cong \left\{0,1,\ldots,m-1\right\}$ and $\operatorname{Mor}(C)\cong\left\{0,1,\ldots,n-1\right\}$. In this case, the equalities of morphisms and objects are decidable and hence the distinction between Conditions 1 and 2 vanishes. I just thought I would be better if I can keep my argument within finitism and at the same time discuss with decent generality where finiteness is unnecessary. I'd find any literature and explanation helpful.

17more comments