In the constructive theory of direct categories, is it decidable whether an arbitrary morphism is an identity or not?

Question

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.

1. We say $D$ is direct if the quiver obtained by removing all the identity morphisms from $D$ is direct.
2. We say $D$ is direct if it is obtained by freely adjoining identities to a direct semicategory.
3. (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$:

4. 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.
5. 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.

Answer 1

I believe (2) is the best definition. Consider what you want to do with a direct category: you want to construct presheaves and natural transformations between them inductively, assuming that they are already constructed for all $x<y$ and then constructing them for $y$. But then you have to construct them (or prove them to be natural) for all morphisms too. Your inductive hypothesis shows you how to deal with morphisms that strictly raise degree, and of course you can deal with identities; but if you don't know that all morphisms fall into one of these two classes (which is what (2) tells you), for a general morphism you are stuck.

My preprint Reedy categories and their generalizations includes a definition of direct categories (or their opposites, inverse categories) as those obtained from the empty category by successively taking collages along profunctors to discrete sets. Since a collage has decidable identities on the newly added objects, this should be constructively equivalent to definition (2). This definition is also nicely adapted to inductive constructions, as shown in the paper.

Answer 2

To ask whether it is decidable if a morphism is an identity is the wrong question here. In any more general setting the answer to this ought to be "no", however, here we don't have any non-identity automorphisms. Thus, the actual question is:

Is equality of objects decidable?

The answer to this will depend on where your directed categories are coming from and what you want to do with them. If you are in a setting where equality of objects is not decidable, you probably should work with the quiver+composition instead of the directed category (just like partial orders tend to work a bit nicer than quasiorders without decidable equality).

What needs more caution is, as Simon Henry points out, how to handle the well-foundedness.