Let $I$ be the (nerve of the) walking isomorphism (a simplicial set). Consider the inclusion $\Delta^1 \to I$ and the inclusion $\partial \Delta^1 \to \Delta^1$. Take their [pushout-product](https://ncatlab.org/nlab/show/pushout-product) to obtain a map


$$\Delta^1 \times \Delta^1 \cup\_{\partial \Delta^1 \times \Delta^1} \partial \Delta^1 \times I \to \Delta^1 \times I$$


**Question 1:** Is this map a Joyal equivalence?


**Question 2:** Is this map (cellularly) inner anodyne?


If we reflect to $Cat$, then the map becomes an isomorphism. The content of this assertion is that if I have a commtutative square in a category $C$ and two opposite ends are isomorphisms, then we have an isomorphism in the arrow category $C^{\Delta^1}$.


I am fairly certain this is also true in quasicategories, so the answer to (1) is presumably *yes*. I'd like a direct proof of this fact, and the most straightforward proof would be to explicitly fill some horns and see that it's cellularly inner anodyne -- i.e. obtained just by gluing on some inner horns -- no retracts required, and no fancier Joyal trivial cofibrations required. But perhaps this is not possible.



Is $\Delta^1 \times \Delta^1 \cup_{\partial \Delta^1 \times \Delta^1} \partial \Delta^1 \times I \to \Delta^1 \times I$ inner anodyne?
As requested, here is a proof that the map in question is inner anodyne that does not proceed by explicitly filling inner horns.


By definition (more or less), a map is inner anodyne iff it has the LLP wrt all inner fibrations; but if moreover the codomain of that map is a quasi-category, as in our example, it suffices by pull-back to show that it has the LLP wrt all inner fibrations between quasi-categories.


So let $p \colon X\to Y$ be an inner fibration between quasi-categories. By adjointness, the pushout-product of the boundary inclusion $i \colon \partial\Delta^1 \to \Delta^1$ with the inclusion $j \colon \Delta^1 \to \mathbb{I}$ has the LLP wrt $p$ iff the inclusion $j$ has the LLP wrt to the "pullback-internal hom" of $i$ and $p$, $\{i.p\} \colon \operatorname{Fun}(\Delta^1,X) \to \operatorname{Fun}(\partial\Delta^1,X) \times\_{\operatorname{Fun}(\partial\Delta^1,Y)}\operatorname{Fun}(\Delta^1,Y)$.


Now, since $i$ is a bijective-on-0-simplices monomorphism and $p$ is an inner fibration between quasi-categories, this map $\{i,p\}$ is a conservative inner fibration between quasi-categories.


So the result follows from the fact that any conservative inner fibration between quasi-categories has the RLP wrt to the inclusion $j \colon \Delta^1 \to \mathbb{I}$. This is a consequence of Joyal's special outer horn lifiting theorem, for this inclusion $j \colon \Delta^1 \to \mathbb{I}$ can be built up by filling outer horns $\Lambda^n\_n \to \Delta^n$ for $n > 1$ all of whose final edges are the edge of the original domain $\Delta^1$.


