Kerodon

In the second paragraph of the proof, "is factors as" should read "factors as".

Yep. Thanks!

In condition (2) in the proof, "with both with" should just be "with". In condition (3), "element of" should be "as elements of". In the second display in the proof, $f_{10}\circ v_{00}$ should be $(vf)_{01}$.

In the big commutative diagram, there are a couple of errors: in the arrow pointing from $F(vf)$ to $F(v'vf)$, the subscript for $vf$ should be $10$ not $00$, and in the arrow pointing from $F(v'vfu)$ to $F(v'vfuu')$, $u_{11}$ should be $u'_{00}$.

Oops, in my comment #1062, the last expression was meant to be $(vf)_{10}$.

Four instances of a subscript 01 in the proof should be changed to 10: in the first display in the proof, in the big commutative diagram in the arrow from $F(vf)$ to $F(vfu)$, and in the antepenultimate and final displays.

Yep. Thanks!