I'm looking for a proof of the existence of the Joyal model structure -- with its usual description -- which uses Cisinski theory directly. The closest thing I know of is Theorem 5.26 of Ara's Higher quasi-categories vs higher Rezk spaces, but even there it seems he needs to *assume* the existence of the Joyal model structure before he can compare it to a certain model structure obtained from Cisinski theory.

More precisely, let

$\mathsf{IH} = \{\Lambda^k[n] \to \Delta[n] \mid 0 < k < n\}$ be the set of inner horns;

$\mathsf{J} = \{\Delta[0] \to J\}$ where $J$ is the walking isomorphism.

Then we have the following

**Theorem:** (Existence of the Joyal model structure) There exists a Cisinski model structure on $sSet$ such that

- $(\ast(\mathsf{IH} \cup \mathsf{J})):$ The fibrant objects (resp. fibrations between fibrant objects) are those objects (resp. morphisms between fibrant objects) which have the right lifting property with respect to $\mathsf{IH} \cup \mathsf{J}$.

What I'm looking for is a write-up of the following proof outline of the above theorem:

**Proof Sketch:** By Cisinski theory, there exists a Cisinski model structure on $sSet$ such that $\ast(\Lambda(\mathsf{IH} \cup \mathsf{J}))$ holds, where for any $S$ we define

$\Lambda^0(S) = S \cup \{\Delta[n] \cup \partial \Delta[n] \times J \to \Delta[n] \times J\}$

$\Lambda^{n+1}(S) = \{B \times \partial \Delta[1] \cup A \times J \to B \times J \mid A \to B \in \Lambda^n(S)\}$

$\Lambda(S) = \cup_n \Lambda^n(S)$

We now verify (and these verifications are what I'd like to see!) that the morphisms of $\Lambda(\mathsf{IH} \cup \mathsf{J})$ can be constructed as retracts of transfinite composites of cobase changes of morphisms of $\mathsf{IH} \cup \mathsf{J}$. Therefore $\ast(\mathsf{IH} \cup \mathsf{J})$ and $\ast(\Lambda(\mathsf{IH} \cup \mathsf{J}))$ are equivalent, and we are done.

I'm pretty sure that all the necessary combinatorics has been done somewhere, but I'd like to see it strung together.

I'd also be interested in an analogous approach to the Kan-Quillen model structure.