I would follow the suggestion you made in your comment. I believe there is a functor $$ R:Set^{\Delta^{op}} \to Set^{\tilde\Delta^{op}} $$ (where $\tilde\Delta$ is the subcategory of $\Delta$ with the same objects but only coface maps) that takes a simplicial set and removes all degenerate simplices. If I am not mistaken, this should be adjoint to one of the adjoints to the restriction along the inclusion $\tilde\Delta \to \Delta$, the one which adds the smallest number of degenerate simplices. (Check this, I am in a rush to leave on an interstate drive)

There are analogues $R_n$ for the finite subcategories of $\Delta$ consisting of all objects $\le n$.

Assume $S$ is $n$-dimensional. Define it to be of pure dimension if $S' := R_n sk_n S$ satisfies:

• for all $m \le n$, the face maps $d_i : S'_m \to S'_{m+1}$ are jointly surjective.

I think the functors $R,R_n$ preserve products, as do the skeleton functors, so showing that dimension is additive should be ok.

I [EDIT: almost] would follow the suggestion you made in your comment.

[EDIT: below the line was my original answer, which is wrong, as pointed out by Karol in the comments. Here is an answer which is less functorial, but I hope more correct.]

• It would be nice to define pure dimension internal to categories other than $Set$. Unfortunately the definition so far need the internal logic to satisfy excluded middle, and I'm not sure how to get around this. My intuition is that a finitely extensive regular category should be the minimum requirement.

Assume $S$ is $n$-dimensional (i.e. $n$-skeletal). Let $ND(S_n) \subset S_n$ be the non-degenerate $n$-simplices (in Harry's original example this is a finite set), that is, the compliment of the joint image of $$ s_{i_1}\ldots s_{i_{n-k}} : \coprod_{k = 0}^{n-1} S_k \to S_n $$ (we can do this step for simplicial objects in a Boolean topos, or more generally in a regular category with complements of all subobjects and finite coproducts). This defines a presheaf on $\tilde\Delta_n$, the subcategory of $\Delta$ consisting of objects $\le n$ and only the coface maps. The $n$-simplices are $ND(S_n)$ and all lower dimensional simplices are the same as for $S$. Unfortunately this construction is not functorial, because a map of simplicial sets may send non-degenerate simplices to degenerate ones.

Definition: A presheaf $S'$ on $\tilde\Delta_n$ is of pure dimension if the collection of maps

$$ d_{i_1}\ldots d_{i_{n-k}} : S'_n \to \coprod_{k = 0}^{n-1} S'_k $$

is jointly regular epimorphic. This step works in any regular category with finite coproducts. This differs from Harry's suggestion in that we ask that all $k$-simplices are a face of a non-degenerate $n$-simplex.

I'll have a think about the proof that pure dimension, defined this way, is additive. It is here that I think the extensivity should be used.

I believe there is a functor $$ R:Set^{\Delta^{op}} \to Set^{\tilde\Delta^{op}} $$ (where $\tilde\Delta$ is the subcategory of $\Delta$ with the same objects but only coface maps) that takes a simplicial set and removes all degenerate simplices. If I am not mistaken, this should be adjoint to one of the adjoints to the restriction along the inclusion $\tilde\Delta \to \Delta$, the one which adds the smallest number of degenerate simplices. (Check this, I am in a rush to leave on an interstate drive)

There are analogues $R_n$ for the finite subcategories of $\Delta$ consisting of all objects $\le n$.

Assume $S$ is $n$-dimensional. Define it to be of pure dimension if $S' := R_n sk_n S$ satisfies:

• for all $m \le n$, the face maps $d_i : S'_m \to S'_{m+1}$ are jointly surjective.

I think the functors $R,R_n$ preserve products, as do the skeleton functors, so showing that dimension is additive should be ok.