Do you have a source for the discussion where Corfield made that remark?

+1, very enlightening. It looks like the world where the $(n,r) \mapsto (n+1,r+1)$ step were the one "chosen" would have $(2,1)$-categories as its notion of "poset, one dimension up", and this makes sense once I think about it being enriched in groupoids.

I just meant something more from the type theory POV, rather than the category theory one.