Proposition [efr-0018]

A pseudo double category is equivalently a simplicial object in \mathsf {Cat} so that the diagrams X[n] \to X[1] are homotopy pullbacks.