The common definition of Reedy category seems to be this one that a Reedy category is a small category $R$ with two wide subcategories $R_+$ and $R_-$ and an ordinal-valued degree function on its objects such that
- Every nonidentity morphism in $R_+$ raises degree,
- Every nonidentity morphism in $R_-$ lowers degree, and
- Every morphism $f$ in $R$ factors uniquely as a map in $R_-$ followed by a map in $R_+$.
However, in a few places, such as the DHKS book Homotopy Limit Functors on Model Categories and Homotopical Categories or Barwick's note On Reedy Model Categories, there is a slightly different definition in which the factorizations are only required to be functorial, rather than unique. Unique factorizations are functorial, but the converse is not generally true.
I think I can prove that a "Reedy category" with functorial factorizations is also a Reedy category with unique factorizations, but my proof is quite roundabout and involves (at least apparently) shrinking the subcategories $R_-$ and $R_+$. Are the definitions actually equivalent?
Edit: Now I think this claim is wrong; see my answer below.