Define the **distributive lattice cube category** or **Dedekind cube category** $\square_{\land\lor}$ to be the full subcategory of the category of posets and monotone maps consisting of objects of the form $[1]^n \triangleq \{0 < 1\}^n$ for $n \ge 0$. Morphisms $[1]^m \to [1]^n$ in this category correspond to $n$-tuples of terms in $m$ variables in the theory of bounded distributive lattices, hence the name. (In terms of generators, every morphism can be written as a composite of face maps, degeneracies, permutations, diagonals, and min- and max-connections─this fact appears on the logical side as the disjunctive/conjunctive normal form presentations.)

The presheaf category $\mathrm{PSh}(\square_{\land\lor})$ is then one of many variations on "cubical sets". I'd like to know whether the following finiteness property is satisfied by the representable cubes in this category:

**Question**: In the presheaf category $\mathrm{PSh}(\square_{\land\lor})$, does every representable object have finitely many subobjects up to isomorphism? Equivalently, are there finitely many sieves on every object of $\square_{\land\lor}$?

In general, say that a category $\mathcal{C}$ has the **finite sieve property** if there are finitely many sieves on each object of $\mathcal{C}$. Recall that a sieve on an object $A$ in category $\mathcal{C}$ is a set $\mathcal{S}$ of arrows into $A$ such that if $g : B \to A$ is in $\mathcal{S}$ and $f : C \to B$ is an arbitrary arrow, then $g \circ f$ is in $\mathcal{S}$. To show that the set of sieves on some $A$ is finite, it suffices to show there are finitely many *principal sieves*, that is, sieves of the form $\langle g \rangle \triangleq \{g \circ f \mid f : C \to B\}$ for some $g : B \to A$. Using this and some specifics of $\square_{\land\lor}$, we can thus give the following more concrete reformulations:

**Equivalent Question**: Fix $k \ge 0$. Does there exist $\ell \ge 0$ such that every $f : [1]^n \to [1]^k$ generates the same principal sieve as some $f' : [1]^\ell \to [1]^k$?

**Equivalent Question 2**: Fix $k \ge 0$. Does there exist $\ell \ge 0$ such that for every $f : [1]^n \to [1]^k$, there are maps $[1]^n \overset{g}\to [1]^\ell \overset{h}\to [1]^n$ with $f \circ h \circ g = f$? (If this is so, then $\langle f \rangle = \langle f \circ h \rangle$.)

I'm interested in this cube category because of its relevance to modelling cubical type theories. In work with Christian Sattler we're in the process of writing up, we've found that finite product categories with the finite sieve property can be embedded in generalized Reedy categories in a useful way. We used this to characterize a certain model structure on $\square_\lor$ (the subcategory with just one connection, see remarks below), but don't know if any of the arguments apply with $\square_{\land\lor}$.

### Some partial and related answers

The remainder of this post just collects special cases and related results that might or might not be helpful.

**Remark**: Any Eilenberg-Zilber category $\mathcal{C}$ in which there are finitely many face maps into any object has the finite sieve property.

*Proof*: Any $f : B \to A$ generates the same sieve as the degree-raising map of its Reedy factorization, as the degree-lowering map is a split epimorphism. $\blacksquare$

In particular, the simplex category and cartesian cube category (the wide subcategory of $\square_{\land\lor}$ generated by face maps, degeneracies, permutations, and diagonals) have the finite sieve property. If we add one connection to the latter, we get a category that is not generalized Reedy but still has the finite sieve property.

**Proposition**: The wide subcategory $\square_\lor$ of $\square_{\land\lor}$ consisting of maps generated by face maps, degeneracies, permutations, diagonals, and the max-connection $\lor$ has the finite sieve property. (Note: this is equivalently the wide subcategory of join-preserving maps.)

