\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem}
\usepackage{tikz-cd}
\usepackage[numbers,sort&compress]{natbib}
\usepackage[colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,urlcolor=blue!55!black]{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}

\setlength{\emergencystretch}{2em}
\numberwithin{equation}{section}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\nCat}{n\mathrm{Cat}}
\newcommand{\omCat}{\omega\mathrm{Cat}}
\newcommand{\sSet}{\mathrm{sSet}}
\newcommand{\Street}{N_n}
\newcommand{\OrdN}{N}
\newcommand{\U}[1]{U_{#1}}
\newcommand{\Uinf}[1]{U^{\infty}_{#1}}
\newcommand{\Disk}[1]{D_{#1}}
\newcommand{\Orient}[1]{\mathcal O_{#1}}
\newcommand{\trunc}{\tau_n}
\newcommand{\Sd}{\mathrm{Sd}}
\newcommand{\Ex}{\mathrm{Ex}}
\newcommand{\id}{\mathrm{id}}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator*{\colim}{colim}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\im}{im}
\newcommand{\KQ}{\mathrm{KQ}}
\newcommand{\inj}{\text{-}\mathrm{inj}}
\newcommand{\cof}{\text{-}\mathrm{cof}}
\newcommand{\cell}{\text{-}\mathrm{cell}}

\title{Strict Higher Categories Model Spaces in Every Dimension}
\author{A self-contained account of the theorem of Ara and Maltsiniotis}
\date{2026}

\begin{document}
\maketitle

\begin{abstract}
For every $1\le n\le\infty$, the category of small strict globular
$n$-categories admits a proper combinatorial model structure that is
Quillen equivalent to the standard model category of simplicial sets.
Weak equivalences and fibrations are detected by the twice-extended
Street nerve $\Ex^2 N_n$. The Quillen equivalence is the adjunction
$c_n\Sd^2\dashv\Ex^2 N_n$. This proves the higher-dimensional
Thomason model--structure conjecture of Ara and Maltsiniotis.

This writeup gives a complete proof. It is addressed to a reader who
has seen the basic language of categories and topological spaces, but
who may never have met orientals, the Gray tensor product, or the
small-object argument. Every technical step is spelled out, and every
result borrowed from the literature is cited at the exact point of
use. The path from a strict $n$-category to a space follows three
machines: a positive relative prism that makes a strict cylinder
stationary on an old subcategory, a family of fibre and sieve
calculations that let covers be glued, and the small-object argument
that assembles everything into a model structure.
\end{abstract}

\tableofcontents

\section{What the theorem says and why it matters}
\label{sec:introduction}

\subsection{The question}

Topology has a useful trick. A space $X$ is often hard to study
directly. But spaces can be approximated by combinatorial models: cell
complexes, simplicial sets, simplicial groups, and so on. Two spaces
are considered equivalent if they can be deformed into each other
(they are \emph{homotopy equivalent}). The goal of \emph{homotopy
theory} is to understand spaces up to this deformation. The collective
insight of the last fifty years is that a very wide range of
combinatorial objects carry their own internal notion of \emph{weak
equivalence} (a notion of ``these two objects describe the same
space''), and that this notion assembles into a rich algebraic
structure called a \emph{model category}.

The question we answer here is a refinement of a landmark result of
Thomason~\cite{Thomason1980}. Call a functor between small categories
a \emph{Thomason equivalence} if the ordinary nerve construction turns
it into a weak homotopy equivalence of simplicial sets. Thomason
proved that the collection of small categories carries a model
structure whose weak equivalences are exactly these, and that this
model structure is Quillen equivalent to the model structure on
simplicial sets. In plain terms, categories are just as good a model
of spaces as simplicial sets. The bridge is provided by the composite
$c_1\Sd^2\dashv\Ex^2 N_1$, where $N_1$ is the ordinary nerve, $c_1$
is its left adjoint (the ``categorification'' functor), and
$\Sd\dashv\Ex$ is the classical subdivision--extension adjunction of
simplicial sets. Two subdivisions are needed: one is not enough.

\emph{Strict higher categories} generalise categories in another
direction. A strict globular $n$-category has collections of
$k$-cells for $k=0,1,\dots,n$. Objects are $0$-cells; a $1$-cell
$x\to y$ is an arrow; a $2$-cell $\alpha\colon x\Rightarrow y$ sits
between parallel $1$-cells; a $3$-cell sits between parallel $2$-cells;
and so on. Composition is strict: it is associative on the nose and
obeys unit and interchange laws exactly. When $n=1$ we recover ordinary
categories, when $n=\infty$ we get strict globular $\omega$-categories,
and the ``strict'' in the name is deliberate: positive-dimensional
cells need not be invertible.

The Street nerve $N_n$ makes strict $n$-categories into simplicial
sets, and it has a left adjoint $c_n$ given by a colimit of
\emph{orientals}. The higher–dimensional Thomason conjecture of
Ara and Maltsiniotis asks whether the composite
$L_n=c_n\Sd^2$, together with its right adjoint $R_n=\Ex^2 N_n$,
transfers the Kan--Quillen model structure from $\sSet$ to $\nCat$,
and whether the resulting model structure is Quillen equivalent to
$\sSet$ via $(L_n,R_n)$. Ordinary Thomason is the case $n=1$.

\subsection{The main theorem}

We use the following fixed notation.

$\nCat$ is the category of small strict globular $n$-categories and
strict functors; $\omCat=\mathrm{1Cat}_{\omega}$ is the case $n=\infty$;
$\sSet$ is the category of simplicial sets.

$\Orient{m}$ is the $m$th \emph{oriental} of Street. Its defining
property is that maps from $\Orient{m}$ to a strict $\omega$-category
$X$ determine what is called an $m$-\emph{simplex} of $X$, with all
expected face and degeneracy compatibilities. The orientals assemble
into a cosimplicial object $\Orient{\bullet}\colon\Delta\to\omCat$.

For $1\le n\le\infty$, the \emph{Street nerve} is the simplicial set
\[
 N_nX\colon[m]\longmapsto \Hom_{\omCat}(\Orient{m},X)
   =\Hom_{\nCat}(\trunc\Orient{m},X),
\]
where $\trunc\colon\omCat\to\nCat$ is the left adjoint to inclusion
(retaining cells only in dimensions $\le n$). The left adjoint of
$N_n$ is the functor $c_n\colon\sSet\to\nCat$ defined degreewise by the
colimit of orientals
$c_nK=\colim_{\Delta[k]\to K}\trunc\Orient{k}$.

$\Sd\dashv\Ex$ is the classical subdivision adjunction on $\sSet$:
$\Sd\Delta[m]$ is the ordered nerve of the poset of nonempty subsets
of $\{0,\dots,m\}$, and $(\Ex K)_m=\Hom_{\sSet}(\Sd\Delta[m],K)$.
There are natural maps $\ell\colon\Sd\to\id$ and
$j\colon\id\to\Ex$, both objectwise weak homotopy equivalences; both
statements are classical.

Set
\[
 L_n=c_n\Sd^2\colon\sSet\longrightarrow\nCat,
 \qquad
 R_n=\Ex^2N_n\colon\nCat\longrightarrow\sSet.
\]
The composite $L_n\dashv R_n$ is again an adjunction.

Let $W_{\mathrm{KQ}}$ denote the class of weak homotopy equivalences in
$\sSet$ and $\mathrm{Fib}_{\mathrm{KQ}}$ the class of Kan fibrations.
Define three classes of morphisms in $\nCat$:
\begin{equation}\label{eq:main-classes}
  W_n=R_n^{-1}(W_{\mathrm{KQ}})=N_n^{-1}(W_{\mathrm{KQ}}),
  \quad
  F_n=R_n^{-1}(\mathrm{Fib}_{\mathrm{KQ}}),
  \quad
  C_n={}^{\perp}(F_n\cap W_n).
\end{equation}
Here ${}^{\perp}S$ denotes the left lifting class of $S$: the class
of maps that lift on the left against every map in $S$. The two
descriptions of $W_n$ agree because $\Ex$ preserves and reflects weak
equivalences (a consequence of $j$ being an objectwise weak
equivalence; see \S\ref{sec:foundations}).

Set
\begin{align*}
  I&=\{\partial\Delta[m]\hookrightarrow\Delta[m]:m\ge0\},
  \\
  J&=\{\Lambda^k[m]\hookrightarrow\Delta[m]:m\ge1,\ 0\le k\le m\}.
\end{align*}

\begin{theorem}[Main theorem]\label{thm:main}
For every $n\in\{1,2,3,\dots\}\cup\{\infty\}$, the three classes
$(C_n,W_n,F_n)$ in \eqref{eq:main-classes} form a proper
combinatorial model structure on $\nCat$. It is cofibrantly
generated by $(L_nI,L_nJ)$. The adjunction
\[
 L_n\colon\sSet_{\mathrm{KQ}}
   \rightleftarrows(\nCat,C_n,W_n,F_n)\colon R_n
\]
is a Quillen equivalence.
\end{theorem}

In words: $\nCat$ is a model category in which a map is a weak
equivalence iff its twice-extended Street nerve is a weak
homotopy equivalence, a fibration iff its twice-extended Street nerve
is a Kan fibration, and a cofibration iff it has the left lifting
property against the simultaneous weak equivalences and fibrations.
The pair $(L_n,R_n)$ lifts the standard simplicial model structure to
$\nCat$ on the nose, and it is an equivalence of homotopy theories.

\subsection{How the proof goes: three machines}

A reader meeting the theorem for the first time may wonder why it is
not obvious. There are two obstacles that do not occur in
dimension one.

\emph{The subdivision obstacle.} One subdivision $\Sd$ is not enough
to make the natural map $\Sd K\to N_1c_1\Sd K$ a weak equivalence;
a second subdivision fixes the problem by iterating the direction
of the subdivision. The same phenomenon occurs here, and we defer
it entirely: the subdivision facts are inputs, and the meaningful
work happens after subdivision.

\emph{The pushout obstacle.} To build a model structure by transfer
from $\sSet$, one needs to know that the small-object construction
behaves well. Concretely, for every map $d$ in the generating set $J$,
one needs that any pushout of $L_nd$ is a weak equivalence in $\nCat$.
But $L_nd$ is a map of the form $\U{A}\to\U{B}$, where
$\U{E}=c_n\OrdN E$ is the strict $n$-category attached to a poset $E$
and $\OrdN$ is the ordinary nerve. So the question becomes: when is a
pushout
\[
 X\longrightarrow X\amalg_{\U{A}}\U{B}
\]
a weak equivalence, for every attaching functor $\U{A}\to X$?

Thomason solved this in dimension one by identifying a class of
poset inclusions --- the \emph{Dwyer maps} --- with the property that
their every cobase change is a weak equivalence. The heart of the
present proof is the discovery that this class admits a clean
synthesis in every higher dimension.

\textbf{Machine 1: the positive relative prism.} Fix a downward-closed
poset inclusion $A\subset E$ (a ``sieve''). Suppose $f,g\colon E\to E$
are monotone with $f\le g$, with $f$ and $g$ agreeing on $A$, and with
$g$ constant on the complement $E\setminus A$. Then there is an
explicit \emph{strict right Gray cylinder}
\[
 P_{f,g}\colon\U{E}\otimes\Disk{1}\longrightarrow\U{E}
\]
whose two endpoints are $U(f)$ and $U(g)$, and which is \emph{stationary}
on $\U{A}$: at every parameter value it acts on $\U{A}$ by the common
restriction $f|_A=g|_A$. The construction is a simplexwise chain
computation using the Alexander--Whitney corner, and it survives
descent to every finite dimension by an internal-hom calculation.
The stationarity is what makes everything glue.

\textbf{Machine 2: covers.} Given a sieve $A\subseteq B$ whose
inclusion into its upward closure $Z$ has a right-adjoint retraction
$r\colon Z\to A$, one uses the prism to contract $A\hookrightarrow Z$
\emph{couniversally}: for every attaching functor $\U{A}\to X$, the
map $X\to X\amalg_{\U{A}}\U{Z}$ is a weak equivalence. Then one covers
$B$ by the two cosieves $Z$ and $B\setminus A$, glues by simplicial left
properness, and obtains the comparison between a pushout of nerves and
the nerve of the pushout. Applied to the twice-subdivided boundaries
and horns, this supplies the model-structure inputs.

\textbf{Machine 3: transfer.} With the acyclicity and invariance
inputs in hand, the small-object argument runs as in any transfer
proof. The subtlety is that the small-object factorisation is
computed in $\nCat$, not in $\sSet$; this is where the requirement
that all attaching functors be allowed to be arbitrary matters.
The unit of the adjunction $L_n\dashv R_n$ on an arbitrary simplicial
set is assembled from the poset case by gluing along boundaries,
using left properness of $\sSet$.

\subsection{Relation to earlier work}

Thomason~\cite{Thomason1980} proves the case $n=1$. Cisinski
\cite{Cisinski1999} corrects the retract argument used for properness.
Ara and Maltsiniotis developed an abstract transfer theorem and
proved the case $n=2$ together with the Quillen equivalence
\cite{AraMaltsiniotis2014}. They also state the general conjecture;
Ara's 2023 manuscript \cite{Ara2023} records the remaining condition
and Guetta and Maltsiniotis \cite{GuettaMaltsiniotis2024} restate the
$\omega$-dimensional case. The positive-poset and unit conditions in
all dimensions were proved earlier
\cite{AraMaltsiniotis2015,Gagna2018}; the missing ingredient was the
couniversality of a sieve with a right-adjoint retraction, which the
present relative prism supplies in arbitrary target categories.

\subsection{Organization and conventions}

Sections~\ref{sec:foundations}--\ref{sec:attachments} are the
mathematical core. Section~\ref{sec:foundations} fixes notation and
proves the small foundational lemmas. Section~\ref{sec:prisms}
constructs the relative prism and proves the cylinder-gluing lemma.
Section~\ref{sec:pieces} does the fibre and sieve calculations.
Section~\ref{sec:couniversality} proves couniversality and the
unit on posets. Section~\ref{sec:attachments} proves the comparison
for subdivided boundary and horn attachments. Section~\ref{sec:transfer}
assembles the model structure, properness, and Quillen equivalence.
Section~\ref{sec:presentability} is an appendix proving local
finite presentability of $\nCat$ from a signature.

Throughout, the universe is fixed and small; we write ``small'' for
``sets'', and we allow ourselves to enlarge the universe when forming
categories of small objects. The symbol $\Disk{1}$ denotes the
interval category $0\to1$, and $\Disk{i}$ the free strict $\omega$-category
on one $i$-cell. The interval is the \emph{right} tensor factor in
every Gray-cylinder formula, per the convention of
\cite[Appendix~B.4]{AraMaltsiniotis2020}.

\subsection*{Notation at a glance}

For the reader's convenience, here is a compact index of the symbols
that appear most often. Detailed definitions are in the section that
first introduces each item.

\begin{itemize}
\item $\nCat$: small strict globular $n$-categories. $\omCat$: the case
  $n=\infty$.
\item $\sSet$: simplicial sets; $N$: ordinary nerve; $\Street$: Street
  nerve.
\item $\Orient{m}$: the $m$th oriental. $\Disk{i}$: the free strict
  $\omega$-category on one $i$-cell.
\item $c_n$: left adjoint of $\Street$, computed by
  $c_nK=\colim_{\Delta[m]\to K}\trunc\Orient{m}$.
\item $\Sd\dashv\Ex$: subdivision-extension adjunction on simplicial
  sets.
\item $L_n=c_n\Sd^2$, $R_n=\Ex^2\Street$: the two sides of the Quillen
  equivalence.
\item $W_n,F_n,C_n$: weak equivalences, fibrations, cofibrations.
\item $\U{E}=c_n\OrdN E$: strict $n$-category attached to a poset $E$.
\item $\nu$: Steiner's functor from directed chain complexes to strict
  $\omega$-categories.
\item $M[m]$: normalized simplex complex. $G[i]$: globe complex.
\item $\otimes$: Gray tensor product. $\Disk{1}$: interval, used as the
  right factor.
\item $H(Y)$: right internal hom for the Gray tensor.
\item $W_{\mathrm{KQ}},\mathrm{Fib}_{\mathrm{KQ}}$: weak equivalences
  and Kan fibrations in $\sSet$.
\item $I,J$: generating sets for the simplicial model structure.
\end{itemize}

\section{Foundations}
\label{sec:foundations}

The pushout argument rests on four foundations: strict categories give
a concrete presentation of the Gray tensor product through directed
chain complexes; strict right cylinders correspond to certain
simplicial homotopies of nerves; strict categories are locally
finitely presentable, so filtered colimits are well behaved; and
certain pushouts of simplicial sets are weak equivalences whenever
one leg is monomorphic. We fix notation and prove the small local
statements here, deferring only the presentability proof to
Section~\ref{sec:presentability}.

\subsection{Strict globular categories}

We fix a universe. A \emph{globular set} is a sequence
$X_0,X_1,X_2,\dots$ of sets with maps $s,t\colon X_{k+1}\to X_k$ (source
and target) satisfying $ss=st$ and $ts=tt$, where the leftmost letter
is the inner face. A \emph{strict globular $\omega$-category} is a
globular set together with compositions $\circ_k$ along $k$-matching
boundaries (for $k\ge0$ and $x,y\in X_{k+1}$ with $sx=ty$), identities
$e_k\colon X_k\to X_{k+1}$, satisfying the strict associativity, unit,
and interchange laws. Positive-dimensional cells are not required to
be invertible. A \emph{strict globular $n$-category} for finite $n$ is
a strict $\omega$-category with exactly one cell in each dimension
$>n$. We write $\nCat$ for the category of small strict $n$-categories
and strict functors, and $\omCat=\mathrm{1Cat}_\omega$ (the case
$n=\infty$).

The inclusion $\nCat\hookrightarrow\omCat$ has a left adjoint
$\trunc=\tau_n$. Explicitly, $\tau_n X$ retains the cells of $X$ in
dimensions below $n$; its $n$-cells are the $n$-cells of $X$ modulo
the congruence closed under every defined composition and generated by
\[
 s_n(z)=t_n(z)\qquad(z\text{ an }(n+1)\text{-cell of }X).
\]
Generating pairs are parallel $n$-cells, so their identifications
leave every lower matching boundary unchanged; compositions descend.
Cells above $n$ become identities. Every strict functor from $X$ to an
$n$-category annihilates these relations, proving the reflection
property. Set $\tau_\infty=\id$.

Write $\Disk{k}$ for the free strict $\omega$-category on one $k$-cell
with all its globular faces. Thus $\Hom_{\omCat}(\Disk{k},X)$ is the
set of $k$-cells of $X$, $\Disk{0}$ is terminal, and $\Disk{1}$ is the
category $0\to1$.

\subsection{Orientals and the Street nerve}

The $m$th \emph{oriental} $\Orient{m}$ is a strict $\omega$-category
freely generated by the $m$-simplex. The cosimplicial structure maps
$[-]\colon\Delta\to\omCat$ encode faces and degeneracies by applying a
monotone map of ordinals $\alpha\colon[q]\to[m]$ to the generating
chain complex; this is standard, and we take it from Street
\cite{Street1987}. For $1\le n\le\infty$ the \emph{Street nerve}
\[
 \Street X\colon[m]\longmapsto\Hom_{\omCat}(\Orient{m},X)
     =\Hom_{\nCat}(\trunc\Orient{m},X)
\]
is a simplicial set. The two formulas agree because maps out of
$\Orient{m}$ into an $n$-category annihilate the congruence defining
$\trunc\Orient{m}$. The left adjoint
$c_n\colon\sSet\to\nCat$ is computed by the canonical colimit
\begin{equation}\label{eq:categorification-colimit}
 c_nK=\colim_{(\Delta[m]\to K)\in\Delta/K}\trunc\Orient{m}
     \cong\colim_{\Delta[m]\to K}\trunc\Orient{m},
\end{equation}
by the universal property of a colimit and the definition of the
nerve.

For a poset $E$ write $\OrdN E$ for its ordinary nerve (the
simplicial set of monotone maps $[m]\to E$), and
\[
 \U{E}=c_n\OrdN E,\qquad \Uinf{E}=c_\infty\OrdN E,
\]
so $\U{E}=\trunc\Uinf{E}$. For a monotone map $f\colon E\to E'$, write
$U(f)=c_n\OrdN(f)$ and $U^\infty(f)=c_\infty\OrdN(f)$. On ordinary
categories $N_1$ agrees with $N_\infty$: a map from an oriental is
determined by its successive edges, because the triangular cells
impose the composition equations. In particular
$N_\infty\Disk{1}=\Delta[1]$.

\subsection{Subdivision, extension, and the prescribed classes}

The \emph{subdivision} functor $\Sd\colon\sSet\to\sSet$ sends
$\Delta[m]$ to the ordered nerve of the poset of nonempty subsets of
$\{0,\dots,m\}$; it is a left adjoint, with right adjoint
$\Ex\colon\sSet\to\sSet$ defined by
$(\Ex K)_m=\Hom_{\sSet}(\Sd\Delta[m],K)$. The \emph{last-vertex
transformation} $\ell\colon\Sd\to\id$ is objectwise a weak homotopy
equivalence; its mate $j\colon\id\to\Ex$ is also objectwise a weak
homotopy equivalence. Both facts are classical
\cite[Theorem~4.5]{AraMaltsiniotis2014},
\cite[III.4.6]{GoerssJardine1999}. Naturality of $\ell$ and $j$ together
with formal two-out-of-three shows that $\Sd$ and $\Ex$ preserve and
reflect weak homotopy equivalences.

Set $L_n=c_n\Sd^2$ and $R_n=\Ex^2\Street$. They are adjoint by
composition of adjunctions. Let $W_{\mathrm{KQ}}$ be the class of weak
homotopy equivalences and $\mathrm{Fib}_{\mathrm{KQ}}$ the class of
Kan fibrations in $\sSet$. Define
\[
 W_n=R_n^{-1}(W_{\mathrm{KQ}})=N_n^{-1}(W_{\mathrm{KQ}}),
 \quad
 F_n=R_n^{-1}(\mathrm{Fib}_{\mathrm{KQ}}),
 \quad
 C_n={}^\perp(F_n\cap W_n).
\]
The two descriptions of $W_n$ agree because $\Ex^2$ preserves and
reflects $W_{\mathrm{KQ}}$. Set
$I=\{\partial\Delta[m]\hookrightarrow\Delta[m]:m\ge0\}$ and
$J=\{\Lambda^k[m]\hookrightarrow\Delta[m]:m\ge1,\ 0\le k\le m\}$.

\subsection{Augmented directed complexes and Steiner's functor}

An \emph{augmented directed complex} is a nonnegative chain complex
$K$ of abelian groups with augmentation $\epsilon\colon K_0\to\mathbb Z$
and a specified additive submonoid $K_p^+\subset K_p$ in each degree.
Morphisms are chain maps preserving augmentation and submonoids. All
complexes below have a specified free basis; the positive submonoid
is generated by the basis. For each basis element write
$dc=d^+c-d^-c$ with disjoint positive supports. A basis is
\emph{unital} when $\epsilon((d^-)^pb)=\epsilon((d^+)^pb)=1$ for each
basis element $b$ in degree $p$. A basis is \emph{strongly loop-free}
when the relations
\[
 a<b\quad\text{if }a\text{ occurs in }d^-b,\qquad
 b<a\quad\text{if }a\text{ occurs in }d^+b
\]
are contained in a strict partial order on the whole basis.
A complex with such a basis is a \emph{strong Steiner complex}.

Steiner's functor $\nu$ sends augmented directed complexes to strict
$\omega$-categories. A $p$-cell of $\nu K$ is a table
\[
 (x_0^-,x_0^+\mid x_1^-,x_1^+\mid\cdots\mid x_p^-,x_p^+),
 \quad x_r^\pm\in K_r^+,
\]
such that
\[
 \epsilon x_0^-=\epsilon x_0^+=1,\quad
 d x_r^-=d x_r^+=x_{r-1}^+-x_{r-1}^-\ \ (1\le r\le p),\quad
 x_p^-=x_p^+.
\]
An identity appends a zero pair. A positive augmentation-preserving
chain map acts entrywise, giving a strict functor. For a basis element
$b$ in degree $p$, its \emph{atom} has top pair $(b,b)$ and entries
$\langle b\rangle_r^\pm=(d^\pm)^{p-r}b$: reduce the boundary by
alternating positive or negative parts. For a strong Steiner complex
these tables are cells, and $\nu K$ is freely generated as a polygraph
by these atoms; maps out of $\nu K$ are determined by their values on
them \cite[Definitions~2.6, 2.8, Theorem~6.1]{Steiner2004}.

We use two concrete complexes.

\textbf{(i) The normalized simplex complex} $M[m]$. Its degree-$p$
basis is the set of strictly increasing tuples $[i_0,\dots,i_p]$ in
$[m]=\{0,\dots,m\}$, with $d=\sum_j(-1)^j(\text{delete }i_j)$ for
$p>0$ and $\epsilon[i]=1$. A monotone map of ordinals acts by applying
it to the tuple; a tuple with a repeated entry becomes zero. It is
strong Steiner and $\nu M[m]=\Orient{m}$. The atom of a nonempty
tuple has its first and last vertices as its $0$-source and
$0$-target.

\textbf{(ii) The globe complex} $G[i]$. It has one top basis element
in degree $i$ and two basis elements (source and target faces) in each
degree below $i$. Positive-degree differentials are target minus
source; vertices have augmentation one. It is strong Steiner and
$\nu G[i]=\Disk{i}$. For $i=0$ there is one vertex.

Both facts are contained in \cite[Examples~3.8--3.10, Example~4.7,
Theorem~5.11]{Steiner2004}, and the oriental identification and
cosimplicial action, including repeated entries, in
\cite[Theorem~3.2, \S4]{Steiner2007}.

The tensor of augmented directed complexes is the ordinary nonnegative
chain tensor with separate augmentation:
\begin{equation}\label{eq:tensor-differential}
 d(x\otimes y)=dx\otimes y+(-1)^{|x|}x\otimes dy,\qquad
 \epsilon(x\otimes y)=\epsilon(x)\epsilon(y)\ \ (|x|=|y|=0).
\end{equation}
Its positive submonoid is generated by tensors of positive elements.
The tensor product of two strong Steiner bases (as sets) is the
positive basis of the tensor complex.

\subsection{The Gray tensor product}

The category $\omCat$ (and $\nCat$ for finite $n$) carries the
\emph{biclosed Gray tensor product}
$\otimes\colon\omCat\times\omCat\to\omCat$, which we take from
Ara and Maltsiniotis \cite[Theorem~A.15 and \S A.16]{AraMaltsiniotis2020}.
It has unit $\Disk{0}$, preserves small colimits separately in each
variable, and admits natural identifications
\begin{equation}\label{eq:steiner-tensor}
 \nu K\otimes\nu L\ \cong\ \nu(K\otimes L)
 \qquad(K,L\text{ strong Steiner}),
\end{equation}
natural in every morphism between strong Steiner complexes,
including ones sending basis elements to sums or zero. This is the
completed extension theorem; the general extension is not being
inferred from the incomplete proof of \cite[Theorem~7.3]{Steiner2004}.
Colimit preservation is a property of the Gray tensor, not of $\nu$.

It follows that $\Disk{i}\otimes\Disk{1}$ is generated by the atoms
indexed by pairs of globe basis elements, of dimension the sum. The
same holds for $\Orient{m}\otimes\Disk{1}$. Globe face inclusions and
simplex face inclusions identify the corresponding based subcomplexes:
the positive and negative boundaries of a basis element inside the
subcomplex are unchanged by inclusion, so the atom agrees.

Throughout, the interval is the \emph{right} tensor factor. Write
$e_0,e_1$ for the degree-zero basis elements of $M[1]$ and $u$ for
its degree-one element, so $du=e_1-e_0$. Write
$e_a\colon\Disk{0}\to\Disk{1}$ for the endpoint functors and
$\epsilon\colon\Disk{1}\to\Disk{0}$ for the unique functor. The
\emph{projection} is $\pi_X=\id_X\otimes\epsilon\colon
X\otimes\Disk{1}\to X\otimes\Disk{0}\cong X$. No interchange of
factors is used.

\subsection{Right cylinders and truncation}

Biclosedness supplies an $\omCat$-object $H(Y)$ and natural bijections
\begin{equation}\label{eq:right-internal-hom}
 \Hom_{\omCat}(X,H(Y))\cong\Hom_{\omCat}(X\otimes\Disk{1},Y).
\end{equation}
In the notation of \cite[\S A.18]{AraMaltsiniotis2020},
$H(Y)=\Hom_{\mathrm{oplax}}(\Disk{1},Y)$; formula
\eqref{eq:right-internal-hom} fixes the convention. Evaluation at
$e_0,e_1$ and precomposition with $\pi_X$ give, respectively, the
endpoints and constant cylinders, transposing functors of one
variable. To extend cylinders through pushouts we use transposes into
$H(Y)$. The next lemma shows that this stays within $\nCat$ when
$Y$ is an $n$-category.

\begin{lemma}[Internal hom and reflection]\label{lem:internal-truncation}
Let $n<\infty$ and let $Y$ be a strict $n$-category. Then $H(Y)$ is a
strict $n$-category. Consequently the reflection unit $X\to\trunc X$
induces a natural bijection
\begin{equation}\label{eq:truncated-cylinder-bijection}
 \Hom_{\omCat}((\trunc X)\otimes\Disk{1},Y)
 \ \xrightarrow{\ \cong\ }\
 \Hom_{\omCat}(X\otimes\Disk{1},Y).
\end{equation}
This bijection respects endpoints and restriction along functors in
the first variable. For $n=\infty$ the same assertion holds with
$\trunc=\id$.
\end{lemma}

\begin{proof}
An $i$-cell of $H(Y)$ is a functor
$P\colon\Disk{i}\otimes\Disk{1}\to Y$. Let
$s\colon\Disk{i-1}\to\Disk{i}$ be the source inclusion and
$p\colon\Disk{i}\to\Disk{i-1}$ the map sending the top $i$-cell to
the identity of the top $(i-1)$-cell. Then $ps=\id$, and
$q=sp$ collapses $\Disk{i}$ onto its source. Under
\eqref{eq:right-internal-hom}, the identity of the source of $P$ is
$P(q\otimes\id)$. We show that $P=P(q\otimes\id)$ when $i>n$.

The atoms of $\Disk{i}\otimes\Disk{1}$ outside
$\Disk{i-1}\otimes\Disk{1}$ come from pairs: top $i$-generator
paired with $e_0$, $e_1$, or $u$; target $(i-1)$-generator paired
with $e_0$, $e_1$, or $u$. Their dimensions are respectively
$i,i,i+1$ and $i-1,i-1,i$. If $i>n+1$, all exceed $n$. If $i=n+1$,
only the target $n$-generator paired with $e_0$ or $e_1$ has
dimension $\le n$. Either endpoint, $P$ sends the top
$(n+1)$-cell to an identity, so its source and target $n$-cells have
equal images; these are the two comparisons needed to match
$P$ and $P(q\otimes\id)$ on the remaining degree-$n$ atoms. All atoms
in the source face are fixed by $q\otimes\id$.

The two functors therefore agree on all atoms of dimension $\le n$.
They also agree on higher atoms: in an $n$-category the image of a
cell of dimension $>n$ is the iterated identity on its $n$-source,
which is already determined. Generation by atoms proves
$P=P(q\otimes\id)$. Thus every cell of $H(Y)$ above $n$ is an
identity, so $H(Y)$ is an $n$-category.

Now transpose a cylinder to a functor $X\to H(Y)$. Since $H(Y)$ is an
$n$-category, it factors uniquely through $\trunc X$. Transposing
back proves \eqref{eq:truncated-cylinder-bijection}. Naturality of
reflection and of the adjunction prove the restriction assertion;
endpoint assertions follow by naturality of evaluation or by
uniqueness of the factorization into $Y$.
\end{proof}

\begin{remark}\label{rem:omega-tensor-at-finite-n}
Even for $X,Y$ in $\nCat$, the expression $X\otimes\Disk{1}$
denotes their tensor in $\omCat$ and may have cells above $n$. A map
from this tensor into $Y$ is nevertheless represented by a map
$X\to H(Y)$ \emph{in $\nCat$}. This is what permits stationary
cylinders to be glued by arbitrary pushouts in $\nCat$.
\end{remark}

\subsection{A strict right cylinder gives a nerve homotopy}

The next lemma lets a strict cylinder $P\colon X\otimes\Disk{1}\to Y$
be turned into an ordinary simplicial homotopy of Street nerves. It
uses the Alexander--Whitney diagonal. The statement is due to Ara
\cite[\S\S5.2.2--5.2.6, especially Proposition~5.2.3]{Ara2023}; we
include a proof for completeness.

\begin{lemma}[Right Gray cylinder gives a nerve homotopy]
\label{lem:gray-nerve}
There is a natural simplicial map
\[
 J_X\colon N_\infty X\times\Delta[1]\longrightarrow
          N_\infty(X\otimes\Disk{1})
\]
whose restriction at the endpoint $a\in\{0,1\}$ is
$N_\infty(\id_X\otimes e_a)$, and for which
$N_\infty(\pi_X)\,J_X$ is the projection onto $N_\infty X$.
Consequently a strict functor $P\colon X\otimes\Disk{1}\to Y$
induces a simplicial homotopy between the nerves of its endpoint
functors. If a functor $a\colon A\to X$ satisfies
$P(a\otimes\id)=h\pi_A$ for some $h\colon A\to Y$, then the
homotopy restricts along $N_\infty a$ to the constant homotopy
of $N_\infty h$. The same applies to $\Street$ when $X,Y$ are
$n$-categories.
\end{lemma}

\begin{proof}
For each $m$, define the Alexander--Whitney diagonal
\cite[IV.2, Remark~2.5]{GoerssJardine1999}
\[
 \operatorname{AW}_m[i_0,\dots,i_p]
   =\sum_{a=0}^{p}[i_0,\dots,i_a]\otimes[i_a,\dots,i_p]
\]
as a map $M[m]\to M[m]\otimes M[m]$. It is a positive chain map.
In $d$ of the right side, the term obtained by deleting a vertex
strictly before or after the shared vertex matches a term in
$\operatorname{AW}_md$; the term deleting the final vertex of the
first factor at cut $a$ and the term deleting the initial vertex of
the second factor at cut $a-1$ are equal up to sign, hence cancel
by the tensor sign in \eqref{eq:tensor-differential}. Every summand
is positive. On vertices the augmentation is one; applying the
counit to the first or second factor selects, respectively, only
the cut $a=0$ or $a=p$. Thus both counits give the identity.

The diagonal is natural for every monotone ordinal map. For a
strictly increasing image this is term by term. If the image has
equalities at positions $j,j+1$, then every cut $a\le j$ yields a
degenerate second factor and every cut $a\ge j+1$ yields a degenerate
first factor; both sides of naturality are zero after normalization.
This verifies faces and degeneracies. Only this cosimplicial
naturality is claimed.

Apply $\nu$ and \eqref{eq:steiner-tensor} to get natural functors
$\delta_m\colon\Orient{m}\to\Orient{m}\otimes\Orient{m}$. For an
$m$-simplex $F\colon\Orient{m}\to X$ and monotone
$\theta\colon[m]\to[1]$ put
\[
 J_X(F,\theta)=(F\otimes\Orient{\theta})\delta_m,
\]
where $\Orient{\theta}\colon\Orient{m}\to\Orient{1}=\Disk{1}$ is
the cosimplicial structure map. The naturality just verified shows
that $J_X$ is simplicial. If $\theta$ is constant at $a$, the map
factors through the right counit and the endpoint $e_a$, giving
$J_X(-,a)=N_\infty(\id_X\otimes e_a)$. Applying $\pi_X$ also yields
the right counit, so $N_\infty(\pi_X)J_X$ is the projection.
Postcomposing with $N_\infty P$ proves the homotopy assertion.
Naturality in $X$ and the projection formula prove stationarity.
\end{proof}

\subsection{Filtered colimits and local presentability}

Strict $n$-categories admit a simple filtered-colimit theory. The
argument is deferred to Section~\ref{sec:presentability}, and we only
record the consequences here.

\begin{lemma}[Filtered colimits]\label{lem:filtered}
For every $1\le n\le\infty$ the category $\nCat$ is locally
finitely presentable; filtered colimits in $\nCat$ are computed on
cells. Each $\trunc\Orient{m}$ is finitely presentable in $\nCat$.
Consequently $\Street$, and $\Ex^r\Street$ for every finite $r\ge0$,
preserve filtered colimits. Weak homotopy equivalences of simplicial
sets are closed under filtered colimits of arrows, as are the maps
$f$ of $\nCat$ for which $\Street f$ is a weak homotopy equivalence.
No monomorphism hypothesis on transition maps is required.
\end{lemma}

\begin{proof}
The first two claims are proved in
Proposition~\ref{prop:strict-presentability}. For the third: an
oriental has a finite polygraphic presentation with one generator
per nonempty strictly increasing tuple. A map from $\Orient{m}$ into
a filtered colimit lifts to one stage, and equality of two such maps
is detected there; the same argument applies to
$\trunc\Orient{m}$. Hence $\Orient{m}$ and $\trunc\Orient{m}$ are
finitely presentable, and the colimits in \eqref{eq:categorification-colimit}
display $\Street$ as preserving filtered colimits degreewise.
Indeed $(\Ex K)_m=\Hom(\Sd\Delta[m],K)$ with $\Sd\Delta[m]$ finite,
so $\Ex$ also preserves filtered colimits.

Now the weak-equivalence claim. Let $Q=\Ex^\infty$. It preserves
filtered colimits because $\Ex$ does and colimits commute with
colimits. A filtered colimit of Kan complexes is Kan: any horn has
finitely many nondegenerate simplices and its equations occur at one
stage. For a filtered diagram of Kan complexes $K_i$, choose a
vertex $x$ of $\colim K_i$ represented by $x_i\in K_i$. The coslice
$(i\to j)$ is filtered with final projection onto the base; for each
$k\ge 1$,
\[
 \colim_{(i\to j)}\pi_k(K_j,x_j)\cong\pi_k(\colim_jK_j,x),
\]
because the pointed sphere $\Delta[k]/\partial\Delta[k]$ and its
finite reduced cylinder represent classes and homotopies in finite
data, all of which lift to a sufficiently late stage. This proves
both surjectivity and injectivity of the comparison, including
eventual equalities without injectivity of transitions. It follows
that an objectwise weak equivalence between filtered diagrams of Kan
complexes induces a weak equivalence on colimits. Combining with
$K\to QK$ and two-out-of-three gives the claim for $W_n$, and then
$\Street$ preservation gives it for $W_n=N_n^{-1}(W_{\mathrm{KQ}})$.
\end{proof}

\subsection{The simplicial gluing lemma}

We need one properness-type statement for the Kan--Quillen model
structure, phrased so that it isolates the monomorphic leg.

\begin{lemma}[Gluing with one monomorphic leg]
\label{lem:simplicial-gluing}
Consider a map of spans of simplicial sets
\[
 \begin{tikzcd}[column sep=large]
  A \arrow[d,"a"'] &
  C \arrow[l] \arrow[r,hook,"i"] \arrow[d,"c"'] &
  B \arrow[d,"b"]\\
  A' &
  C' \arrow[l] \arrow[r,hook,"i'"'] &
  B'.
 \end{tikzcd}
\]
where $i$ and $i'$ are monomorphisms. If $a,b,c$ are weak
equivalences, then the induced map
$A\amalg_CB\to A'\amalg_{C'}B'$ is a weak equivalence. There is no
condition on $C\to A$ or $C'\to A'$. Each displayed pushout computes
a homotopy pushout. In particular, cobase change of a weak
equivalence along a simplicial monomorphism is a weak equivalence.
\end{lemma}

\begin{proof}
Put $E=B\amalg_C C'$. By simplicial left properness $B\to E$ is a
weak equivalence, as the pushout of $c$ along the monomorphism $i$.
Two-out-of-three gives $E\to B'$ a weak equivalence. Both
$C'\to E$ and $C'\to B'$ are cofibrations, hence cofibrant in
$C'/\sSet$. Cobase change along $C'\to A'$ is a left Quillen
functor $C'/\sSet\to A'/\sSet$; its right adjoint restricts along
the structure map, which preserves fibrations and trivial
fibrations. It preserves weak equivalences between cofibrant
objects, so
\[
 A'\amalg_C B\cong A'\amalg_{C'}E\to A'\amalg_{C'}B'
\]
is a weak equivalence. Also $A\to A\amalg_CB$ is a monomorphism
(pushout of $i$), so left properness applied to $a$ gives
$A\amalg_CB\to A'\amalg_CB$ a weak equivalence. Composing the two
proves the main claim.

For the homotopy-pushout assertion, factor $C\to A$ as a cofibration
$C\hookrightarrow\widetilde A$ followed by a trivial fibration
$\widetilde A\to A$. The span
$\widetilde A\leftarrow C\hookrightarrow B$ is a cofibrant
replacement of the given span: three cofibrant objects, both legs
cofibrations. Its pushout is weakly equivalent to $A\amalg_CB$ by
the main claim.
\end{proof}

The gluing lemma completes the foundations. Sections
\ref{sec:prisms}--\ref{sec:attachments} build the relative prism and
couniversality; Section~\ref{sec:transfer} assembles the model
structure.

\section{The positive relative prism}
\label{sec:prisms}

The heart of the proof is a construction which turns a certain pair of
poset maps into a strict Gray cylinder, with two crucial properties:
the two endpoints are given by the two maps, and the cylinder is
\emph{stationary} on an old subset --- at every parameter value it acts
by the same prescribed functor. Stationarity is what allows the
cylinder to survive pushouts: after an attachment identifies the old
subset with something new, the whole cylinder lands inside the
pushout.

The construction works at the level of directed chain complexes. A
sieve $A\subseteq E$ of posets fixes a downward-closed subposet; on
the new part $E\setminus A$ we contract to a constant. Then
Steiner's functor $\nu$ converts the chain-level cylinder into a
strict functor of $\omega$-categories, and reflection $\trunc$ carries
it to finite $n$.

Throughout this section the interval is the right tensor factor.
Write $\epsilon\colon\Disk{1}\to\Disk{0}$ for the unique functor to
the Gray unit, and set
$\pi_B=\id_B\otimes\epsilon\colon B\otimes\Disk{1}\to B$.
For $i\colon A\to B$ and $v\colon A\to C$, a cylinder
$P\colon B\otimes\Disk{1}\to C$ is \emph{stationary along $i$
relative to $v$} if
\[
 P(i\otimes\id)=v\pi_A
\]
as strict functors (including every cell of $A$).

\subsection{The relative prism lemma}

\begin{lemma}[Relative prism]\label{lem:relative-prism}
Let $A\subseteq E$ be a downward-closed subposet, and let
$f,g\colon E\to E$ be monotone with
\[
 f(e)\le g(e)\ \ (e\in E),\qquad f|_A=g|_A,
 \qquad g|_{E\setminus A}\text{ constant}.
\]
For each $1\le n\le\infty$ there is a strict functor
\[
 P_{f,g}\colon\U{E}\otimes\Disk{1}\longrightarrow\U{E}
\]
whose restrictions at the two interval endpoints are $U(f)$ and
$U(g)$. Writing $i\colon A\hookrightarrow E$ and
$v=fi=gi\colon A\to E$, one has the stationarity identity
\begin{equation}\label{eq:prism-stationarity}
 P_{f,g}(U(i)\otimes\id_{\Disk{1}})=U(v)\pi_{\U{A}}.
\end{equation}
Consequently the endpoints induce simplicially homotopic maps on
Street nerves, stationary relative to $\Street U(v)$.
\end{lemma}

\begin{proof}
\emph{Step 1: setup.} If $T$ is a nonempty finite totally ordered set,
write $M[T]$ for the augmented normalized simplex chain complex on $T$
with basis the strictly increasing tuples $[t_0,\dots,t_p]$, and with
augmentation sending each vertex to $1$. A weakly increasing tuple
with a repeated entry means zero. The alternating deletion formula
remains valid in the normalized quotient.

Fix a simplex $\sigma=(v_0\le\dots\le v_m)\colon\Delta[m]\to\OrdN E$
and put $T_\sigma=\{f(v_i),g(v_i):0\le i\le m\}\subseteq E$. The
indices with $v_i\in A$ form a prefix $0\le i\le r$. On that prefix
$f$ and $g$ coincide. If $r<m$, all remaining $g$-images equal a
common $b=g(v_m)$, and $f(v_r)=g(v_r)\le f(v_{r+1})\le b$. Hence
$T_\sigma$ is the ordered $f$-image list
$[f(v_0),\dots,f(v_m)]$, possibly with $b$ adjoined above. The order
embedding $T_\sigma\hookrightarrow E$ gives
$\nu M[T_\sigma]\to\Uinf{E}$.

\emph{Step 2: the simplexwise chain map.} Write $e_0,e_1$ for the
vertices and $u$ for the edge of $M[1]$, so $du=e_1-e_0$. On the tensor
basis of $M[m]\otimes M[1]$, prescribe for
$x=[i_0<\dots<i_p]$, $w_j=v_{i_j}$:
\begin{align}
 C_\sigma(x\otimes e_0)&=F(w):=[f(w_0),\dots,f(w_p)],\notag\\
 C_\sigma(x\otimes e_1)&=G(w):=[g(w_0),\dots,g(w_p)],\label{eq:prism-basis}\\
 C_\sigma(x\otimes u)&=h(w):=[f(w_0),\dots,f(w_p),g(w_p)].\notag
\end{align}
All images are weakly increasing in $T_\sigma$; each is a positive
basis element or zero. Both endpoint prescriptions are the normalized
chain maps of the monotone maps $f,g$ on vertices, hence preserve
augmentation. So $C_\sigma$ is augmentation-preserving in degree zero.

\emph{Step 3: chain identity.} The only nontrivial check is on
$x\otimes u$ with $p>0$. We need
$d h(w)=C_\sigma(d(x\otimes u))$. The left side is the alternating sum
of the $p+2$ deletions of entries of $h(w)$; the right side equals
\begin{equation}\label{eq:prism-rhs}
 \sum_{j=0}^{p-1}(-1)^j h(w_0,\dots,\widehat{w_j},\dots,w_p)
 +(-1)^p B' +(-1)^p(G(w)-F(w)),
\end{equation}
with
\[
 B:=[f(w_0),\dots,f(w_{p-1}),g(w_p)],\qquad
 B':=[f(w_0),\dots,f(w_{p-1}),g(w_{p-1})].
\]
Note $h(w_0,\dots,\widehat{w_p})=B'$. The $j$-labelled terms for
$j<p$ coincide on both sides. So it suffices to compare tails: $dh(w)$ has tail $(-1)^pB+(-1)^{p+1}F(w)$, while $C_\sigma(d(x\otimes u))$ has tail $(-1)^pB'+(-1)^p(G(w)-F(w))$. These agree iff $B-F(w)=B'+G(w)-F(w)$, i.e.\ $B-B'=G(w)$.
We verify this in the two possible cases for $w_{p-1}$.

\emph{Case $w_{p-1}\in A$.} Then $w_0,\dots,w_{p-1}\in A$ (downward
closed), so $f(w_j)=g(w_j)$ for $j<p$. If also $w_p\in A$, then
$B=G(w)$, and $B'$ has repeated last two entries, so $B'=0$. If
$w_p\notin A$, then $f(w_j)=g(w_j)$ for $j<p$ gives $B=G(w)$, and
$g(w_{p-1})=f(w_{p-1})$ makes the last two entries of $B'$ equal, so
$B'=0$. Either way $B-B'=G(w)$.

\emph{Case $w_{p-1}\notin A$.} Since $A$ is a sieve and
$w_{p-1}\le w_p$, also $w_p\notin A$. Constancy of $g$ on
$E\setminus A$ gives $g(w_{p-1})=g(w_p)=b$, so $B=B'$ and
$G(w)$ has repeated last two entries, so $G(w)=0$. Again $B-B'=G(w)$.

The case $p=0$ reduces to $d[f(w_0),g(w_0)]=[g(w_0)]-[f(w_0)]$. This
proves \eqref{eq:prism-basis} is a positive augmentation-preserving
chain map in every degree. The strong Steiner tensor identification
\eqref{eq:steiner-tensor} gives the strict functor
\begin{equation}\label{eq:prism-simplex-cylinder}
 \Orient{m}\otimes\Disk{1}\cong\nu(M[m]\otimes M[1])
   \xrightarrow{\nu C_\sigma}\nu M[T_\sigma]
   \longrightarrow\Uinf{E}.
\end{equation}

\emph{Step 4: naturality in the simplex.} Let
$\alpha\colon[q]\to[m]$ be monotone and $\rho=\sigma\alpha$. The
embeddings of simplex values give $j\colon T_\rho\hookrightarrow T_\sigma$
as an ordered subset. On the tensor basis we claim
\begin{equation}\label{eq:prism-naturality}
 M(j)C_\rho=C_\sigma(M(\alpha)\otimes\id_{M[1]}).
\end{equation}
Fix a basis tuple $[a_0<\dots<a_p]$ in $M[q]$. If $\alpha$ is
injective on it, both sides equal the same tuple in
\eqref{eq:prism-basis} selected by the indices
$\alpha(a_0),\dots,\alpha(a_p)$, on tensoring with $e_0$, $e_1$, or
$u$. If $\alpha$ is not injective on the tuple, then the right side
is $0$ by normalization. On the left, equal selected indices yield
repeated $f$-images in the $e_0$ and $u$ prescriptions, and repeated
$g$-images in the $e_1$ prescription, so all three images are $0$.
These cases include faces, degeneracies, and every composite;
naturality of the strong Steiner identification and functoriality of
$\nu$ turn \eqref{eq:prism-naturality} into an equality of strict
functors after mapping into $\Uinf{E}$.

Note: the vanishing of $h(w)$ as a \emph{chain} does not collapse
$C_\sigma$ to identity on a trivial cell. When the top entry of a
$q$-cell is zero (with $q>0$), the two $(q-1)$-entries of its cell
table coincide, so the induced cell is the identity on a common
$(q-1)$-cell. That common cell need not itself be an identity.
Equation~\eqref{eq:prism-naturality} compares the whole chain map
degree-by-degree, so it captures agreement on these retained
boundaries as well.

\emph{Step 5: assembly.} The categorification formula
\eqref{eq:categorification-colimit}, together with cocontinuity of the
Gray tensor in its first variable gives
\[
 \Uinf{E}\otimes\Disk{1}
 \cong\colim_{\sigma\colon\Delta[m]\to\OrdN E}
       \bigl(\Orient{m}\otimes\Disk{1}\bigr).
\]
The compatible maps \eqref{eq:prism-simplex-cylinder} consequently
induce $P^\infty_{f,g}\colon\Uinf{E}\otimes\Disk{1}\to\Uinf{E}$.
The endpoint maps are $U^\infty(f)$ and $U^\infty(g)$ by their
simplexwise formulas. The colimit is taken in strict
$\omega$-categories; tensor cocontinuity suffices.

\emph{Step 6: stationarity.} On a simplex
$\sigma$ entirely in $A$, the maps $F$ and $G$ coincide and $h(w)=0$
for every selected tuple. Precisely, the whole chain map
$C_\sigma$ equals $F\circ(\id_{M[m]}\otimes\epsilon)$, where
$\epsilon$ is the interval augmentation
($\epsilon(e_0)=\epsilon(e_1)=1$, $\epsilon(u)=0$). Applying $\nu$
and the simplex colimit proves \eqref{eq:prism-stationarity}.

\emph{Step 7: descent to finite $n$.} For $n<\infty$, let
$q_E\colon\Uinf{E}\to\U{E}$ be the reflection unit. By
Lemma~\ref{lem:internal-truncation}, $q_EP^\infty_{f,g}$ factors
uniquely as
\[
 \Uinf{E}\otimes\Disk{1}
   \xrightarrow{q_E\otimes\id}\U{E}\otimes\Disk{1}
   \xrightarrow{P_{f,g}}\U{E}.
\]
Endpoint identities follow by precomposing with $q_E$ and using the
universal property of reflection. To verify
\eqref{eq:prism-stationarity} after reflection, precompose both sides
with $q_A\otimes\id$; the resulting equality is the $\omega$-case.
Injectivity in the bijection of Lemma~\ref{lem:internal-truncation}
gives the equality with target $\U{E}$. For $n=\infty$ no reflection
is needed. Empty $A$ or $E$ uses the empty colimit, and the statements
follow. Finally Lemma~\ref{lem:gray-nerve} gives the stated
simplicial homotopy.
\end{proof}

\subsection{Gluing a stationary cylinder through a pushout}

The stationary cylinder extends through any pushout, by transposing to
the right internal hom.

\begin{lemma}[Gluing a stationary cylinder]\label{lem:pushout-cylinder}
Let $i\colon B_0\to B$ and $a\colon B_0\to X$ be arbitrary strict
functors of $n$-categories, and form the pushout
\[
 \begin{tikzcd}
  B_0\ar[r,"i"]\ar[d,"a"']&B\ar[d,"b"]\\
  X\ar[r,"j"']&Y.
 \end{tikzcd}
\]
Suppose $F_0,F_1\colon B\to B$ satisfy $F_0i=F_1i=i$, and suppose
$P\colon B\otimes\Disk{1}\to B$ has endpoints $F_0,F_1$ and satisfies
$P(i\otimes\id)=i\pi_{B_0}$. Then there is a cylinder
$Q\colon Y\otimes\Disk{1}\to Y$ stationary on $X$, whose endpoints
$\overline F_0,\overline F_1\colon Y\to Y$ are specified by
$\overline F_\delta j=j$ and $\overline F_\delta b=bF_\delta$ for
$\delta=0,1$. Its restriction along $b\otimes\id$ is $bP$. This
construction is natural in $a\colon B_0\to X$, and its nerve gives a
simplicial homotopy between $\Street\overline F_0$ and
$\Street\overline F_1$ stationary along $\Street j$.
\end{lemma}

\begin{proof}
Let $H(Y)\in\nCat$ represent functors $(-)\otimes\Disk{1}\to Y$; this
is an $n$-category by Lemma~\ref{lem:internal-truncation} (and
automatic for $n=\infty$). The cylinders $bP\colon B\otimes\Disk{1}\to Y$
and $j\pi_X\colon X\otimes\Disk{1}\to Y$ transpose to maps
$B\to H(Y)$ and $X\to H(Y)$. That these maps agree on $B_0$ is the
identity
\[
 bi\pi_{B_0}=ja\pi_{B_0},
\]
which follows from the stationarity of $P$ and the defining relation
$ji=ba$. The pushout universal property in $\nCat$ gives a unique map
$Y\to H(Y)$ extending both; its transpose is $Q$. The endpoint
formulas and $Q(j\otimes\id)=j\pi_X$ follow from naturality of the
adjunction and the same pushout universal property. The restriction
to $B$ is $bP$ by construction. Naturality in $a$ follows because for
$X\to X'$ commuting with $a$ the two maps $Y\to H(Y')$ agree on $X$
and $B$. Lemma~\ref{lem:gray-nerve} gives the final homotopy
assertion. No injectivity, freeness, or cofibrancy on $i,a,X$ is used.
\end{proof}

\section{Labelled pieces of algebraic pushouts}
\label{sec:pieces}

We fix $1\le n\le\infty$. The labelled-piece formalism lets us compute
the fibers of the nerve of a pushout of strict $n$-categories, and it
lets us write a pushout of nerves as a union of two-piece covers, so
that a weak-equivalence conclusion on the pieces glues to the whole.

The underlying idea is a bookkeeping device. Label every object of
the target category by $0$ or $1$; the labelled formula identifies the
$0$-fiber and $1$-fiber of the pushout with pushouts of the
corresponding fibers of the legs. Two labels combine by a maximum or
minimum of monotone maps, and the two-piece structure falls out
automatically, even when the attaching functor identifies old objects
or collapses old cells to identities.

A \emph{full sub-$n$-category} of $X$ on a set of objects $S$ has
exactly those objects and contains every positive-dimensional cell
whose $0$-source and $0$-target lie in $S$. It is a \emph{sieve} if a
$1$-cell $x\to y$ with $y\in S$ forces $x\in S$, and a \emph{cosieve}
if a $1$-cell $x\to y$ with $x\in S$ forces $y\in S$. A sieve is
equivalently the fiber over $0$ of a strict functor $X\to\Disk{1}$, and
a cosieve is the fiber over $1$: the labelled object assignment extends
uniquely to a strict functor because each nonempty hom in the target is
terminal, and the sieve/cosieve condition excludes arrows labelled
$1\to 0$. Fibers so obtained are full, since all cells between objects
with the same label must map to identities at that label.

\subsection{Fibers preserve colimits}

\begin{lemma}[Fibers and objects preserve colimits]\label{lem:fibers}
For $\epsilon\in\{0,1\}$ the functor
\[
 F_\epsilon\colon\nCat/\Disk{1}\longrightarrow\nCat,\qquad
 (p\colon X\to\Disk{1})\longmapsto X_\epsilon=p^{-1}(\epsilon),
\]
preserves all small colimits. The object functor
$\Ob\colon\nCat\to\mathrm{Set}$ also preserves all small colimits.
Both hold for $n=\infty$.
\end{lemma}

\begin{proof}
Build a right adjoint $Q_0$ to $F_0$. Given $B$, place all its objects
over $0$ and adjoin a new object $*$ over $1$. Retain the homs
$B(b,b')$, and set
\[
 Q_0(B)(b,*)=\mathbf{1},\quad
 Q_0(B)(*,b)=\varnothing,\quad
 Q_0(B)(*,*)=\mathbf{1},
\]
where $\mathbf{1}$ and $\varnothing$ are terminal and initial in the
relevant dimension. All remaining compositions either have empty domain
or terminal codomain, hence are uniquely determined; the strict
$n$-category laws follow from those of $B$ or by uniqueness. For
$p\colon X\to\Disk{1}$ a functor $X_0\to B$ extends uniquely over
$\Disk{1}$ to $X\to Q_0(B)$: all objects of $X_1$ go to $*$, their
internal cells and cells from $X_0$ to $X_1$ take unique images, and no
cell goes from $X_1$ to $X_0$ since its $1$-boundary would map to an
arrow $1\to 0$. So
$\Hom_{\nCat/\Disk{1}}(X,Q_0(B))\cong\Hom_{\nCat}(X_0,B)$ and $F_0$ is
a left adjoint. The $F_1$ case uses a new initial object over $0$ with
terminal homs into $B$. Both constructions include $B=\varnothing$ and
so preserve the empty colimit.

For $\Ob$, let $K(S)$ be the ordinary chaotic category on $S$ regarded
as an $n$-category with identity cells above dimension one. Every
$\Ob X\to S$ extends uniquely to $X\to K(S)$; hence $\Ob$ is a left
adjoint.
\end{proof}

\subsection{Oriental segments and poset pieces}

\begin{lemma}[Full oriental segments]\label{lem:oriental-segments}
Let $I$ be an initial or final segment of $[m]=\{0,\dots,m\}$. If $I$
is nonempty with $q+1$ vertices, the face inclusion identifies
$\trunc\Orient{q}$ with the full sub-$n$-category of $\trunc\Orient{m}$
on $I$. If $I=\varnothing$, that full subcategory is empty.
\end{lemma}

\begin{proof}
The atoms of an oriental are indexed by strictly increasing tuples;
the $0$-source and $0$-target of the atom at $[i_0<\dots<i_p]$ are
$i_0$ and $i_p$. All cells are finite composites and identities of
atoms, and every $1$-cell has nondecreasing endpoints. Suppose a cell
has $0$-source $a$ and $0$-target $b$. Induction on the expression
shows every occurring atom has all vertices in $[a,b]$: for an atom
this is the tuple description, for a $0$-composite the factors have
endpoints $(a,c)$ and $(c,b)$ with $a\le c\le b$, for a composition
in positive dimension both factors keep the endpoints of the composite,
and identities preserve the property. If $a,b\in I$, then
$[a,b]\subseteq I$ and the expression uses only atoms of that face. So
the face generates every cell on those objects.

For finite $n\ge1$, reflection leaves objects unchanged, and every
cell of dimension $\le n$ is represented by a cell of the source. The
same argument applied to a representative shows the reflection
surjects onto the full subcategory. For injectivity, the inclusion
$I\hookrightarrow[m]$ has a monotone retraction (clamp to the last
vertex of an initial segment, or to the first of a final one), which
by cosimplicial functoriality induces a retraction on orientals and
then on reflections; the face map is injective on every cell set. The
empty case has no objects and no cells.
\end{proof}

\begin{lemma}[Poset pieces]\label{lem:poset-pieces}
There is a canonical identification $\Ob\U{P}=P$ for every poset $P$.
If $S\subseteq P$ is a sieve, the map $\U{S}\to\U{P}$ is the
inclusion of the full $0$-fiber of the membership label
$\U{P}\to\Disk{1}$. If $S$ is a cosieve, it is the inclusion of the
full $1$-fiber. These identifications are natural for maps of
labelled posets and include empty posets and empty fibers.
\end{lemma}

\begin{proof}
Use the canonical simplex presentation
\begin{equation}\label{eq:poset-simplex-colimit}
 \U{P}=\colim_{\sigma\colon\Delta[m]\to\OrdN P}\trunc\Orient{m}.
\end{equation}
By Lemma~\ref{lem:fibers} its object set is the colimit of vertex sets
$[m]$, and sending the $j$th vertex of a simplex $\sigma$ to
$\sigma(j)$ identifies it with $P$: each element occurs as a
zero-simplex, and face inclusions identify every vertex with that
occurrence.

For a sieve $S$, the characteristic map $P\to[1]$ ($0$ on $S$, $1$ on
the complement) is monotone and induces a label on $\U{P}$, because
$\U{[1]}=\Disk{1}$. The presentation \eqref{eq:poset-simplex-colimit}
is a colimit in $\nCat/\Disk{1}$ as well (slice colimits have
underlying colimits in $\nCat$). In a $\sigma$-piece the vertices
mapping to $S$ form an initial segment $I_\sigma$. By
Lemma~\ref{lem:oriental-segments} the $0$-fiber of that piece is its
truncated segment oriental. Taking fibers of the colimit commutes
with the colimit by Lemma~\ref{lem:fibers}.

The resulting colimit of segment orientals is canonically $\U{S}$:
restricting simplex segments to $S$ gives compatible maps to $\U{S}$;
each simplex in $S$ embeds fully; the composites are identities on
simplices of $S$ and on nonempty segments via the face inclusion
selecting $I_\sigma$ (a simplicial-set morphism in $\OrdN P$), while
empty segments have nothing to check. The isomorphism obtained is the
map $\U{S}\to\U{P}$ landing in its fiber. Fibers are full sieves; the
cosieve case uses label $1$ on $S$, final vertex segments, and $F_1$.
Everything commutes with maps of labelled posets.
\end{proof}

\subsection{Fibers of a labelled pushout}

\begin{proposition}[Labelled attachments]\label{prop:labelled-pushout}
Let $A\subseteq P$ be a full subposet, $a\colon\U{A}\to X$ any strict
functor, and form $Y=X\amalg_{\U{A}}\U{P}$. Suppose a monotone
$\lambda\colon P\to[1]$ and a strict functor $\xi\colon X\to\Disk{1}$
satisfy $\xi a=U(\lambda|_A)$. Write $P_\epsilon=\lambda^{-1}(\epsilon)$,
$A_\epsilon=A\cap P_\epsilon$, $X_\epsilon=\xi^{-1}(\epsilon)$. Then
the induced label $Y\to\Disk{1}$ has actual full fibers
\begin{equation}\label{eq:pushout-fiber}
 Y_\epsilon\cong X_\epsilon\amalg_{\U{A_\epsilon}}\U{P_\epsilon}.
\end{equation}
Independently of the labels,
\begin{equation}\label{eq:pushout-objects}
 \Ob Y\cong\Ob X\amalg_A P\cong\Ob X\amalg(P\setminus A).
\end{equation}
For two compatible pairs $(\lambda_i,\xi_i)$, $i=1,2$, with induced
labels $\bar\lambda_i$ on $Y$, the $0$-fibers intersect in the
$0$-fiber of $\max\circ(\bar\lambda_1,\bar\lambda_2)$, and the
$1$-fibers in the $1$-fiber of
$\min\circ(\bar\lambda_1,\bar\lambda_2)$. Formula
\eqref{eq:pushout-fiber} computes these intersections using the same
max or min on both legs.
\end{proposition}

\begin{proof}
Compatibility makes the defining pushout a pushout in
$\nCat/\Disk{1}$. Applying $F_\epsilon$ and then
Lemmas~\ref{lem:fibers} and~\ref{lem:poset-pieces} gives
\eqref{eq:pushout-fiber}. The map from that pushout into $Y$ identifies
with the inclusion of a full fiber. The object formula follows from
the object part of Lemma~\ref{lem:fibers} and
Lemma~\ref{lem:poset-pieces}: its last isomorphism uses only the
injectivity of $A\hookrightarrow P$, so old vertices of $P$ are
replaced by their images in $X$ while vertices in $P\setminus A$ remain
distinct. No injectivity of $\Ob a$ is required.

Two labels on $Y$ give $Y\to\Disk{1}\times\Disk{1}$. The monotone
functions $\max,\min\colon[1]\times[1]\to[1]$ are strict functors, so
their composites are labels. An object has maximum label $0$ iff both
labels are $0$, and minimum label $1$ iff both are $1$. Full
subcategories on the same objects coincide. The composite labels
restrict to the corresponding max/min labels on both legs, so
\eqref{eq:pushout-fiber} applies to the intersections.
\end{proof}

\begin{corollary}[Sieve and cosieve covers after attachment]
\label{cor:attachment-covers}
With the notation above, the following are canonical identifications
of subcategories of $Y$.

\textup{(i)} If $P_1,P_2$ are sieves of $P$ containing $A$ and
covering $P$, then
$Y_i=X\amalg_{\U{A}}\U{P_i}$ ($i=1,2$) are sieves covering $Y$ on
objects, and $Y_1\cap Y_2=X\amalg_{\U{A}}\U{P_1\cap P_2}$.

\textup{(ii)} If $T_1,T_2$ are cosieves of $P$ covering $P$ with
$A\subseteq T_1$ and $A\cap T_2=\varnothing$, then
$Y_1=X\amalg_{\U{A}}\U{T_1}$ and $Y_2=\U{T_2}$ are cosieves covering
$Y$ on objects, and $Y_1\cap Y_2=\U{T_1\cap T_2}$.

If $A$ is itself a sieve of $P$, then $X\to Y$ is the inclusion of a
full sieve.
\end{corollary}

\begin{proof}
For (i), label membership in $P_i$ by $0$ and label every object of
$X$ by $0$. Apply Proposition~\ref{prop:labelled-pushout} to the two
labels and their maximum. For (ii), label membership in each $T_i$ by
$1$; use constant label $1$ on $X$ for $T_1$ and constant label $0$ on
$X$ for $T_2$. These agree on the attaching source. The $1$-fibers of
the old-side labels are empty, and so is their minimum;
formula~\eqref{eq:pushout-fiber} gives $\U{T_2}$ and
$\U{T_1\cap T_2}$ exactly. In both cases \eqref{eq:pushout-objects}
proves the object cover. When $A$ is a sieve of $P$, label $A$ and
$X$ by $0$ and $P\setminus A$ by $1$: the $0$-fiber is
$X\amalg_{\U{A}}\U{A}=X$.
\end{proof}

In particular, an attaching functor may identify old objects, collapse
old cells to identities, or identify parallel old cells. None of these
affect the cover calculation, since the labels agree on every old cell
before the pushout is taken.

\subsection{Nerves of two-piece covers}

\begin{lemma}[Two-piece covers]\label{lem:nerve-cover}
Let $C_1,C_2\subseteq C$ be two full sieves (or two full cosieves)
that cover the objects of $C$. Put $C_{12}=C_1\cap C_2$. Then
\[
 \begin{tikzcd}
  \Street C_{12} \ar[r,hook] \ar[d,hook] & \Street C_2 \ar[d,hook] \\
  \Street C_1 \ar[r,hook] & \Street C
 \end{tikzcd}
\]
is an ordinary pushout of simplicial sets. All four maps are
monomorphisms, so it is a homotopy pushout.
\end{lemma}

\begin{proof}
A full inclusion gives a nerve monomorphism, and the intersection of
the two nerves is $\Street C_{12}$: a functor whose image lies in both
subcategories factorises uniquely through their full intersection. It
remains to prove every simplex $z\colon\Orient{m}\to C$ lies in one of
the two nerves. For a sieve cover choose a piece containing $z(m)$; for
$j\le m$ the oriental has an arrow $j\to m$ whose image lies in that
piece; fullness then puts every cell of the simplex there. For a
cosieve cover choose a piece containing $z(0)$ and use the arrows
$0\to j$. This handles $m=0$ as well. So the union is the whole
$\Street C$ degreewise; the intersection pushout holds because the two
pieces are simplicial subsets with intersection the third.
Monomorphy of the legs is immediate, and the homotopy-pushout
assertion follows from Lemma~\ref{lem:simplicial-gluing}.
\end{proof}

The labelled-piece machinery is now complete. Section
\ref{sec:couniversality} uses it to glue local contractions into a
couniversality statement for sieves with a right-adjoint retraction.

\section{Couniversality and the unit on posets}
\label{sec:couniversality}

Fix $n\in\{1,2,\dots\}\cup\{\infty\}$. Call a strict functor a
\emph{Thomason equivalence} if its Street nerve is a weak homotopy
equivalence. The term uses no model structure on $\nCat$. We prove
that the inclusion $A\hookrightarrow E$ of a sieve into a poset, when
it has a right-adjoint retraction, remains a Thomason equivalence
after every pushout. From this we deduce that the unit of
$c_n\dashv N_n$ on every poset is a Thomason equivalence, independently
of transfer.

A right-adjoint retraction of a poset inclusion $i\colon A\hookrightarrow E$
is a monotone $r\colon E\to A$ with $ri=\id_A$ and
\begin{equation}\label{eq:poset-adjunction}
 a\le e\iff a\le r(e)\qquad(a\in A,\ e\in E).
\end{equation}
We identify $A$ with its image. In particular $r(e)\le e$, and $A$ is
a \emph{sieve} when $e\le a\in A$ forces $e\in A$. For any attaching
functor $a\colon\U{A}\to X$, write
\[
 Y=X\amalg_{\U{A}}\U{E},\qquad
 j:X\to Y,\qquad v:\U{E}\to Y.
\]
Below, elements of $A$ are denoted $b$.

\subsection{One greatest new element}

\begin{lemma}[Greatest new element]\label{lem:greatest-new}
Let $i\colon A\hookrightarrow E$ be a sieve with a right-adjoint
retraction, and suppose $E\setminus A$ has a greatest element. Then
for every attaching functor $a$ in $Y=X\amalg_{\U{A}}\U{E}$, the map
$j\colon X\to Y$ admits a retraction $p\colon Y\to X$ with
$N_n(jp)$ and $\id_{N_nY}$ joined by a zigzag of simplicial
homotopies. Consequently $j$ is a Thomason equivalence. Neither $A$
nor $E$ needs to be finite.
\end{lemma}

\begin{proof}
Let $x$ be greatest in $E\setminus A$ and $t=r(x)\in A$. If $b\in A$,
$y\in E\setminus A$, $b\le y$, then $b\le y\le x$; by
\eqref{eq:poset-adjunction} we get $b\le t$. Define maps $E\to E$ by
\[
 k(e)=\begin{cases}e,&e\in A\\ t,&e\notin A\end{cases}
 \qquad
 g(e)=\begin{cases}e,&e\in A\\ x,&e\notin A\end{cases}.
\]
Both are monotone: old-old and new-new cases go through unchanged; an
old-new pair $e\le e'$ has $e\le t\le x$; a new-old pair cannot occur
since $A$ is a sieve. Thus
\begin{equation}\label{eq:local-zigzag}
 \id_E\le g,\qquad k\le g,
\end{equation}
and all three restrict to $\id_A$. The map $g$ is constant on
$E\setminus A$, so the relative prism (Lemma~\ref{lem:relative-prism})
applies to both $(\id_E,g)$ and $(k,g)$.

Apply Lemma~\ref{lem:pushout-cylinder} to the two comparisons in
\eqref{eq:local-zigzag}. Let $G,K\colon Y\to Y$ be the pushout
endomorphisms whose restrictions to $X$ are $j$ and whose restrictions
to $\U{E}$ are $vU(g)$ and $vU(k)$ respectively. The resulting right
Gray cylinders are stationary on $X$; their endpoint pattern is
\[
 \id_Y\longrightarrow G\longleftarrow K.
\]
By Lemma~\ref{lem:gray-nerve} this gives matching simplicial homotopies
on Street nerves.

The image of $k$ lies in $A$, so $k=i\bar k$ for some monotone
$\bar k\colon E\to A$. The maps $\id_X$ and $aU(\bar k)\colon\U{E}\to X$
agree on $\U{A}$, defining $p\colon Y\to X$ with $pj=\id_X$.
Comparing restrictions to the two pushout summands gives $jp=K$: on
$X$ both are $j$; on $\U{E}$ both are
$vU(k)=vU(i)U(\bar k)=jaU(\bar k)$. So the homotopy from $\id_Y$ to $G$
followed by the reverse of the homotopy from $jp$ to $G$ exhibits
$N_np$ as a homotopy inverse of $N_nj$. The reversal is of an ordinary
topological homotopy, not of a Gray cylinder.
\end{proof}

\subsection{Small finite posets: induction through two-piece covers}

\begin{theorem}[Couniversality]\label{thm:couniversal}
Let $i\colon A\hookrightarrow E$ be a sieve of small posets with a
right-adjoint retraction. Then $c_n\OrdN(i)$ is a couniversal
Thomason equivalence: for every $a\colon\U{A}\to X$ the canonical map
$X\to X\amalg_{\U{A}}\U{E}$ is a Thomason equivalence.
\end{theorem}

\begin{proof}
\emph{Finite case.} Induct on $|E\setminus A|$, simultaneously for all
$X$ and $a$. If $E\setminus A$ is empty, $j$ is an isomorphism. If
$E\setminus A$ has a greatest element, use Lemma~\ref{lem:greatest-new}.

Otherwise $E\setminus A$ has two distinct maximal elements
$x_1,x_2$ (a finite poset with a unique maximal element has that
element as its greatest). Each $x_i$ is maximal in $E$: an element
above a new element cannot be in the sieve $A$. Put
\[
 E_1=E\setminus\{x_1\},\quad
 E_2=E\setminus\{x_2\},\quad
 E_{12}=E\setminus\{x_1,x_2\}.
\]
These are sieves of $E$ containing $A$, with $E_1\cup E_2=E$ and
$E_1\cap E_2=E_{12}$. The restriction of $r$ to each $E_T$ takes
values in $A$ and satisfies \eqref{eq:poset-adjunction}; each
complement $E_T\setminus A$ is smaller. Put
$Y_T=X\amalg_{\U{A}}\U{E_T}$, $j_T\colon X\to Y_T$. By induction each
$N_n(j_T)$ is a weak homotopy equivalence.

Corollary~\ref{cor:attachment-covers}(i), applied to the sieves
$E_1,E_2$ of $E$, identifies $Y_i\to Y$ as full sieve inclusions;
their intersection is $Y_{12}$; and they cover $Y$ on objects.
Lemma~\ref{lem:nerve-cover} then exhibits the bottom pushout of the
commuting map of spans
\[
 \begin{tikzcd}[column sep=large]
  \Street X \arrow[d,"\Street j_1"'] &
  \Street X \arrow[l,equal] \arrow[r,equal] \arrow[d,"\Street j_{12}"] &
  \Street X \arrow[d,"\Street j_2"]\\
  \Street Y_1 &
  \Street Y_{12} \arrow[l,hook] \arrow[r,hook] &
  \Street Y_2
 \end{tikzcd}
\]
as $\Street Y$. The vertical maps are weak equivalences by induction;
the horizontal legs are monomorphisms. Lemma~\ref{lem:simplicial-gluing}
makes the induced map on pushouts a weak equivalence. The top pushout
is $\Street X$ and the bottom $\Street Y$, so the map in question is
$\Street j$. The finite induction is complete; no compatibility between
local cylinders on different pieces is used.

\emph{Arbitrary posets.} Write $q=ir\colon E\to E$; then $q^2=q$.
Let $\mathcal F$ be the collection of finite subsets $F\subseteq E$
with $q(F)\subseteq F$. It is filtered under inclusion (it contains
$\varnothing$ and is closed under finite unions), and every finite
$T\subseteq E$ is contained in the finite stable $T\cup q(T)$. Give
each $F$ the induced order and put $A_F=A\cap F$. Then $A_F$ is a
sieve of $F$ and $r(F)\subseteq A_F$, so $r_F\colon F\to A_F$ is a
right-adjoint retraction.

For each $F$ put $Y_F=X\amalg_{\U{A_F}}\U{F}$, $j_F\colon X\to Y_F$.
Each $j_F$ is a Thomason equivalence by the finite case. Inclusions
$F\subseteq F'$ give compatible transitions $Y_F\to Y_{F'}$ under
$X$. Ordinary nerve simplices have finite vertex support, so
\[
 \OrdN E=\colim_{F\in\mathcal F}\OrdN F,\qquad
 \OrdN A=\colim_{F\in\mathcal F}\OrdN A_F.
\]
The left adjoint $c_n$ preserves colimits, so colimits commute:
\[
 \colim_{F\in\mathcal F}Y_F\cong Y=X\amalg_{\U{A}}\U{E}.
\]
Under this identification $\colim j_F=j$. By Lemma~\ref{lem:filtered},
$N_n$ preserves these filtered colimits and weak homotopy equivalences
are closed under filtered colimits. Hence $N_nj$ is a weak homotopy
equivalence. The same proof applies verbatim to $n=\infty$.
\end{proof}

\subsection{The unit on posets}

The following is known
\cite[Cor.~10.11]{AraMaltsiniotis2015},
\cite[Thm.~6.9]{Gagna2018},
\cite[Prop.~9.2.3]{Ara2023}; we include a prism-based proof.

\begin{proposition}[The unit on every poset]\label{prop:poset-unit}
For every small poset $S$ the adjunction unit
$\eta_S\colon\OrdN S\to\Street\U{S}$ is a weak homotopy equivalence.
This is natural in $S$ and holds for every finite $n\ge1$ and for
$n=\infty$.
\end{proposition}

\begin{proof}
\emph{Finite case.} Induct on $|S|$. For $S=\varnothing$ both sides
are empty and $\eta_S$ is an isomorphism. If $S$ has a greatest
element $x$, the pointwise inequality $\id_S\le\mathrm{const}_x$
contracts $\OrdN S$. Lemma~\ref{lem:relative-prism}, with old sieve
$\varnothing$, gives a right cylinder from $\id_{\U{S}}$ to
$c_n\OrdN(\mathrm{const}_x)$, and the latter factors through
$\U{\{x\}}=\Orient{0}$, the terminal strict $n$-category.
Lemma~\ref{lem:gray-nerve} contracts $\Street\U{S}$. Both sides are
nonempty contractible, so $\eta_S$ is a weak homotopy equivalence.

Otherwise choose two distinct maximal elements $x_1,x_2$ of $S$ and
put $S_i=S\setminus\{x_i\}$, $S_{12}=S\setminus\{x_1,x_2\}$. These
are sieves, the two single deletions cover $S$, and all three posets
are smaller. Their ordinary nerves cover $\OrdN S$: a simplex belongs
to a sieve containing its last vertex. Lemmas~\ref{lem:poset-pieces}
and~\ref{lem:nerve-cover} give a full sieve cover of $\U{S}$ and of
its Street nerve, with the joint zero label cutting the intersection
out as $\U{S_{12}}$. Naturality of the unit gives a commuting map of
spans
\[
 \begin{tikzcd}[column sep=large]
  \OrdN S_1 \arrow[d,"\eta_{S_1}"'] &
  \OrdN S_{12} \arrow[l,hook] \arrow[r,hook]
              \arrow[d,"\eta_{S_{12}}"] &
  \OrdN S_2 \arrow[d,"\eta_{S_2}"]\\
  \Street\U{S_1} &
  \Street\U{S_{12}} \arrow[l,hook] \arrow[r,hook] &
  \Street\U{S_2}.
 \end{tikzcd}
\]
The vertical maps are weak equivalences by induction; the horizontal
legs are monomorphisms. Lemma~\ref{lem:simplicial-gluing} makes the
induced map on pushouts a weak equivalence. Under the cover
identifications this is exactly $\eta_S$: on each $\OrdN S_i$ it is
that unit by naturality. This proves the finite case.

\emph{Arbitrary posets.} Every poset is the filtered union of its
finite full subposets. The ordinary nerve preserves this union since
each simplex has finite support; $c_n$ preserves the resulting colimit;
$N_n$ preserves the resulting filtered colimit by
Lemma~\ref{lem:filtered}. Naturality identifies $\eta_S$ with the
filtered colimit of the units on the finite full subposets.
Filtered-colimit closure of weak homotopy equivalences gives the
result. Only the prism, cover, and gluing lemmas are used; the proof
precedes and is independent of transfer.
\end{proof}

\section{Comparison for subdivided attachments}
\label{sec:attachments}

We compare an ordinary pushout of Street nerves with the Street nerve
of an actual attachment. Attaching functors are arbitrary; they may
identify old objects and cells. The comparison supplies both the
acyclicity of horn attachments and the preservation of weak
equivalences under boundary attachments.

The strategy follows Thomason~\cite[Proposition~4.3]{Thomason1980}.
Let $A\subseteq B$ be a sieve of posets whose inclusion into its
upward closure $Z$ has a right-adjoint retraction.
Couniversality (Theorem~\ref{thm:couniversal}) controls the attachment
over $Z$; the two-piece cosieve cover with $B\setminus A$ then adds
the rest of $B$. After proving this general comparison, we identify
the twice-subdivided boundaries and horns as poset pairs with these
properties.

\subsection{The attachment comparison}

\begin{proposition}[Attachment comparison]
\label{prop:attachment-comparison}
Let $A\subseteq B$ be a sieve of small posets and $Z$ its upward
closure in $B$, with $A\hookrightarrow Z$ admitting a right-adjoint
retraction. For every $a\colon\U{A}\to X$ in $\nCat$, put
\[
 V_B(X)=X\amalg_{\U{A}}\U{B},\qquad
 P_B(X)=\Street X\amalg_{\Street\U{A}}\Street\U{B}.
\]
Then
\begin{equation}\label{eq:attachment-comparison}
 \gamma_{B,X}\colon P_B(X)\longrightarrow\Street V_B(X)
\end{equation}
is a simplicial weak equivalence. The map
$\Street\U{A}\to\Street\U{B}$ is a monomorphism. The comparison is
natural in every $f\colon X\to X'$ under $\U{A}$.
\end{proposition}

\begin{proof}
\emph{Step 1: attachment over $Z$.} Put
$V_Z(X)=X\amalg_{\U{A}}\U{Z}$ and
$P_Z(X)=\Street X\amalg_{\Street\U{A}}\Street\U{Z}$.
Theorem~\ref{thm:couniversal} applied to $A\hookrightarrow Z$ gives
$X\to V_Z(X)\in W_n$. Applying it with old target $\U{A}$ gives
$\U{A}\to\U{Z}\in W_n$. Since $A$ is a sieve in $Z$,
Lemma~\ref{lem:poset-pieces} identifies $\U{A}\to\U{Z}$ with an actual
full inclusion; its Street nerve is monomorphic and a weak equivalence,
hence a trivial cofibration. Its pushout $\Street X\to P_Z(X)$ is
therefore a weak equivalence. The canonical triangle
\[
 \begin{tikzcd}[column sep=large]
  \Street X \arrow[r] \arrow[dr] & P_Z(X) \arrow[d,"\gamma_{Z,X}"]\\
  & \Street V_Z(X)
 \end{tikzcd}
\]
then has $\gamma_{Z,X}$ a weak equivalence by two-out-of-three.

\emph{Step 2: adding the rest of $B$.} Write
$C=B\setminus A$ and $T=Z\setminus A=Z\cap C$. Both $Z$ and $C$ are
cosieves in $B$ and they cover $B$: an element outside $C$ belongs to
$A\subseteq Z$. Their intersection is $T$. Lemma~\ref{lem:poset-pieces}
therefore gives cosieves $\U{Z},\U{C}\subseteq\U{B}$ with intersection
$\U{T}$. Apply Corollary~\ref{cor:attachment-covers}(ii) with $P=B$,
$T_1=Z$, $T_2=C$; its remaining hypotheses hold ( $A\subseteq Z$,
$A\cap C=\varnothing$ ). The canonical maps identify
\begin{equation}\label{eq:attachment-fibers}
 V_Z(X),\ \U{C}\ \subseteq\ V_B(X),\qquad
 V_Z(X)\cap\U{C}=\U{T}
\end{equation}
as full cosieves and their full intersection. These two cosieves cover
all objects of $V_B(X)$; the corollary applies to the arbitrary
functor $a$, including its identifications of old objects and cells.

Apply Lemma~\ref{lem:nerve-cover} to the two cosieve covers just
obtained. It gives ordinary simplicial pushouts
\begin{align}
 \Street\U{B}
   &=\Street\U{Z}\amalg_{\Street\U{T}}\Street\U{C},
   \label{eq:attachment-source-cover}\\
 \Street V_B(X)
   &=\Street V_Z(X)\amalg_{\Street\U{T}}\Street\U{C}.
   \label{eq:attachment-target-cover}
\end{align}
All maps from the intersections to the pieces are monomorphisms.
Reassociating the pushout defining $P_B(X)$ via
\eqref{eq:attachment-source-cover} gives
$P_B(X)=P_Z(X)\amalg_{\Street\U{T}}\Street\U{C}$. Under these
identifications the comparison \eqref{eq:attachment-comparison} is the
map induced by $\gamma_{Z,X}$ and by $\id_{\Street\U{C}}$. In
particular the square
\[
 \begin{tikzcd}[column sep=large]
  P_Z(X) \arrow[r,hook] \arrow[d,"\gamma_{Z,X}"'] &
  P_B(X) \arrow[d,"\gamma_{B,X}"]\\
  \Street V_Z(X) \arrow[r,hook] & \Street V_B(X)
 \end{tikzcd}
\]
is a pushout: $\Street V_Z(X)\amalg_{P_Z(X)}P_B(X)$ equals
$\Street V_Z(X)\amalg_{\Street\U{T}}\Street\U{C}$. The top horizontal
map is the cobase change of the specific monomorphism
$\Street\U{T}\hookrightarrow\Street\U{C}$. Simplicial left
properness, recorded in Lemma~\ref{lem:simplicial-gluing}, makes
$\gamma_{B,X}$ a weak equivalence. Neither $\Street\U{A}\to\Street X$
nor $\Street\U{T}\to P_Z(X)$ needs to be monomorphic.

\emph{Step 3: monomorphy and naturality.}
That $\Street\U{A}\to\Street\U{B}$ is monic follows directly from the
sieve identification in Lemma~\ref{lem:poset-pieces}. Naturality:
$\gamma_{B,X}$ is defined by canonical maps from $\Street X$ and
$\Street\U{B}$; for $f\colon X\to X'$ under $\U{A}$ these commute with
$\Street f$ and the induced pushout functor
$V_B(X)\to V_B(X')$, so the pushout universal property gives the
strict square
\[
 \begin{tikzcd}[column sep=large]
  P_B(X) \arrow[r,"\gamma_{B,X}"] \arrow[d] &
  \Street V_B(X) \arrow[d]\\
  P_B(X') \arrow[r,"\gamma_{B,X'}"'] & \Street V_B(X').
 \end{tikzcd}
\]
\end{proof}

\subsection{The twice-subdivided boundary and horn}

\begin{lemma}[The subdivision posets]\label{lem:subdivision-posets}
Let $d\colon K\hookrightarrow\Delta[m]$ be a boundary inclusion
($m\ge0$) or a horn inclusion $\Lambda^k[m]\hookrightarrow\Delta[m]$
($m\ge1$, $0\le k\le m$). There exist finite posets $A\subseteq B$ and
a canonical identification $\Sd^2d=(\OrdN A\hookrightarrow\OrdN B)$.
$A$ is a sieve in $B$; its upward closure $Z$ in $B$ is a cosieve,
and $A\hookrightarrow Z$ has a right-adjoint retraction.
\end{lemma}

\begin{proof}
Put $M=\{0,\dots,m\}$, $P$ the poset of nonempty subsets of $M$
under inclusion. The subposet $P_K$ of faces belonging to $K$ is
\[
 P_K=\begin{cases}
  \{F:\varnothing\neq F\subsetneq M\},&K=\partial\Delta[m],\\
  \{F:\varnothing\neq F\subseteq M,\ M\setminus\{k\}\nsubseteq F\},
    &K=\Lambda^k[m].
 \end{cases}
\]
For a horn, the excluded faces are $M$ and $M\setminus\{k\}$, exactly
those containing $M\setminus\{k\}$; $P_K$ is downward closed.

Barycentric subdivision of an ordered simplicial complex has a vertex
per nonempty face and a nondegenerate simplex per strict chain of
faces. Hence $\Sd\Delta[m]=\OrdN P$ and $\Sd K=\OrdN P_K$; the
identifications agree on every face and glue over $K$. The
nondegenerate simplices of $\OrdN P$ are nonempty chains in $P$ with
face given by deletion. Applying the description again gives
\[
 B=\{\sigma:\sigma\text{ a nonempty chain in }P\},\qquad
 A=\{\sigma\in B:\sigma\subseteq P_K\},\qquad
 \sigma\le\tau\iff\sigma\subseteq\tau.
\]
This proves the claimed identifications as simplicial sets, including
degeneracies, and identifies the inclusion.

Every nonempty subchain of a chain in $A$ again belongs to $A$, so $A$
is a sieve of $B$. Its upward closure is
$Z=\{\sigma\in B:\sigma\cap P_K\neq\varnothing\}$: for the nontrivial
direction, a face $F\in\sigma\cap P_K$ gives $\{F\}\in A$ below
$\sigma$; conversely a chain $\sigma$ below some $\tau\in A$ must
contain the members of $\tau$, so $\sigma\cap P_K\neq\varnothing$. Define
\[
 r\colon Z\longrightarrow A,\qquad r(\sigma)=\sigma\cap P_K.
\]
This is a nonempty chain (contains $\sigma\cap P_K$ as its own bottom
chain), monotone, and fixes $A$. For $\alpha\in A$, $\sigma\in Z$:
$\alpha\subseteq\sigma\iff\alpha\subseteq\sigma\cap P_K=r(\sigma)$,
which is right adjunction.

For $m=0$, $\partial\Delta[0]=\varnothing$, so $B$ is a singleton,
$A=Z=\varnothing$, and the adjunction is the identity of the empty
poset. For a one-dimensional horn, $P_K=\{\{k\}\}$, so $A$ is a
singleton and $Z$ consists of chains containing $\{k\}$. These cases
are included in the formulas above; there are no zero-dimensional
horn generators.
\end{proof}

\begin{remark}
For the zero-dimensional boundary $A=Z=T=\varnothing$ and $B=C$ is a
singleton. So $V_Z(X)=X$ and $\gamma_{Z,X}=\id$; the two cosieves of
$V_B(X)=X\amalg\U{B}$ are disjoint. The comparison is the isomorphism
$\Street X\amalg\Delta[0]\cong\Street(X\amalg\U{B})$.
\end{remark}

\subsection{Horn attachments are acyclic}

\begin{corollary}[Horn acyclicity]\label{cor:horn-acyclic}
For every horn inclusion $d\in J$ and every attaching target, every
pushout of $L_nd$ lies in $W_n$.
\end{corollary}

\begin{proof}
Write $L_nd$ as $\U{A}\to\U{B}$ via Lemma~\ref{lem:subdivision-posets}.
The nerve inclusion $\OrdN A\to\OrdN B$ is a weak equivalence: the horn
inclusion is a simplicial weak equivalence, and subdivision preserves
weak equivalences by two-out-of-three from the objectwise
$\Sd\to\id$ \cite[Theorem~4.5]{AraMaltsiniotis2014}. The adjunction
unit gives a commuting square
\[
 \begin{tikzcd}[column sep=large]
  \OrdN A \arrow[r] \arrow[d] & \OrdN B \arrow[d]\\
  \Street\U{A} \arrow[r] & \Street\U{B}
 \end{tikzcd}
\]
whose vertical maps are weak equivalences by
Proposition~\ref{prop:poset-unit}. Two-out-of-three makes the lower
map a weak equivalence; by Proposition~\ref{prop:attachment-comparison}
it is monic. So it is a trivial cofibration. For any attaching target
$\U{A}\to X$ the pushout $\Street X\to P_B(X)$ is a weak equivalence.
The composite
\[
 \Street X\longrightarrow P_B(X)\xrightarrow{\gamma_{B,X}}\Street V_B(X)
\]
is the nerve of the attachment $X\to V_B(X)$, and both factors are
weak equivalences; the attachment belongs to $W_n$.
\end{proof}

\begin{corollary}[Invariance under attachment]
\label{cor:attachment-invariance}
Let $d\in I\cup J$, write $L_nd$ as $\U{A}\to\U{B}$ via
Lemma~\ref{lem:subdivision-posets}, and let $f\colon X\to X'\in W_n$.
For every $a\colon\U{A}\to X$, the induced functor
\[
 X\amalg_{\U{A}}\U{B}\longrightarrow X'\amalg_{\U{A}}\U{B}
\]
(the second attaching functor is $fa$) belongs to $W_n$.
\end{corollary}

\begin{proof}
$\Street X\to P_B(X)$ is monomorphic, being the cobase change of
$\Street\U{A}\hookrightarrow\Street\U{B}$. There is a canonical
pushout identification $P_B(X')=\Street X'\amalg_{\Street X}P_B(X)$.
Simplicial left properness makes $P_B(X)\to P_B(X')$ a weak
equivalence, since $\Street f$ is one. In the naturality square of
Proposition~\ref{prop:attachment-comparison}, both horizontal maps are
weak equivalences; two-out-of-three makes the right vertical map, the
nerve of the asserted functor, a weak equivalence.
\end{proof}

The comparison and invariance leave the model-theoretic inputs in
place. Section~\ref{sec:transfer} assembles them into the model
structure and the Quillen equivalence.

\section{The model structure and the Quillen equivalence}
\label{sec:transfer}

Fix $n\in\{1,2,\dots\}\cup\{\infty\}$. Corollary~\ref{cor:horn-acyclic}
supplies acyclic horn attachments; Corollary~\ref{cor:attachment-invariance}
supplies invariance under boundary attachment. We first extend the
acyclicity through transfinite compositions, then build the model
structure by the small object argument, prove properness, and finish
the Quillen equivalence by checking the unit on an arbitrary simplicial
set.

In plain terms, a model structure requires two weak factorization
systems and compatibility of the three classes with each other. The
small object argument builds each factorization system one generating
attachment at a time. The inputs from Section~\ref{sec:attachments}
are exactly what makes the horn attachments register as weak
equivalences and what makes the boundary attachments preserve weak
equivalences under cobase change. Without those two inputs the
transferred classes would fail the model axioms.

\subsection{The simplicial inputs}

Write
\[
 L_n=c_n\Sd^2,\qquad R_n=\Ex^2\Street,\qquad
 L_n\dashv R_n.
\]
The Kan--Quillen model structure on $\sSet$ has weak equivalences
$W_{\mathrm{KQ}}$, fibrations $\mathrm{Fib}_{\mathrm{KQ}}$, and
generating sets
\[
 I=\{\partial\Delta[m]\hookrightarrow\Delta[m]:m\ge0\},\qquad
 J=\{\Lambda^k[m]\hookrightarrow\Delta[m]:m\ge1,\ 0\le k\le m\}.
\]
In particular $\partial\Delta[0]=\varnothing$.

The last-vertex transformation $\ell\colon\Sd\to\id$ is an objectwise
weak equivalence \cite[Theorem~4.5]{AraMaltsiniotis2014}; its mate
$j\colon\id\to\Ex$ is also objectwise \cite[Theorem~III.4.6]{GoerssJardine1999}.
Both hold unconditionally. Naturality of $j$ gives
$j_{K'}f=(\Ex f)j_K$ for any $f\colon K\to K'$, so two-out-of-three
shows that $\Ex$ preserves and reflects $W_{\mathrm{KQ}}$. The same
for $\ell$ and $\Sd$. Hence the two descriptions of $W_n$ in
\[
 W_n=\Street^{-1}(W_{\mathrm{KQ}})
     =R_n^{-1}(W_{\mathrm{KQ}}),\qquad
 F_n=R_n^{-1}(\mathrm{Fib}_{\mathrm{KQ}}),\qquad
 C_n={}^\perp(F_n\cap W_n)
\]
agree. The class $W_n$ has two-out-of-three and is closed under
retracts. By Lemma~\ref{lem:filtered} it is also closed under filtered
colimits of arrows, without any injectivity of transitions.

For a set $\mathcal S$ of maps, write
$\mathcal S\text{-inj}$ for the maps with the right lifting property
against $\mathcal S$, and $\mathcal S\text{-cof}={}^\perp(\mathcal S\text{-inj})$.
A relative $\mathcal S$-cell map is a transfinite composite of pushouts
of coproducts of members of $\mathcal S$.

\subsection{Transfinite horn attachments}

\begin{lemma}[Transfinite horn attachments]\label{lem:transfinite-horns}
Every relative $L_nJ$-cell map lies in $W_n$.
\end{lemma}

\begin{proof}
Corollary~\ref{cor:horn-acyclic} proves one-attachment acyclicity
with arbitrary target. A set of simultaneous attachments may be well
ordered: at each stage map into the original target followed by the
inclusion of the current stage. The universal property of the resulting
colimit is the pushout of the coproduct. It suffices to handle a
continuous ordinal sequence $(X_\alpha)_{\alpha\le\lambda}$ in which
each successor is a single attachment.

By transfinite induction $X_0\to X_\alpha\in W_n$ for every $\alpha$.
Base: identity. Successor: compose with the weak equivalence from
Corollary~\ref{cor:horn-acyclic}. Nonzero limit $\beta$: the ordinal
of stages $\alpha<\beta$ is filtered; apply Lemma~\ref{lem:filtered}
to the diagram of arrows $X_0\to X_\alpha$. Its colimit is
$X_0\to\colim_{\alpha<\beta}X_\alpha=X_\beta$ (the colimit of the
constant source diagram is $X_0$).
\end{proof}

\subsection{The model structure}

\begin{proposition}[Transferred model structure]\label{prop:model-structure}
The classes $(C_n,W_n,F_n)$ form a combinatorial model structure on
$\nCat$, cofibrantly generated by $(L_nI,L_nJ)$.
\end{proposition}

\begin{proof}
The underlying category is locally presentable, hence complete and
cocomplete, by Lemma~\ref{lem:filtered}. Choose an infinite regular
cardinal $\kappa$ above the presentability bound of every domain in
$\mathcal S=L_nI$ or $L_nJ$ (exists by local presentability, since
$\mathcal S$ is a set).

\emph{The small-object argument.} Given $X\to Y$, set $X_0=X$. At
stage $\alpha+1$ attach to $X_\alpha$ one copy of the codomain of each
member of $\mathcal S$ for every commutative square from that member
to $X_\alpha\to Y$; this is a set of squares (local smallness). Use
colimits at limit stages. The result is
$X\xrightarrow{i}X_\kappa\xrightarrow{p}Y$. Here $i$ is a relative
$\mathcal S$-cell map and $p\in\mathcal S\text{-inj}$: any map from a
generating domain to $X_\kappa$ factors through some $X_\alpha$
($\kappa$ is $\kappa$-filtered), and its lifting square was attached at
stage $\alpha+1$, supplying the lift.

Pushouts, transfinite composites, and retracts of maps with a fixed
left lifting property retain that property, so every relative
$\mathcal S$-cell map lies in $\mathcal S\text{-cof}$. Conversely if
$u\in\mathcal S\text{-cof}$, factor as
$A\xrightarrow{i}Z\xrightarrow{p}B$ by the construction above; the
square with top $i$, left $u$, right $p$, bottom $\id_B$ has a diagonal
$s\colon B\to Z$. This gives $su=i$, $ps=\id_B$. Thus $u$ is a retract
of $i$ in the arrow category with fixed source. Hence
\[
 (\mathcal S\text{-cof},\mathcal S\text{-inj})
\]
is a weak factorization system; its left class is exactly the retracts
of relative $\mathcal S$-cell maps.

\emph{Lifting characterizations.} The adjunction identifies lifting
squares and their fillers, so
\[
 (L_nI)\text{-inj}
   =R_n^{-1}(I\text{-inj})=F_n\cap W_n,\qquad
 (L_nJ)\text{-inj}
   =R_n^{-1}(J\text{-inj})=F_n.
\]
(Here $I\text{-inj}$ in $\sSet$ is trivial Kan fibration $=W_{\mathrm{KQ}}\cap\mathrm{Fib}_{\mathrm{KQ}}$;
$J\text{-inj}$ is $\mathrm{Fib}_{\mathrm{KQ}}$.) Thus $(C_n,F_n\cap W_n)$
is a weak factorization system.

\emph{Second factorization system.} Put $\mathcal D=(L_nJ)\text{-cof}$.
Because $F_n\cap W_n\subseteq F_n$, we get $\mathcal D\subseteq C_n$.
Lemma~\ref{lem:transfinite-horns} and retract closure also give
$\mathcal D\subseteq W_n$. For the reverse inclusion, take
$u\colon A\to B\in C_n\cap W_n$ and factor by the second argument as
$A\xrightarrow{i}Z\xrightarrow{p}B$ with $i\in\mathcal D$,
$p\in F_n$. Then $i\in W_n$ and $u=pi\in W_n$, so $p\in F_n\cap W_n$ by
two-out-of-three. Lifting of $u$ against $p$ supplies
$s\colon B\to Z$ with $su=i$, $ps=\id_B$. The fixed-source retract
puts $u\in\mathcal D$. Hence \(\mathcal D=C_n\cap W_n\), so
$(C_n\cap W_n,F_n)$ is a weak factorization system. Model axioms are
complete: two-out-of-three and retract for $W_n$, and both weak
factorization systems, on a bicomplete category; local presentability
and the displayed generating sets make it combinatorial.
\end{proof}

\subsection{Properness}

\begin{proposition}[Properness]\label{prop:properness}
The model structure of Proposition~\ref{prop:model-structure} is left
and right proper.
\end{proposition}

\begin{proof}
\emph{Right properness.} Let $p\colon Y\to Z\in F_n$ and
$w\colon Z'\to Z\in W_n$. The right adjoint $R_n$ carries the pullback
$Y\times_Z Z'$ to the simplicial pullback
$R_nY\times_{R_nZ}R_nZ'$ (right adjoints commute with limits). Its map
to $R_nY$ is a weak equivalence by right properness of the Kan--Quillen
structure, since $R_np$ is a Kan fibration and $R_nw$ a weak
equivalence. So $Y\times_Z Z'\to Y\in W_n$.

\emph{Left properness.} First take $i\colon X\to Y$ a relative
$L_nI$-cell map and $w\colon X\to X'\in W_n$. Write $i$ as a continuous
sequence of individual boundary attachments $X_\alpha$ starting at $X$,
and put $X'_\alpha=X'\amalg_X X_\alpha$. Inductively,
$X_\alpha\to X'_\alpha\in W_n$: base is $w$; at a successor stage the
second attachment has attaching map followed by
$X_\alpha\to X'_\alpha$, so Corollary~\ref{cor:attachment-invariance}
proves the step; at a nonzero limit, Lemma~\ref{lem:filtered} gives the
statement. So $Y\to X'\amalg_XY\in W_n$.

For general $i\in C_n$: the first small object factorization and its
lifting retract (from the proof of Proposition~\ref{prop:model-structure})
give $i$ a retract of a relative $L_nI$-cell $j\colon X\to Z$ with
the same source: $s\colon Y\to Z$, $p\colon Z\to Y$, $si=j$, $pj=i$,
$ps=\id_Y$. Cobase change along $w$ gives matching $s',p'$ between
$X'\amalg_XY$ and $X'\amalg_XZ$ with $p's'=\id$. So
$Y\to X'\amalg_XY$ is a retract of $Z\to X'\amalg_XZ$, which is in
$W_n$ by the previous paragraph. Both properness arguments apply to
arbitrary objects; no cofibrancy or fibrancy is used.
\end{proof}

\subsection{The unit after two subdivisions}

Let $\eta_T\colon T\to\Street c_nT$ denote the unit of $c_n\dashv N_n$.
The poset case is Proposition~\ref{prop:poset-unit}. The next
proposition extends to all simplicial sets.

\begin{proposition}[The subdivided unit]\label{prop:subdivided-unit}
For every simplicial set $K$, the map
\begin{equation}\label{eq:subdivided-unit}
 \theta_K=\eta_{\Sd^2K}\colon\Sd^2K\longrightarrow\Street L_nK
\end{equation}
is a weak equivalence.
\end{proposition}

\begin{proof}
For $K=\Delta[m]$ and $K=\partial\Delta[m]$,
Lemma~\ref{lem:subdivision-posets} identifies $\Sd^2K$ with the
ordinary nerve of a poset; the assertion is
Proposition~\ref{prop:poset-unit}. For $K=\varnothing$, both sides are
empty.

Every simplicial set is obtained from $\varnothing$ by a continuous
transfinite sequence of boundary attachments: order nondegenerate
simplices by dimension and well-order those in each dimension; the
boundary of a simplex maps into the already-constructed stage. The
attaching map may identify vertices or faces, or send faces to
degenerate simplices; the construction still recovers $K$ by the
unique expression of each simplex as a degeneration of a nondegenerate
one.

Consider a successor step $K_+=K_0\amalg_{\partial\Delta[m]}\Delta[m]$
and assume the assertion for $K_0$. Put
\[
 V=\Sd^2K_0,\quad A=\Sd^2\partial\Delta[m],\quad B=\Sd^2\Delta[m].
\]
Since subdivision is a left adjoint,
$\Sd^2K_+=V\amalg_AB$. Naturality of $\eta$ gives a map
\begin{equation}\label{eq:unit-gluing-map}
 q\colon V\amalg_AB\longrightarrow
       \Street c_nV\amalg_{\Street c_nA}\Street c_nB.
\end{equation}
The three maps on objects are weak equivalences: on $V$ by induction,
on $A,B$ by the simplex and boundary cases. The leg $A\to B$ is
monomorphic. Writing $A=\OrdN E$, $B=\OrdN F$ as in
Lemma~\ref{lem:subdivision-posets}, the inclusion $E\subseteq F$ is a
sieve; Lemma~\ref{lem:poset-pieces} makes $c_nA\to c_nB$ a sieve
inclusion, so $\Street c_nA\to\Street c_nB$ is monomorphic.
Lemma~\ref{lem:simplicial-gluing} with these two monomorphic legs
makes $q$ a weak equivalence; no monomorphism of $A\to V$ is required.

Apply Proposition~\ref{prop:attachment-comparison} to the arbitrary
attaching functor $c_nA\to c_nV$: the map
\begin{equation}\label{eq:unit-attachment-comparison}
 t\colon\Street c_nV\amalg_{\Street c_nA}\Street c_nB
       \longrightarrow
       \Street(c_nV\amalg_{c_nA}c_nB)
\end{equation}
is a weak equivalence. Since $c_n$ preserves colimits, its target is
$\Street c_n(V\amalg_AB)$. The composite $tq$ is exactly
$\eta_{V\amalg_AB}$: on each pushout leg this is naturality of $\eta$,
and equality on the two legs determines the map from the pushout. So
$\theta_{K_+}$ is a weak equivalence, and noninjective boundary maps
cause no change.

At a nonzero limit, $\Sd^2$ and $L_n$ preserve the colimit as left
adjoints, and $\Street$ preserves the filtered colimit by
Lemma~\ref{lem:filtered}. The unit at that stage is the filtered
colimit of previous units, hence a weak equivalence by the same
lemma. Transfinite induction proves \eqref{eq:subdivided-unit} for
every $K$. Only the simplex and boundary descriptions of subdivision
enter, so the argument is not affected by arbitrary attaching maps.
\end{proof}

\subsection{The Quillen equivalence}

\begin{theorem}[Quillen equivalence]\label{thm:quillen-equivalence}
The adjunction
\[
 L_n\colon\sSet_{\mathrm{KQ}}
     \rightleftarrows(\nCat,C_n,W_n,F_n)\colon R_n
\]
is a Quillen equivalence.
\end{theorem}

\begin{proof}
The lifting characterization from the proof of
Proposition~\ref{prop:model-structure} shows that $R_n$ preserves
fibrations and trivial fibrations, so this is a Quillen adjunction.

\emph{Sub-calculation for the composite subdivision.} Put $S=\Sd$,
$T=\Ex$, and let $a_K\colon K\to TSK$ be the unit of $S\dashv T$. The
mate identity is $j_K=T(\ell_K)a_K\colon K\to TK$. Since $j_K$ is a
weak equivalence, $\ell_K$ is, and $T$ preserves weak equivalences,
$T(\ell_K)$ is a weak equivalence; two-out-of-three gives $a_K$ a
weak equivalence. In particular $a_{SK}$ is, and the unit $b_K$ of
$S^2\dashv T^2$,
\[
 b_K=T(a_{SK})a_K\colon K\to T^2S^2K,
\]
is a weak equivalence (because $T$ preserves).

\emph{The composite unit.} The unit of $L_n\dashv R_n$ is
\[
 u_K=T^2(\theta_K)\,b_K\colon
   K\to T^2\Street c_nS^2K=R_nL_nK.
\]
Proposition~\ref{prop:subdivided-unit} makes $\theta_K$ a weak
equivalence, and $T$ preserves; so $u_K$ is a weak equivalence for
every $K$. For any strict functor $f\colon L_nK\to Y$, its simplicial
adjunct is $f^\sharp=R_n(f)u_K\colon K\to R_nY$. By definition of
$W_n$ and two-out-of-three,
\[
 f\in W_n\iff R_n(f)\in W_{\mathrm{KQ}}\iff f^\sharp\in W_{\mathrm{KQ}}.
\]
This is the Quillen-equivalence criterion (for cofibrant $K$ and
fibrant $Y$). Together with
Propositions~\ref{prop:model-structure} and~\ref{prop:properness}, this
proves every assertion of Theorem~\ref{thm:main} for each finite
$n\ge1$ and for $n=\infty$.
\end{proof}

\appendix

\section{Local finite presentability of \texorpdfstring{$\nCat$}{nCat}}
\label{sec:presentability}

We prove the presentability assertion used in
Lemma~\ref{lem:filtered}. The subtle point is that an equation between
boundary cells can create new composable pairs, so a presentation must
generate \emph{defined terms} and \emph{equations} together. Taking a
plain quotient of existing cells would miss the composites that become
defined after the identification. All sets and constructions below
lie in the fixed universe.

\subsection{Signature and equations}

Fix $n\in\{1,2,\dots,\infty\}$, with $\infty$ meaning $\omega$. Use
one sort $C_d$ for each $0\le d\le n$, or one per nonnegative integer
when $n=\infty$. The total operations are
\[
 s_d,t_d\colon C_d\longrightarrow C_{d-1}\quad(d>0),
 \qquad
 e_d\colon C_d\longrightarrow C_{d+1}\quad(d<n).
\]
For $0\le k<d$, $s_k^d$, $t_k^d$, $e_k^d$ are iterated. There is a
binary partial operation $*_k^d$ on $C_d$ with domain
\begin{equation}\label{eq:pres-domain}
 s_k^d(x)=t_k^d(y).
\end{equation}
We read $x*_k^dy$ as ``$x$ after $y$'' and suppress superscripts when
the sort is clear.

The equations are the strict-globular-category laws.

Globularity and identity boundary:
\[
 s_{d-1}s_d=s_{d-1}t_d,\quad
 t_{d-1}s_d=t_{d-1}t_d,\quad
 s_{d+1}e_d=\id=t_{d+1}e_d,
\]
for $2\le d\le n$ and $0\le d<n$, all $d$ when $n=\infty$. For a pair
satisfying \eqref{eq:pres-domain}, the composition boundary axioms are
\[
\begin{array}{ll}
 s_d(x*_{d-1}y)=s_d(y),&
 t_d(x*_{d-1}y)=t_d(x),\\
 s_d(x*_k y)=s_d(x)*_k s_d(y),&
 t_d(x*_k y)=t_d(x)*_k t_d(y)\quad(k<d-1).
\end{array}
\]
For each $k$, associativity is imposed on triples with
$s_k(x)=t_k(y)$, $s_k(y)=t_k(z)$. Units are
$x*_k e_k^d(s_k^d x)=x$ and $e_k^d(t_k^d x)*_k x=x$. Identities
preserve every lower composition:
$e_d(x*_k^d y)=e_d(x)*_k^{d+1}e_d(y)$.

Interchange, for $k<l<d$, is
\begin{equation}\label{eq:pres-interchange}
 (x*_l y)*_k(z*_l w)=(x*_k z)*_l(y*_k w),
\end{equation}
guarded by all four inner matchings
\[
 s_l^d(x)=t_l^d(y),\quad s_l^d(z)=t_l^d(w),\quad
 s_k^d(x)=t_k^d(z),\quad s_k^d(y)=t_k^d(w).
\]
These imply the outer comparisons by globularity; for example
$s_k^d(x*_l y)=s_k^d(x)=s_k^d(y)$ and
$s_k^d(z*_lw)=s_k^d(z)=s_k^d(w)$, so the left side is composable.
Thus the guard is an ordinary composable-array condition and not an
extra restriction. Definedness of the right-hand side alone does not
supply the guard.

This is a set of conditional equations with finite terms and finitely
many premises; no operation or equation takes infinitely many
arguments. Its models are precisely strict globular $n$-categories.
For finite $n$, adjoining iterated identities above dimension $n$
gives the convention of Section~\ref{sec:foundations}.

\subsection{Defined terms and presentations}

A \emph{sorted set of generators} $G$ assigns a dimension to each
generator. Let $T(G)$ be the set of all finite well-sorted raw terms.
A raw term belongs to $T(G)$ even if its boundary equation is not yet
known; it becomes a cell only once declared defined. Let $R$ be a set
of equations between raw terms of the same sort. An equation in $R$
is \emph{strong}: its interpretation requires both terms defined AND
equal. In particular $t=t$ can be used to force $t$ to be defined.

\begin{lemma}[Strict-category presentations]
\label{lem:strict-presentations}
For every sorted $G$ and every set $R$ of strong equations, there is a
small strict $n$-category $P(G,R)$ such that, naturally in $Y$,
strict functors $P(G,R)\to Y$ correspond to sorted assignments of the
generators to cells of $Y$ satisfying $R$.
\end{lemma}

\begin{proof}
Generate simultaneous judgments $\mathsf D(t)$ (defined) and $t=u$
(both defined, equal) by these rules.

(i) Every generator is defined and each member of $R$ is an equation.

(ii) An equation $t=u$ implies $\mathsf D(t)$, $\mathsf D(u)$.
Definedness of an operation term implies definedness of all
arguments. Definedness of $x*_k y$ also gives the matching
\eqref{eq:pres-domain}.

(iii) Total operations applied to defined arguments yield defined
terms. Defined arguments satisfying \eqref{eq:pres-domain} yield a
defined composite.

(iv) Equality is symmetric and transitive. Reflexivity is
$\mathsf D(t)\Rightarrow t=t$; it is not imposed on undefined raw
terms.

(v) Equal arguments transport definedness and equality through an
operation: from $t_i=u_i$ and $\mathsf D(f(t_i))$ infer
$\mathsf D(f(u_i))$ and equality of the two operation terms.

(vi) Every ground instance of the strict-category equations above is
imposed when its arguments are defined and its stated matchings hold;
the conclusion is equality of the two sides, hence definedness of both.
Interchange retains all four conditions in \eqref{eq:pres-interchange}.

Globularity, identity boundary and unit equations need definedness of
their variables; composition boundary and identity preservation from
identities require \eqref{eq:pres-domain}; associativity requires its
two matchings. Each rule has finitely many premises, and every rule is
sound in a strict category.

Start with the assumptions and repeatedly add conclusions of all
applicable rules. The union of finite stages is the least closed set
of judgments; any rule's finitely many premises occur together at
some stage; every resulting judgment has a finite derivation.
Everything involved is a set.

Let $P(G,R)_d$ be defined terms of sort $d$ modulo derivable equality.
Equality rules make this an equivalence relation; rules (iii) and (v)
descend total operations. For a partial operation, suppose the
boundary classes of $[x]$, $[y]$ match. Total boundary terms are
defined, so class equality means $s_k(x)=t_k(y)$ is derivable; rule
(iii) declares $x*_k y$ defined. This is independent of
representatives: $x=x'$ and $y=y'$ give $s_k(x)=s_k(x')$,
$t_k(y)=t_k(y')$, so the matching descends and rule (v) carries the
composites. Rule (ii) ensures matching boundaries on the quotient.
Rule (vi) gives all strict category laws.

Now an assignment $G\to Y$ satisfying $R$. Induction on derivations
shows every defined term evaluates in $Y$ and every derived equation
has equal values; rule (v) transports because equal arguments have
identical boundary values, so existence of one partial value entails
existence of the other. Evaluation therefore descends to a strict
functor, unique by induction on terms. Conversely, every strict
functor gives such an assignment. The construction is small,
consistent (the trivial strict category satisfies everything), and
empty when $G=\varnothing$ (no raw ground terms since all operations
have positive arity).
\end{proof}

\begin{remark}\label{rem:presentations-create-composites}
The simultaneous construction is essential even for ordinary
categories. If the source and target of a free arrow are identified,
its presentation must create the square of the arrow and all higher
powers; these are not quotients of the original cells, but new cells
introduced by rule (iii) as soon as their boundaries become derivable.
\end{remark}

\subsection{Colimits, filtered colimits, finite presentations}

\begin{proposition}[Local finite presentability]
\label{prop:strict-presentability}
For every $1\le n\le\infty$, the category $\nCat$ is locally small,
complete, cocomplete, and locally finitely presentable. Filtered
colimits are computed on cells. Every set of objects has a common
infinite regular presentability bound.
\end{proposition}

\begin{proof}
\emph{Colimits.} For a small diagram $X\colon I\to\nCat$, take a
generator $[i,a]$ per cell $a$ of each $X_i$ and impose the
operation-table equations
\[
 s([i,a])=[i,s(a)],\quad t([i,a])=[i,t(a)],\quad
 e([i,a])=[i,e(a)],\quad [i,a]*_k[i,b]=[i,a*_kb]
\]
(the last whenever $a*_kb$ is defined), and, for each arrow
$f\colon i\to j$, the equation $[i,a]=[j,X(f)(a)]$. By
Lemma~\ref{lem:strict-presentations}, maps from this presentation to
$Y$ are exactly compatible families $X_i\to Y$; it is the colimit.

\emph{Limits and local smallness.} In each dimension take the set of
compatible families; source, target, identity descend coordinatewise,
and composition is defined coordinatewise on exactly the matching
pairs. All laws and the limit universal property hold
coordinatewise, including the empty limit. Strict functors form a
subset of the product of cell maps, so the category is locally small.

\emph{Filtered colimits.} Form the colimit of each set of cells.
Finitely many representatives occur at one stage; any matching equation
holds at a later common stage where the composite is defined; a further
common stage proves independence of choices. Each category law holds at
a stage containing its finite tuple and matchings. No injectivity of
transitions is used.

\emph{Finite-term witness.} If finitely many assigned generator values
make a finite collection of terms defined and satisfy specified
equations in the colimit, those facts occur at one stage. Induct on
subterms: lift arguments, lift the boundary equality needed for a
partial composite, lift the composite, lift the required equalities.
Each step uses the equality criterion for filtered colimits of sets.

\emph{Finite presentations.} For finite $G,R$, a map
$P(G,R)\to\colim_i X_i$ is an assignment of finitely many generator
values satisfying finitely many strong equations, so it lifts to a
stage. If two stage maps are equal in the colimit, their values on $G$
agree at a later common stage; by the presentation universal property
the whole functors agree there. So
\[
 \colim_i\Hom(P(G,R),X_i)\cong\Hom(P(G,R),\colim_iX_i),
\]
and $P(G,R)$ is finitely presentable.

\emph{A generating set.} Every strict category $X$ has its full
\emph{cell presentation}: one generator $g_a$ per cell and all
operation-table equations. Evaluation is onto and, by induction on
defined terms together with the table equations, injective. Write it
$(G_X,R_X)$. Consider the finite pairs $(G_0,R_0)$ with
$G_0\subseteq G_X$, $R_0\subseteq R_X$, every generator in $R_0$
contained in $G_0$. Ordered by inclusion, these form a nonempty
filtered poset (empty pair allowed, finite unions upper). Their
presented categories have colimit $P(G_X,R_X)$: a compatible family of
maps from finite presentations assigns a value to every generator and
enforces every relation. The finite pairs need not be closed under
operations; finite presentations themselves supply closures. Thus every
object is a filtered colimit of objects from a set of finitely
presentable ones. With cocompleteness, $\nCat$ is locally finitely
presentable. The same argument goes through with the countable
signature in the $\omega$ case.

\emph{Common regular bound.} For a cardinal $\kappa$, the same proof
makes $P(G,R)$ $\kappa$-presentable when $|G|,|R|<\kappa$ and $\kappa$
is infinite regular: fewer than $\kappa$ generator values and fewer than
$\kappa$ relations must be lifted, and the witnesses form a diagram of
size $<\kappa$ so a cocone places them at one stage. Equality of maps is
detected by fewer than $\kappa$ generator equalities. The full cell
presentation of $X$ has cardinality at most
$\max\{\aleph_0,|\coprod_d X_d|\}$; choose a larger infinite regular
cardinal. For a set of objects, bound their full presentations and
choose one larger infinite regular cardinal.
\end{proof}

\bibliographystyle{plainnat}
\begin{thebibliography}{99}

\bibitem[Adamek et al.(1999)]{AdamekHebertRosicky1999}
J.~Ad{\'a}mek, M.~H{\'e}bert, and J.~Rosick{\'y}.
\newblock On essentially algebraic theories and their generalizations.
\newblock {\em Algebra Universalis}, 41(3):213--227, 1999.

\bibitem[Ad{\'a}mek \& Rosick{\'y}(1994)]{AdamekRosicky1994}
J.~Ad{\'a}mek and J.~Rosick{\'y}.
\newblock {\em Locally Presentable and Accessible Categories}, volume~189
  of {\em LMS Lecture Note Series}. Cambridge University Press, 1994.

\bibitem[Ara(2023)]{Ara2023}
D.~Ara.
\newblock Th{\'e}orie de l'homotopie des $\infty$-cat{\'e}gories strictes.
\newblock Habilitation {\`a} diriger des recherches, 2023.
\newblock {\tt https://www.normalesup.org/\~{}ara/files/hdr.pdf}.

\bibitem[Ara \& Maltsiniotis(2014)]{AraMaltsiniotis2014}
D.~Ara and G.~Maltsiniotis.
\newblock Vers une structure de cat{\'e}gorie de mod{\`e}les {\`a} la
  Thomason sur la cat{\'e}gorie des $n$-cat{\'e}gories strictes.
\newblock {\em Advances in Mathematics}, 259:557--654, 2014.
\newblock arXiv:1305.5086v3.

\bibitem[Ara \& Maltsiniotis(2015)]{AraMaltsiniotis2015}
D.~Ara and G.~Maltsiniotis.
\newblock Le type d'homotopie de la $\infty$-cat{\'e}gorie associ{\'e}e
  {\`a} un complexe simplicial.
\newblock arXiv:1503.02720v1, 2015.

\bibitem[Ara \& Maltsiniotis(2020)]{AraMaltsiniotis2020}
D.~Ara and G.~Maltsiniotis.
\newblock {\em Joint et tranches pour les $\infty$-cat{\'e}gories strictes},
  volume~165 of {\em M{\'e}moires de la SMF}.
\newblock SMF, 2020.
\newblock arXiv:1607.00668v4; DOI 10.24033/msmf.473.

\bibitem[Cisinski(1999)]{Cisinski1999}
D.-C. Cisinski.
\newblock La classe des morphismes de Dwyer n'est pas stable par
  r{\'e}tractes.
\newblock {\em Cahiers de Topologie et G{\'e}om{\'e}trie
  Diff{\'e}rentielle Cat{\'e}goriques}, 40(3):227--231, 1999.

\bibitem[Fiore \& Paoli(2010)]{FiorePaoli2010}
T.~M. Fiore and S.~Paoli.
\newblock A Thomason model structure on the category of small $n$-fold
  categories.
\newblock {\em Algebraic \& Geometric Topology}, 10(4):1933--2008, 2010.

\bibitem[Gagna(2018)]{Gagna2018}
A.~Gagna.
\newblock Strict $n$-categories and augmented directed complexes model
  homotopy types.
\newblock {\em Advances in Mathematics}, 331:542--564, 2018.
\newblock arXiv:1612.04450v2.

\bibitem[Goerss \& Jardine(1999)]{GoerssJardine1999}
P.~G. Goerss and J.~F. Jardine.
\newblock {\em Simplicial Homotopy Theory}, volume~174 of {\em Progress in
  Mathematics}. Birkh{\"a}user, Basel, 1999.

\bibitem[Guetta \& Maltsiniotis(2024)]{GuettaMaltsiniotis2024}
L.~Guetta and G.~Maltsiniotis.
\newblock Homologie polygraphique des syst{\`e}mes locaux.
\newblock {\em Advances in Mathematics}, 448:109719, 2024.
\newblock arXiv:2309.10466v2.

\bibitem[H{\'e}bert et al.(2001)]{HebertAdamekRosicky2001}
M.~H{\'e}bert, J.~Ad{\'a}mek, and J.~Rosick{\'y}.
\newblock More on orthogonality in locally presentable categories.
\newblock {\em Cahiers de Topologie et G{\'e}om{\'e}trie
  Diff{\'e}rentielle Cat{\'e}goriques}, 42(1):51--80, 2001.

\bibitem[Steiner(2004)]{Steiner2004}
R.~Steiner.
\newblock $\omega$-categories and chain complexes.
\newblock {\em Homology, Homotopy and Applications}, 6(1):175--200, 2004.
\newblock arXiv:math/0403237v2.

\bibitem[Steiner(2007)]{Steiner2007}
R.~Steiner.
\newblock Orientals.
\newblock In {\em Categories in Algebra, Geometry and Mathematical
  Physics}, volume~431 of {\em Contemp. Math.}, pages 427--439. AMS, 2007.
\newblock arXiv:math/0601383v2.

\bibitem[Street(1987)]{Street1987}
R.~Street.
\newblock The algebra of oriented simplexes.
\newblock {\em Journal of Pure and Applied Algebra}, 49(3):283--335, 1987.

\bibitem[Thomason(1980)]{Thomason1980}
R.~W. Thomason.
\newblock {\em Cat\/} as a closed model category.
\newblock {\em Cahiers de Topologie et G{\'e}om{\'e}trie Diff{\'e}rentielle},
  21(3):305--324, 1980.

\bibitem[Worytkiewicz et al.(2007)]{WorytkiewiczHessParentTonks2007}
K.~Worytkiewicz, K.~Hess, P.-E. Parent, and A.~Tonks.
\newblock A model structure {\`a} la Thomason on {\em 2-Cat\/}.
\newblock {\em Journal of Pure and Applied Algebra}, 208(1):205--236, 2007.

\bibitem[Worytkiewicz et al.(2016)]{WorytkiewiczHessParentTonks2016}
K.~Worytkiewicz, K.~Hess, P.-E. Parent, and A.~Tonks.
\newblock Corrigendum to ``A model structure {\`a} la Thomason on
  {\em 2-Cat\/}''.
\newblock {\em Journal of Pure and Applied Algebra}, 220(12):4017--4023,
  2016.

\end{thebibliography}

\end{document}