Theorem [efr-001T]

1. A pseudo double functor \mathbb {C} \to \mathbb {D} is equivalent to a natural transformation N(\mathbb {C}) \to N(\mathbb {D})
2. If \mathbb {C} is a double category in which each vertical isomorphism has a companion, N(\mathbb {C}) is a weak Segal category
3. Every weak Segal category is equivalent to one of the form N(\mathbb {C}) for \mathbb {C} a pseudo double category of this type.

Let \mathbb {C} be a double category in which every vertical isomorphism has a companion. Then by

reference here, Shulman stuff,

the source and target functors are isofibrant. To prove N(\mathbb {C}) is a weak Segal category, it therefore suffices to prove that N(\mathbb {C})[2] \to N(\mathbb {C})[1] \times _{N(\mathbb {C})[0]} N(\mathbb {C})[1] is an equivalence of categories, and the analogous statement in level 3 (it follows for the higher levels by coskeletality).

Now, let X be a weak Segal. By

reference

, every simplicial category is equivalent to one which is Reedy fibrant. Note that being a Segal category is preserved by equivalence, so without loss of generality, assume X is Reedy fibrant.

This means the functor X[n] \to X(\partial \Delta ^n) is an isofibration for each n. First, let n=1. This means X[1] \to X[0] \times X[0] is an isofibration. Since such fibrations are stable under pullback, this implies that the projection X(\partial \Delta ^2) \to X[1] \times _{X[0]} X[1] is again an isofibration, which means the composite X[2] \to X[1] \times _{X[0]} X[1] is an isofibration. Since this pullback is a homotopy pullback, and X is weak Segal, it is an equivalence, and hence a trivial equivalence. Choose a (strict!) section s.

By a completely analogous argument, choose a section of X[3] \to X[1] \times _{X[0]} X[1] \times _{X[0]} X[1], which is again a trivial fibration.

Let our pseudo double category have X[1] \rightrightarrows X[0] as the underlying reflective graph, composition defined by the composite X[1] \times _{X[0]} X[1] \to X[2] \xrightarrow {d_1} X[1], associator defined using the degeneracies, and unitor defined using the section of X[3]. Call this pseudo double category \mathbb {X}

It is easy to see there is a functor X \to N(\mathbb {X}), which is the identity on the first two levels. Since the higher levels are homotopy pullbacks of the lower levels, this implies it is an equivalence at each level, concluding the proof.