Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\). We say a type \(A:\mathord {\textnormal {\textsf {Type}}}(i)\) is categorical fibrant if it is local for the following functions.

• -\((\mathord {\textnormal {\textsf {d}}}^{2},\mathord {\textnormal {\textsf {d}}}^{0}):\Delta \lbrack 1\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{0}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta \lbrack 1\rbrack \rightarrow \Delta \lbrack 2\rbrack \)
• -\(\Delta \lbrack 3\rbrack \mathbin {{}_{(\mathord {\textnormal {\textsf {d}}}^{3}\circ \mathord {\textnormal {\textsf {d}}}^{1},\mathord {\textnormal {\textsf {d}}}^{0}\circ \mathord {\textnormal {\textsf {d}}}^{1})}\mathord {+_{\mathord {\textnormal {\textsf {s}}}^{0}+\mathord {\textnormal {\textsf {s}}}^{0}}}}(\Delta \lbrack 0\rbrack +\Delta \lbrack 0\rbrack )\rightarrow \Delta \lbrack 0\rbrack \)
• -\(((\mathord {\textnormal {\textsf {s}}}^{0},\mathord {\textnormal {\textsf {s}}}^{1}),(\mathord {\textnormal {\textsf {s}}}^{1},\mathord {\textnormal {\textsf {s}}}^{0})):\Delta \lbrack 2\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{1}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta \lbrack 2\rbrack \rightarrow \Delta \lbrack 1\rbrack \times \Delta \lbrack 1\rbrack \)