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

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$$:

1. 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.
2. 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.

• These finite direct categories, will they naturally also have decidable equality of morphisms? (Also, $\mathbf{Ord}$ is not well-behaved constructively, so you should probably look at the other options first.) Sep 18 at 18:25
• The point of direct categories is almost always to be able to do proof by induction on height, so you really want this height function to ordinals to be available. The constructive theory of ordinal is a mess (By that I mean there are many non-equivalent definitions of ordinals), so if this is an option to you I would absolutely suggest to restrict to finite direct categories, so this height functions $h$ takes values in $\mathbb{N}$. This will indeed force identities to be decidable, as an arrow is an identity if and only if $h(t(f)) = h(s(f))$. Sep 18 at 18:56
• I should add that if the finite case is enough for you, then you probably should take finite to mean "finite and decidable", so that equality of arrows and objects are both decidable. If the finite-decidable case isn't enough, I would start by making a list of the properties you need for the application you have in mind and build the "correct" notion from there: there is going to be many non-equivalent definition possible and no reasons to prefer one over another in general Sep 18 at 19:08
• @SimonHenry I would have said that the point of direct categories is to do induction. It doesn't have to be induction on ordinals, so you don't need an ordinal-valued height; all you need is a well-founded relation to do well-founded induction. Sep 18 at 21:03
• I agree. The reason I said that is that I tend to think that defining the "height" is the sort of thing you should be able to do by induction. But given that it is higly dependent on which theory of ordinal you are using, I agree this isn't the all story. Sep 19 at 1:18

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

• @TobyBartels Indeed. But my point is that, in the sorts of applications we usually see of induction on direct categories, you can't prove that without knowing either that $f$ is an identity or that the source of $f$ is $<$ its target. Sep 21 at 16:12
• Let me try to be more explicit, to test my understanding of your answer, @MikeShulman. In order to define a $V$-valued presheaf $F: D^{\mathrm{op}} \to V$, for each $d \in \operatorname{Ob}(D)$, we (i) construct $F(d)$, (ii) construct $F(f)\colon F(d) \to F(d')$ for each $d' \in D$ and $f\colon d' \to d$, and (iii) prove $F(f\circ g) = F(g)\circ F(f)$ for each $d', d'' \in D$ and $g\colon d'' \to d'$ and $f\colon d'\to d$. If we do this by induction on $d \in D$, at the time we do (ii), we have only constructed $F(d')$ for $d' < d$ or $d = d'$ and we're stuck. Sep 21 at 16:25
• Accepted because I'm already convinced by this answer, and the acceptance would be undone anytime. I randomly thought that since the notion of well-ordered sets is all about $<$, not about $\le$, the correct categorification of that concept would be direct semicategories, not any concept of direct categories I defined in my question text. Maybe, the good point about (2) is that the condition is equivalent to direct semicategories and that it defines categories. Sep 22 at 22:05
• I agree -- the categorification of a well-ordered set should really be a direct semicategory, and if we really want a category then we have to make it one as in (2). This definition also covers all "well-ordered posets", because a " well-ordered poset" is not a poset in the usual sense of a reflexive relation $\le$, but defined in terms of an irreflexive relation $<$. It's true that many constructive "well-ordered posets", like Ord, also have a $\le$ that isn't defined as $(x<y)\vee (x=y)$, but this relation is irrelevant to the well-orderedness. Sep 23 at 18:27
• Interestingly, in the case of Ord, the relation $\le$ can be defined in terms of $<$ in a different way: $(y\le z) = \forall x. ((x<y) \to (x<z))$. I don't know whether that could be categorified; it feels a little bit like defining a "co-free" category generated by a semicategory. Sep 23 at 18:32

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.