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.