*Proof*: Let $f : [1]^n \to [1]^k$. Such a morphism corresponds to a tuple of $k$ terms in $n$ variables in the theory of bounded join-semilattices. We can assume without loss of generality that no component $f_j : [1]^n \to [1]$ for $1 \le j \le k$ is constant $1$. Then for each $f_j$, we have a normal form $f_j(x_1,\ldots,x_n) = \bigvee S_j$ for some $S_j \subseteq \{x_1,\ldots,x_n\}$. For $1 \le i \le n$, define $T_i = \{j \mid x_i \in S_j\} \subseteq \{1,\ldots,k\}$. If $n > 2^k$, then we must have $T_i = T_{i'}$ for some $i,i'$. Without loss of generality, say $T_1 = T_2$. Then $x_1$ and $x_2$ appear as disjuncts in the same components, so we have $f \circ d \circ c = f$ where $c : [1]^n \to [1]^{n-1}$ maps $(x_1,\ldots,x_n) \mapsto (x_1 \lor x_2, x_3, \ldots, x_n)$ and $d : [1]^{n-1} \to [1]^n$ maps $(y_1,\ldots,y_{n-1}) \mapsto (y_1,y_1,y_2, \ldots, y_{n-1})$. Thus $\langle f \rangle = \langle f \circ d \rangle$. By repeatedly reducing in this way, we find that $\langle f \rangle = \langle f' \rangle$ for some $f' : [1]^{2^k} \to [1]^k$. $\blacksquare$

**Lemma**: The finite sieve property holds for the objects $[1]^k$ with $k \le 2$ in $\square_{\land\lor}$.

*Proof*: The $k = 0$ case is obvious. For $k = 1$, any $f : [1]^n \to [1]$ is either constant $0$, constant $1$, or (we can see from the disjunctive normal form) satisfies $f \circ \Delta \circ f = f$ where $\Delta : [1] \to [1]^n$ is the diagonal $x \mapsto (x,\ldots,x)$.

Now $k = 2$, a bit sketchily. Suppose we have $f : [1]^n \to [1]^2$ and neither component is constant $0$ or $1$ (in which case we could reduce to the $k = 1$ case). We can write each component in disjunctive normal form, $f_j(x_1,\ldots,x_n) = \bigvee_{i \in I_j} \bigwedge C^j_i$ where $I_j$ is nonempty and each $C^j_i$ is a nonempty set of variables. If there exists some $C^1_i$ which is not a superset of any $C^2_{i'}$, choose one and call this $K_1$; otherwise choose an arbitrary $C^1_i$ to be $K_1$. (Note that in the latter case $f_1 \le f_2$.) Likewise, choose $K_2$ among the $C^2_i$ which is not a superset of any $C^1_{i'}$ if possible. Define $g : [1]^2 \to [1]^n$ by $$ g(u_1,u_2)_i \triangleq \bigvee \{u_j \mid x_i \in K_j \} $$ Then $f \circ g \circ f = f$. $\blacksquare$

In the $k \le 2$ case, we always get $f \circ g \circ f = f$ for some $g$. But this does not happen in general, as demonstrated by the following lower bound:

**Proposition**: For any $k \ge 1$, there exists some $f : [1]^n \to [1]^k$ such that $\langle f \rangle \neq \langle g \rangle$ for every $g : [1]^\ell \to [1]^k$ with ${\ell \choose {\lfloor \ell/2 \rfloor}} < 2^{k-1}$.

*Proof:* For any $v \in [1]^k$, write $\#_v \in [1]^{\lvert [1]^k \rvert}$ for the vector taking value $1$ in all coordinates except the $v$th. We define a monotone map $f : [1]^{\lvert [1]^k \rvert} \to [1]^k$.
$$
\begin{align*}
f(\top) &\triangleq \top \\
f(\#_v) &\triangleq v \\
f(\_) &\triangleq \bot &\text{otherwise}
\end{align*}
$$
Suppose we have $\langle f \rangle = \langle g \rangle$ for some $g : [1]^\ell \to [1]^k$, so there exist $h : [1]^n \to [1]^\ell$ and $t : [1]^\ell \to [1]^n$ with $f \circ t \circ h = f$ (and $g = f \circ t$). Then because $f^{-1}(v) = \{\#_v\}$ for $v \in [1]^k\setminus\{\bot,\top\}$, we must have $(t \circ h)(\#_v) = \#_v$ for these $v$. As $\#_v$ and $\#_w$ are incomparable for $v \neq w$, so must be $h(\#_v)$ and $h(\#_w)$. Thus $[1]^\ell$ must contain a set of at least $\lvert [1]^k\setminus\{\bot,\top\} \rvert = 2^{k-1}$ pairwise-incomparable vectors. The maximal antichain in $[1]^\ell$ has ${\ell \choose {\lfloor \ell/2 \rfloor}}$ elements, so ${\ell \choose {\lfloor \ell/2 \rfloor}} \ge 2^{k-1}$. $\blacksquare$

In particular, there is a principal sieve on $[1]^3$ not generated by any $f : [1]^3 \to [1]^3$.

5more comments