One of Lawvere’s great insights was that it’s much easier to work with *properties* than it is to work with *structure*. Preorders are the type of category where morphisms are properties rather than structure, and so if it is possible to get away with a preorder instead of a category, there are some benefits.

Additionally, in a preorder the “product” (or “meet”) of two objects is the natural notion of “diff” between them. In a category, this is just the product, and hence not very interesting. But in a preorder this can tell you something about how the two objects are related.

The idea for this post happened through thinking about how to implement version control for finite sets, ala chit. In a traditional implementation of finite sets, a finite set is just a natural number. However, in chit a finite set is a finite subset A of the set of UUIDs (which we will identify with \mathbb{N}), along with an equivalence relation on A, which is represented by an idempotent function u_A : A \to A (a \sim_A a' iff u_A(a) = u_A(a')) (this would be implemented as a union-find data structure).

There is a natural preorder structure we can put on the collection of such (A,u_A). Namely, (A, u_A) \leq (B, u_B) if A \subseteq B and the following commutes:

In other words, u_B = u_B \circ u_A. Thus, if a \sim_A a' then a \sim_B a'.

It appears that this condition is quite strict, but in fact it is equivalent to to the inclusion preserving the equivalence relation. To see why, consider (\{1,2\}, - \mapsto 1) and (\{1,2\}, - \mapsto 2). Although these choose different representatives for their equivalence classes, it is the case that (\{1,2\}, - \mapsto 1) \cong (\{1,2\}, - \mapsto 2). More generally, if the inclusion preserves the equivalence relation, then u_A will take an element a of A to something in the same equivalence class in B, so u_B(a) = u_B(u_A(a)) as required.

We call the preorder of such pairs \mathsf{FinRep}, as each pair *represents* a finite set.

Now, there is a functor from \mathsf{FinRep} to \mathsf{FinSet} which sends each pair (A, u_A) to the set \mathrm{im}(u_A) \cong A/\sim, and sends an inclusion (A, u_A) \leq (B, u_B) to u_B|_{\mathrm{im}(u_A)} \colon \mathrm{im}(u_A) \to \mathrm{im}(u_B). Then we put a weak equivalence structure on \mathsf{FinRep} such that (A, u_A) \leq (B, u_B) is a weak equivalence iff it is sent to an isomorphism in \mathsf{FinSet}. This satisfies 2-out-of-6 because the isomorphisms in \mathsf{FinSet} satisfy 2-out-of-6, so this makes \mathsf{FinRep} into a homotopical category.

Let us now investigate finite limits and colimits in \mathsf{FinRep}. It has an initial object, i.e. the empty set, but no terminal object because we only allow finite sets. We now investigate meets (i.e. products). The meet of (A, u_A) and (B, u_B) is A \cap B along with any choice of representatives for the equivalence relation of x \sim_{A \cap B} y iff x \sim_A y and x \sim_B y. Likewise, the join of (A, u_A) and (B, u_B) is A \cup B with the equivalence relation generated by \sim_A and \sim_B. Hopefully there is an efficient algorithm for computing both meets and joins.

Note that the functor \mathsf{FinRep} \to \mathsf{FinSet} is *not* continuous or cocontinuous. We can think of limits/colimits in \mathsf{FinSet} as being in “general position” somehow. I.e., in general A \cap B = \emptyset, and then A \sqcup B = A \cup B. The “general position” for product is taking the join of (A \times B, (a,b) \sim (a, b')), (A \times B, (a,b) \sim (a',b)), which is A \times B with the trivial equivalence relation.

We now investigate the homotopy category of \mathsf{FinRep}. Here I am on very weak ground because I don’t have a lot of experience with categorical homotopy theory, but I will attempt to sketch some ideas.

First of all, the functor \mathsf{FinRep} \to \mathsf{FinSet} is essentially surjective, faithful, and the only maps that get sent to isomorphisms are weak equivalences, by definition. I’m pretty sure this should imply that \mathsf{FinSet} is the homotopy category of \mathsf{FinRep}.

Another way of getting at this would be to consider the category of cospans in \mathsf{FinRep} whose right leg is a weak equivalence, composed by pushout (i.e. meet),

and quotiented by the equivalence relation generated by diagrams of the form

Note that the middle arrow must be a weak equivalence by 2-out-of-3. Call this category \mathrm{WCsp}(\mathsf{FinRep}).

I thought I could get an equivalence \mathsf{FinSet} \cong \mathrm{WCsp}(\mathsf{FinRep}), but something seems to go wrong. Here was my attempt: let’s see if anyone can fix it.

Let \mathbb{F} be a skeleton of \mathsf{FinSet}, whose objects are identified with \mathbb{N}. Then pick an injective function \langle -, -\rangle \colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}, and define a functor F \colon \mathbb{F} \to \mathrm{WCsp}(\mathsf{FinRep}) in the following way. Send n \in \mathbb{F} to F(n) = \{\langle n, 1 \rangle, \ldots, \langle n, n \rangle\}, and send f \colon n \to m to the cospan

This makes sense… except for the case n = m when the right injection fails to be a weak equivalence. In fact, there seem to be no non-identity endomorphisms in \mathrm{WCsp}(\mathsf{FinRep}), which makes it unlikely in my mind that \mathrm{WCsp}(\mathsf{FinRep}) would be the homotopy category of \mathsf{FinRep}.

So I’m not exactly sure where to go from here. I hope the basic idea is clear enough that someone who knows more homotopy theory could give me some guidance.