# The right cancellation property for certain classes of dendroidal anodynes

Miguel Barata  Universiteit Utrecht, Hans Freudenthalgebouw, Budapestlaan 6,
3584 CD Utrecht, The Netherlands<EMAIL_ADDRESS>
###### Abstract.

We generalize a previous result of Stevenson [9] to the category of dendroidal
sets, yielding the right cancellation property of dendroidal inner anodynes
within the class of normal monomorphisms. As an application of this property,
we show how to construct a symmetric monoidal $\infty$-category
$\mathsf{Env}(X)^{\otimes}$ from a dendroidal $\infty$-operad $X$, in a way
that generalizes the symmetric monoidal envelope of a coloured operad.

###### Contents

  1. 1 Introduction
  2. 2 Some recollections about dendroidal sets
  3. 3 The right cancellation property for classes of dendroidal morphisms
  4. 4 An application: the symmetric monoidal envelope of a dendroidal $\mathbf{\infty}$-operad
    1. 4.1 Interpreting $\mathsf{Fin}_{\ast}$ as a category of forests
    2. 4.2 The symmetric monoidal envelope of a dendroidal $\infty$-operad

##  1\. Introduction

The purpose of this note is to give a generalization of the right cancellation
property of inner anodynes in the category of simplicial set $\mathsf{sSets}$
to the category of dendroidal sets $\mathsf{dSets}$. We register here the
central definition of this work.

######  Definition 1.1.

Let $\mathcal{M}$ and $\mathcal{N}$ be classes of morphisms of a category
$\mathcal{C}$ such that $\mathcal{M}$ is contained in $\mathcal{N}$. Then we
say that $\mathcal{M}$ satisfies the right cancellation property within
$\mathcal{N}$ if given any string of morphisms in $\mathcal{C}$

$A\xrightarrow{i}B\xrightarrow{j}C$

such that $i,j,ji$ are in $\mathcal{N}$ and additionally both $i$ and $ji$ are
in $\mathcal{M}$, then $j$ is also in $\mathcal{M}$.

A knowledge of which classes of simplicial morphisms satisfy the right
cancellation property seems to be of particular interest, for instance to
simplify certain conbinatorial arguments in $\mathsf{sSets}$. As an example of
this phenomenon, one has the well-known result [3, Prop. 5.34] in simplicial
homotopy theory which guarantees that, for any saturated class of simplicial
morphisms $\mathcal{M}$ satisfying the right cancellation property within the
monomorphisms, if all the spine inclusion are in $\mathcal{M}$, then actually
all inner anodynes are in $\mathcal{M}$. The upshot of such a result is that,
under the circumstances described, one can often argue with spine inclusions
in place of inner horn inclusions, which tends to be combinatorially easier to
do.

For the sake of easy reference, we register below the simplicial statement we
are aiming to generalize.

######  Theorem 1.2.

The class of inner anodynes in $\mathsf{sSets}$ satisfies the right
cancellation property within the class of simplicial monomorphisms.

The first account and proof of Theorem 1.2 appears in [9] as Theorem 1.5 and
seems to have gone mostly unnoticed in the literature on simplicial sets. In
contrast, the right cancellation property for simplicial left and right
anodynes is more well-known: it was already present in Joyal’s work on
simplicial sets and quasicategories, for instance.

In what concerns the proof of the right cancellation property for simplicial
left and right anodyne maps, the interested reader can check [6, Cor. 4.1.2.2]
and [3, Cor. 8.80] for instance. In any case, we want to mention that these
proofs are not entirely trivial, and rely on certain properties of left and
right anodynes deduced from the existence of the contravariant and covariant
model structures on the slice categories $\mathsf{sSets}_{/V}$. In contrast,
this argument cannot be followed through in the inner anodyne scenario, due to
the corresponding analogues of the contravariant and covariant model
structures not existing. In this sense, Stevenson’s proof turns to be a better
approach: it actually also works (and simplifies somewhat) if one wants to
show the right cancellation property for left and right anodynes.

As we have already mentioned, our intention is to generalize Stevenson’s
result to the context of dendroidal sets. This is a category of presheaves on
the tree category $\mathsf{\Omega}$, first introduced by Moerdijk and Weiss in
[8], and this category play a role in the theory of operads analogous to the
one played by $\mathsf{sSets}$ in category theory. After giving a brief
account in Section 2 of some notation and results on dendroidal sets, we will
dedicate Section 3 to proving the following generalization of Theorem 1.2.

######  Theorem 1.3.

Inner/leaf/root anodynes in $\mathsf{dSets}$ satisfy the right cancellation
property within the class of normal monomorphisms.

Here the classes of leaf and root anodynes play a similar role in the
dendroidal formalism as that of left and right anodynes in $\mathsf{sSets}$,
respectively. We remark that the right cancellation property for leaf anodynes
is already known to hold: for instance, one can easily adapt the simplicial
argument presented in [3] to the dendroidal context, using the existence of
the version of the covariant model structure for the overcategories
$\mathsf{dSets}_{/V}$. However, the version of Theorem 1.3 about inner and
root anodynes doesn’t seem to be present in the literature111We note that, for
the simplicial context, the result for left anodynes immediately implies the
result for right anodynes, due to the existence of the involution
$\mathsf{\Delta}\to\mathsf{\Delta}$ which reverses the order of each poset.
However, there is no parallel in $\mathsf{\Omega}$ of this involution, and
therefore the leaf anodyne result doesn’t imply the root anodyne one..

In Section 4 we give an application of the right cancellation property of
dendroidal inner anodynes. We explain how one can assign to a dendroidal
$\infty$-operad $X$ a simplicial set $\mathsf{Env}(X)^{\otimes}$ which
recovers the usual construction of the symmetric monoidal envelope of a
coloured operad. The exact result we will show is the following:

######  Theorem 1.4.

Let $X$ be a dendroidal set. Then there exists a simplicial set
$\mathsf{Env}(X)^{\otimes}$ satisfying the following properties:

  1. (a)

If $X$ is an $\infty$-operad, then $\mathsf{Env}(X)^{\otimes}$ is a symmetric
monoidal $\infty$-category in the sense of Lurie.

  2. (b)

If $\mathbf{P}$ is a coloured operad and $N\mathbf{P}\in\mathsf{dSets}$ is the
corresponding dendroidal nerve, then $\mathsf{Env}(N\mathbf{P})^{\otimes}$ is
the symmetric monoidal $\infty$-category associated to the symmetric monoidal
category $\mathsf{Env}(\mathbf{P})$ corresponding to the symmetric monoidal
envelope of $\mathbf{P}$.

The main technical hurdle for proving this result will be handled in Section
4.1, where we use the right cancellation property of dendroidal inner anodynes
to investigate a certain category of forests $\mathbb{F}$ constructed from
$\mathsf{Fin}_{\ast}$. Finally, in Section 4.2 we will use these dendroidal
considerations to construct $\mathsf{Env}(X)^{\otimes}$ and prove Theorem 1.4.

Acknowledgements. The author was supported by the Dutch Research Council (NWO)
through the grant 613.009.147. The author would like to thank Ieke Moerdijk
for helpful feedback on earlier drafts of this work.

##  2\. Some recollections about dendroidal sets

Before embarking on proving Theorem 1.3, we will first quickly recall some
definitions and notation regarding the tree category $\mathsf{\Omega}$, as
well as some technical results that will be used in the rest of the text. For
a textbook account of the subject and a more thorough presentation of some of
the definitions below, see [3].

The tree category $\mathsf{\Omega}$ has objects given by non-planar rooted
trees $T$ with finite vertex and edge sets, together with a specified special
edge which is attached to a single vertex, and we call this edge the root of
$T$. As explained in Section 1.3 of [3], every tree $T$ gives rise to a
coloured operad $\mathsf{\Omega}(T)$, and we define the morphism set
$\mathsf{\Omega}(T,S)$ as the the set of all operad maps
$\mathsf{\Omega}(T)\to\mathsf{\Omega}(S)$. We specify some notation which is
useful when discussing trees:

  * $\diamond$

Any edge in $T$ that is adjacent to two vertices is called an inner edge; the
edges which are neither inner nor the root edge are called the leaves.

  * $\diamond$

The edge set $E(T)$ has a poset structure by setting $e_{1}\leq e_{2}$ when
the (unique) path from $e_{2}$ to the root edge contains $e_{1}$. The minimal
element of this ordering is the root edge, and we call the maximal edges the
leaves of $T$. A similar ordering can also be defined on the vertex set
$V(T)$, with the minimal element being the root vertex and the maximal
elements being the leaf vertices.

  * $\diamond$

The set of edges incident to a vertex $v$ has a unique minimal element called
the outcoming edge of $v$, and the remaining edges, which are pairwise
independent in the ordering above, are the incoming edges of $v$. In the
scenario when $v$ admits no incoming edges, we say that the vertex $v$ is a
stump.

  * $\diamond$

the tree which is just a single edge will be represented by $\eta$. The trees
with a single vertex and $n$ incoming edges are the $n$-corollas and will be
denoted throughout by $C_{n}$. As an example, here is a picture of $C_{4}$:

.

######  Example 2.1.

Consider the following example of an object $T$ in $\mathsf{\Omega}$:

$r$$v_{1}$$v_{2}$$u$$f$$g$$e$$h$$v_{r}$

The root edge corresponds to the edge $r$, whereas the edges $e,f,g$ and $h$
are the inner edges of the tree. The edges which are connected to exactly one
vertex are the leaves of $T$. As for the vertices, $v_{1}$ and $v_{2}$ are the
leaf vertices of $T$, $u$ is the only stump and $v_{r}$ is the root vertex.

In a way that mirrors the description of the morphisms in $\mathsf{\Delta}$
via face and degeneracy maps satisfying the simplicial relations, one can show
that the morphisms in $\mathsf{\Omega}$ are generated under composition by the
classes of maps below:

  * $\diamond$

For every inner edge $e$ of $T$, we have an associated inner face
$\partial_{e}T\to T$ which comes from contracting $e$.

  * $\diamond$

For every leaf vertex $v$, there is a leaf face $\partial_{v}T\to T$ coming
from removing this vertex from $T$.

  * $\diamond$

Suppose the root vertex of $T$ has the property that one and only one of its
incoming edge is also an inner edge. Then $T$ admits a root face
$\partial_{\mathrm{root}}T\to T$, where the domain is the tree resulting from
removing the root vertex of $T$ and keeping the rest of $T$.

  * $\diamond$

If $e$ is any edge of $T$, there is a degeneracy map $\sigma_{e}T\to T$ which
subdivides $e$ in half by adding a new vertex.

  * $\diamond$

The isomorphisms $T\xrightarrow{\cong}S$.

We will usually call the faces and degeneracy maps defined above the
elementary faces and elementary degeneracies of a tree.

These morphisms, together with the dendroidal identities in [3, Sec. 3.3.4],
give a complete description of the tree category $\mathsf{\Omega}$ in terms of
generators and relations. The main motivation for considering this category in
the first place is that its presheaves, which form the category
$\mathsf{dSets}$ of dendroidal sets, correctly model the algebraic structure
of an operad. More explicitly, there exists a functor

$N\colon\mathsf{Op}\longrightarrow\mathsf{dSets},$

where $\mathsf{Op}$ is the category of coloured operads, which sends a
coloured operad $\mathbf{P}$ to a dendroidal set $N\mathbf{P}$, which we will
call the dendroidal nerve of $\mathbf{P}$ [8, Ex. 4.2], resembling the usual
construction of the nerve of a small category. We also point out that there is
a pair of adjoint functors

${{\mathsf{dSets}}}$${{\mathsf{sSets}}}$$\scriptstyle{\iota^{*}}$$\scriptstyle{\iota_{!}}$

comparing simplicial and dendroidal presheaves. This is induced by the
inclusion of the full subcategory of $\mathsf{\Omega}$ spanned by the trees
with only vertices with exactly one incoming edge (which we usually call the
linear trees), which is isomorphic to $\mathsf{\Delta}$.

Equipped with this new formalism, one can easily transfer some of the notions
from the homotopy theory of simplicial sets to the world of dendroidal sets.
Let us point out some of these analogous constructions:

  * $\diamond$

Any tree $T$ admits a boundary $\partial T\to T$, given as the union of all
the faces of $T$.

  * $\diamond$

Any inner edge $e$ leads to an inner horn $\Lambda^{e}T\to T$, defined as the
union of all elementary faces except for $\partial_{e}T$.

  * $\diamond$

Any leaf vertex $v$ leads to a leaf horn $\Lambda^{v}T\to T$, defined as the
union of all elementary faces except for $\partial_{v}T$.

  * $\diamond$

If $T$ admits a root face, then the root horn $\Lambda^{v}T\to T$ corresponds
to the union of all faces except the root face. Here $v$ denotes the root
vertex.

  * $\diamond$

A dendroidal map $f\colon X\to Y$ is a normal monomorphism if it is levelwise
injective and, for every tree $T$, the group of automorphisms of $T$ acts
freely on $Y_{T}-\mathrm{im}(f)$.

  * $\diamond$

A dendroidal map is inner anodyne if it can be obtained from the inner horn
inclusions $\Lambda^{e}T\to T$ via pushouts, transfinite compositions and
retracts (that is, the class of inner anodynes is the saturated class
generated by the dendroidal inner horn inclusions). A similar definition
applies for leaf/root anodynes, which form the saturated class generated by
inner horn inclusions and leaf/root horn inclusions.

  * $\diamond$

An inner fibration is a dendroidal map $X\to Y$ that has the right lifting
property with respect to all inner horn inclusions. A similar definition
applies for dendroidal leaf/right fibrations in terms of leaf/root anodynes.

The dendroidal formalism also allows us to define $\infty$-operads, which we
record in the definition below.

######  Definition 2.2.

Let $X$ be a dendroidal set. We say $X$ is an $\infty$-operad if, for any
inner horn inclusion $\Lambda^{e}T\to T$ and solid diagram

${{\Lambda^{e}T}}$${X,}$${T}$

a diagonal dashed lift exists. The underlying $\infty$-category of $X$ is the
simplicial set $\iota^{*}X$, which is indeed an $\infty$-category by [3, Lem.
6.2].

Before finishing this section on background on dendroidal sets, we will
mention some results which we will use in the next section. We recall that
given an $\infty$-operad $X$, we say $x\in X_{C_{1}}$ is an equivalence is it
defines an equivalence in the underlying $\infty$-category of $X$.

######  Theorem 2.3.

Let $T$ be a tree with at least two vertices and a unary root vertex $v$ (that
is, $v$ has only one incoming edge). Given $p\colon X\to Y$ an inner fibration
of $\infty$-operads and a commutative square

${\Lambda^{v}T}$${X}$${T}$${Y}$$\scriptstyle{f}$$\scriptstyle{p}$

such that $f$ sends $v$ to an equivalence in $X$, then the diagram admits a
diagonal lift.

This was originally proved by Cisinski–Moerdijk in [2, Thm. 4.2].

In the theory of simplicial sets, a necessary and crucial step in analysing
the behaviour of the different classes of anodyne maps is to consider how
these interact with the cartesian product in $\mathsf{sSets}$. A similar
situation holds for the category of dendroidal sets, but it is also useful in
a lot of situation to have a grasp on how these classes of morphisms interact
with a different bifunctor

${-}\otimes{-}:\mathsf{dSets}\times\mathsf{dSets}\rightarrow\mathsf{dSets}.$

This is defined on representables via the formula $T\otimes
S=N(\Omega(T)\otimes_{\mathsf{BV}}\Omega(S))$, where $\otimes_{\mathsf{BV}}$
denotes the Boardman–Vogt tensor product of coloured operads, and then extend
to all presheaves by taking left Kan extensions on both variables. The
original definition of the Boardman–Vogt tensor product is contained in [1]
within the more general context of algebraic theories and a similar treatment
is contained in Section 1.6 of [3] for the specific case of coloured operads.

Let us make two important remarks concerning the dendroidal tensor product.
Firstly, $\mathsf{dSets}$ equipped with $\otimes$ does not define a monoidal
structure, since the tensor product will not be associative, even at the level
of the representable presheaves. Secondly, in general there are no projection
maps associated to the dendroidal tensor product; however, in the special case
when $X\in\mathsf{sSets}$ and $Y\in\mathsf{dSets}$, there exists a projection
$\pi_{Y}\colon X\otimes Y\to Y$ onto the dendroidal component, see Section 4.2
of [3] for details.

The dendroidal tensor product takes part in an adjunction, which, for any
$X,Y,A\in\mathsf{dSets}$, takes the form

$\mathsf{dSets}(X\otimes A,Y)\cong\mathsf{dSets}(X,\mathsf{Hom}(A,Y)).$

We will reserve the notation $Y^{A}\in\mathsf{sSets}$ for the underlying
simplicial set of the dendroidal set $\mathsf{Hom}(A,Y)$. As one would expect
and immediately checks, the 0-simplices of $Y^{A}$ are the dendroidal maps
$A\to Y$.

For the next few statements, we will represent the leaf edge of $C_{1}$ by
$0$, and the root edge by $1$. We also recall that, for a dendroidal map
$p\colon X\to Y$ and colour $y\in Y_{\eta}$, we can define the fiber of $y$
via the pullback

${{X_{y}}}$${X}$${\eta}$${Y.}$$\scriptstyle{\lrcorner}$$\scriptstyle{p}$$\scriptstyle{y}$

It follows from this that $X_{y}$ is actually a simplicial set due to the
isomorphism $\mathsf{dSets}_{/\eta}\cong\mathsf{sSets}$: Moreover, it is an
$\infty$-category if $p$ is a dendroidal inner fibration.

######  Lemma 2.4.

Let $i\colon A\to B$ be a dendroidal inner/leaf/root anodyne and $p\colon X\to
Y$ a dendroidal inner/left/right fibration. Then the canonical map to the
pullback

$\Psi:X^{B}\longrightarrow X^{A}\times_{Y^{A}}Y^{B}$

is a trivial Kan fibration.

Moreover, suppose there are dendroidal maps $f,g\colon B\to X$ projecting to
the same pair $(\alpha,\beta)$ via the map $\Psi$. Then there exists a
dendroidal morphism $H\colon C_{1}\otimes B\to X$ with the following
properties:

  1. (a)

$H(0,-)=g$ and $H(1,-)=f$.

  2. (b)

The following diagrams

${C_{1}\otimes B}$${X}$${C_{1}\otimes A}$${C_{1}\otimes
B}$${B}$${Y}$${A}$${X}$$\scriptstyle{H}$$\scriptstyle{\pi_{B}}$$\scriptstyle{p}$$\scriptstyle{\mathrm{id}\otimes
i}$$\scriptstyle{\pi_{A}}$$\scriptstyle{H}$$\scriptstyle{\beta}$$\scriptstyle{\alpha}$

commute.

  3. (c)

For every colour $b\in B_{\eta}$, the 1-corolla $H(-,b)\colon C_{1}\to X$
defines an equivalence in the fiber $X_{g(b)}$ of $p$.

###### Proof.

The proof of the first statement is contained [3, Thm. 6.33]. As for the
second one, we can more succinctly describe the map $H$ as a diagonal lift in
the diagram

${\partial J\otimes B\cup J\otimes A}$${X}$${J\otimes
B}$${Y}$$\scriptstyle{p}$

where the top map is $\left(g\amalg f,\alpha\pi_{A}\right)$ and the bottom one
is $\beta\pi_{B}$, and $J$ is nerve of the groupoid with two objects and an
isomorphism between them. By adjunction, this is equivalent to finding a lift
in

${\partial J}$${X^{B}}$${J}$${X^{A}\times_{Y^{A}}Y^{B}.}$$\scriptstyle{\Psi}$

By the first part and the fact that $\partial J\to J$ is an anodyne map, we
conclude that the desired lift exists. ∎

######  Remark 2.5.

The map $H$ is sometimes known as a fibrewise $J$-homotopy relative to $A$
between $f$ and $g$. For a more thorough study of this notion, see Section 6.8
of [3].

##  3\. The right cancellation property for classes of dendroidal morphisms

In order to prove Theorem 1.3 and following Stevenson’s own proof, we start by
showing the following auxiliary lemma.

######  Lemma 3.1.

Let $p\colon X\to Y$ be an inner fibration of dendroidal sets and $j\colon
B\to C$ a normal monomorphism. Consider any commutative diagram

(1) ${0\otimes C\cup_{0\otimes B}C_{1}\otimes B}$${X}$${C_{1}\otimes
C}$${C}$${Y}$$\scriptstyle{K}$$\scriptstyle{p}$$\scriptstyle{\pi_{C}}$$\scriptstyle{g}$

such that, for every colour $b\in B_{\eta}$, the 1-corolla $K(-,b)\colon
C_{1}\to X$ is an equivalence in the fiber $X_{g(b)}$ of $p$. Then a diagonal
lift always exists.

###### Proof.

Firstly, we can assume that $j$ is a boundary inclusion $\partial T\to T$, due
to the existence of a skeletal filtration for normal monomorphisms [3, Prop.
3.26]. Moreover, by pulling back $p$ along $g$ and using that any tree $T$
defines an $\infty$-operad, we can further assume that $X$ and $Y$ are
$\infty$-operads.

According to Theorem B.2 in [2], there is a finite filtration of the
dendroidal set $C_{1}\otimes T$

$A_{0}\subseteq A_{1}\subseteq\cdots\subseteq A_{n-1}\subseteq
A_{n}=C_{1}\otimes T,$

starting at $A_{0}=0\otimes T\cup_{0\otimes\partial T}C_{1}\otimes\partial T$
and satisfying the following properties:

  1. (i)

The inclusion $A_{j}\to A_{j+1}$ is inner anodyne, as along as $j\neq n-1$.

  2. (ii)

There exists a pushout square

${{\Lambda^{v}S}}$${{A_{n-1}}}$${S}$${{A_{n}}}$$\scriptstyle{\lrcorner}$

where $S$ is a tree with at least two vertices and a unary root vertex $v$.
Moreover, the inclusion of the vertex $v\colon C_{1}\to C_{1}\otimes T$
coincides with the inclusion $C_{1}\otimes r_{T}\to C_{1}\otimes T,$ where
$r_{T}$ denotes the root edge of $T$.

Condition (i), together with $p$ being an inner fibration, provides us with a
diagonal lift for diagram (1) up to stage $A_{n-1}$ of the filtration. For the
last step of the filtration, consider the diagram

${{\Lambda^{v}S}}$${{A_{n-1}}}$${X}$${S}$${{C_{1}\otimes
T}}$${Y}$$\scriptstyle{p}$$\scriptstyle{\lrcorner}$$\scriptstyle{g\pi_{T}}$

It suffices to show that the outer square admits a diagonal lift, since the
leftmost square is a pushout diagram. With this purpose in mind, observe that
property (ii) and our initial hypothesis on $K$ imply that the top map in the
diagram sends the unitary vertex $v$ to an equivalence in $X$. Thus, the
conditions of Theorem 2.3 are satisfied, which provides us with our desired
diagonal lift. ∎

###### Proof of Theorem 1.3.

We will first consider the case of inner anodynes and in the end discuss how
the proof goes for leaf and root anodynes.

Suppose we are given the diagram below

$\leavevmode\hbox to58.38pt{\vbox
to78.56pt{\pgfpicture\makeatletter\hbox{\hskip 29.18918pt\lower-39.329pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-29.18918pt}{-39.22916pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
8.05554pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.75pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.05554pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.34894pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.0434pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${B}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.34894pt\hfil&\hfil\hskip 32.84023pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.53471pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${X}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.84026pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.23679pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.93124pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${C}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.23679pt\hfil&\hfil\hskip 32.3194pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${Y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.31943pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-20.84024pt}{21.2167pt}\pgfsys@lineto{-20.84024pt}{4.01662pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-20.84024pt}{3.81664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.6046pt}{10.10835pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{i}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.69458pt}{21.2167pt}\pgfsys@lineto{10.9934pt}{2.72621pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.78828}{-0.61533}{0.61533}{0.78828}{11.15102pt}{2.60318pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.6598pt}{15.56229pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{fi}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-20.84024pt}{-10.93608pt}\pgfsys@lineto{-20.84024pt}{-28.13617pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-20.84024pt}{-28.33615pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.47633pt}{-21.36389pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{j}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.2913pt}{-4.57637pt}\pgfsys@lineto{10.9087pt}{-4.57637pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.10869pt}{-4.57637pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5816pt}{-0.8625pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{20.34892pt}{-10.93608pt}\pgfsys@lineto{20.34892pt}{-28.13617pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{20.34892pt}{-28.33615pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.70169pt}{-20.5625pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{p}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.40346pt}{-36.72916pt}\pgfsys@lineto{11.42953pt}{-36.72916pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.62952pt}{-36.72916pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.08194pt}{-33.0153pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{g}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},$

with $p$ being an inner fibration. In order to find a diagonal lift in the
bottom square, note first that $ji$ being inner anodyne provides us with a
morphism $s\colon C\to X$ making the outer square commute; however, this will
not make the bottom square commute in general since the equation $sj=f$ may
not hold.

Since $i$ is inner anodyne and $p$ is an inner fibration, the canonical map

$\Psi:X^{B}\longrightarrow X^{A}\times_{Y^{A}}Y^{B},$

is a trivial Kan fibration by Lemma 2.4. Moreover, by the construction of $s$,
both of the morphisms $f,sj\colon B\to X$ lie on the fiber of $\Psi$ over the
pair $(fi,gj)$, and therefore the second part of Lemma 2.4 can be applied.
Spelling out the details, this entails the existence of a dendroidal morphism
$H\colon C_{1}\otimes B\to X$ such that the following hold:

  1. (a)

$H(0,-)=sj$ and $H(1,-)=f$.

  2. (b)

The diagrams

${C_{1}\otimes B}$${X}$${C_{1}\otimes A}$${C_{1}\otimes
B}$${B}$${C}$${Y}$${A}$${B}$${X}$$\scriptstyle{\pi_{B}}$$\scriptstyle{H}$$\scriptstyle{p}$$\scriptstyle{\pi_{A}}$$\scriptstyle{C_{1}\otimes
i}$$\scriptstyle{H}$$\scriptstyle{j}$$\scriptstyle{g}$$\scriptstyle{i}$$\scriptstyle{f}$

commute.

  3. (c)

For any colour $b\in B_{\eta}$, the 1-corolla $H(-,b)\colon C_{1}\to X$
defines an equivalence in the fiber $X_{g(b)}$ of $p$.

The homotopy $H\colon C_{1}\otimes B\to X$ and the diagonal lift $s\colon
C\cong 0\otimes C\to X$ give rise to a map $(s,H)\colon 0\otimes
C\cup_{0\otimes B}C_{1}\otimes B\to X$ on the respective pushout, which
additionally makes the following diagram

(2) ${0\otimes C\cup_{0\otimes B}C_{1}\otimes B}$${X}$${C_{1}\otimes
C}$${C}$${Y}$$\scriptstyle{(s,H)}$$\scriptstyle{p}$$\scriptstyle{\pi_{C}}$$\scriptstyle{g}$

commute. By property (c) above, the restrictions $(s,H)(-,b)$ for each colour
$b\in B_{\eta}$ define an equivalence in the fiber $X_{g(b)}$ of $p$.
Therefore the conditions for Lemma 3.1 are satisfied and a diagonal lift
$t\colon C_{1}\otimes C\to X$ can be constructed. It is now an easy
verification that $t(1,-)$ provides the required lift for our initial diagram,
as desired.

Finally, we discuss the leaf and root anodyne cases. Firstly, these classes of
anodynes have their respective versions of Lemma 2.4, therefore the only
problem rests in Lemma 3.1. Of course, since left and right fibrations are
particular cases of inner fibrations, this result still holds; but notice that
we can show that (2) admits a lift without this extra technical lemma. Indeed,
due to the property that $(s,H)$ define certain equivalences in the fibers, we
can actually replace the left map in (2) by

$0\otimes C\cup_{0\otimes B}J\otimes B\longrightarrow J\otimes C.$

Since $0\to J$ is both a left and right anodyne, an application of [3, Cor.
6.30] shows that this pushout-product is a leaf and root anodyne. ∎

######  Remark 3.2.

One can deduce Stevenson’s original simplicial version of Theorem 1.3 from the
dendroidal variation we just presented. Indeed, if
$A\xrightarrow{i}B\xrightarrow{j}C$ is a string of simplicial monomorphisms
with $ji$ and $i$ inner anodynes, then applying $\iota_{!}$ to it yields a
string of dendroidal sets

$\iota_{!}A\xlongrightarrow{\iota_{!}i}\iota_{!}B\xlongrightarrow{\iota_{!}j}\iota_{!}C.$

All the monomorphisms in questions are normal (being normal is meaningless in
this context), and the dendroidal maps $\iota_{!}i$ and $\iota_{!}(ji)$ are
inner anodynes. Therefore, by right cancellation so is $\iota_{!}j$, which is
equivalent to saying $j$ is a simplicial inner anodyne. This argument also
holds for the other two classes of anodynes we discussed.

##  4\. An application: the symmetric monoidal envelope of a dendroidal
$\mathbf{\infty}$-operad

In this section we will give an application of the right cancellation property
for dendroidal inner anodynes in order to explain how one can associate to any
dendroidal set $X$ a simplicial set $\mathsf{Env}(X)^{\otimes}$ which, when
applied to the dendroidal nerve of a coloured operad $X=N\mathbf{P}$, should
recover the symmetric monoidal envelope of the operad, which we recall below.
Here we will write $\underline{n}=\\{1,2,\ldots,n\\}$, which we often see also
as the poset $\\{1<2<\cdots<n\\}$.

######  Definition 4.1.

Let $\mathbf{P}$ be a coloured operad. We define the symmetric monoidal
envelope of $\mathbf{P}$ is the symmetric monoidal category
$(\mathsf{Env}(\mathbf{P}),\boxplus,\emptyset)$ described by the following:

  * $\diamond$

The objects are the strings $(c_{1},\ldots,c_{n})$ of colours of $\mathbf{P}$,
for $n\geq 0$. The empty string is respresented by $\emptyset$.

  * $\diamond$

A morphism

$(c_{1},\ldots,c_{n})\longrightarrow(d_{1},\ldots,d_{m})$

is determined by a pair $(f,\\{p_{j}:j\in\underline{m}\\})$, where
$f\colon\underline{n}\to\underline{m}$ is a function of finite sets. For each
$j\in\underline{m}$, $p_{j}$ is an operation in $\mathbf{P}$ with output
$d_{j}$, and input set $\\{c_{i}:f(i)=j\\}\subseteq\\{c_{1},\ldots,c_{n}\\}$
ordered according to $\underline{n}$. Composition comes from the operadic
composition of $\mathbf{P}$.

  * $\diamond$

The tensor product is given on objects via concatenation

$(c_{1},\ldots,c_{n})\boxplus(d_{1},\ldots,d_{m})=(c_{1},\ldots,c_{n},d_{1},\dots,d_{m}),$

with unit given by the empty tuple.

######  Remark 4.2.

The symmetric monoidal category $\mathsf{Env}(\mathbf{P})$ has appeared under
many different names throughout the years. They initially appeared under the
name of PROP in [5], connected to the study of cohomology operations by Adams
and Mac Lane. In this work we are working with the notion of a coloured PROP,
which is the one also appearing in the work of Boardman and Vogt in [1], but
not the one used by Hackney and Robertson in [4].

For a great survey on the history of PROPs see [7], and for more on coloured
operads [4] is a good resource.

###  4.1. Interpreting $\mathsf{Fin}_{\ast}$ as a category of forests

We will begin by defining a certain category of forests $\mathbb{F}$ which
will be useful in keeping track of the combinatorics of
$\mathsf{Env}(\mathbf{P})$. By a forest we mean a finite (possibly empty)
collection of trees $\\{T_{i}\in\mathsf{\Omega}:i=1,\dots,n\\}$, which we will
usually denote by $\bigoplus_{i=1}^{n}T_{i}$, and in the special case where
all the $T_{i}$’s are the same tree $T$, we abbreviate the notation to $n\cdot
T$. We note that we can view any forest $\bigoplus_{i=1}^{n}T_{i}$ as the
coproduct of representables $\coprod_{i=1}^{n}T_{i}$ in $\mathsf{dSets}$,
which we be useful at times. We also allow for the possibility of an empty
forest, which we write $\emptyset$.

The category $\mathbb{F}$ is actually isomorphic to the category of finite
pointed sets $\mathsf{Fin}_{\ast}$, but it is useful to have this formulation
of the latter category in terms of forests for the subsequent results. This is
done as follows:

  * $\diamond$

A pointed set $\langle n\rangle=\\{1,\ldots,n\\}\cup\\{\ast\\}$ will be
represented by the forest $n\cdot\eta$, which is $\emptyset$ whenever $n=0$.

  * $\diamond$

A function of pointed sets $\alpha\colon\langle m\rangle\to\langle n\rangle$
is given by a forest

$F=\left(\bigoplus_{j=1}^{n}C_{\lvert\alpha^{-1}(j)\rvert}\right)\oplus\lvert\alpha^{-1}(\ast)\rvert\cdot\eta,$

together with an injective function $\mathsf{input}\colon\underline{m}\to
E(F)$ with image the edges of the corollas and the copies of $\eta$, and
satisfying the relation that the set $\mathsf{input}(\alpha^{-1}(j))$ is the
leaf set of $C_{\lvert\alpha^{-1}(j)\rvert}$, for each $1\leq j\leq n$.

We will graphically represent the information of $\alpha$ in terms of a forest
of the form

$\times$$\times$$\cdot$$\cdot$$\cdot$$\times$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$

where the edges with the symbol $\times$ correspond to the copies of $\eta$,
and the function $\mathsf{input}$ labels the leaves of the corollas. The
target map is given by keeping all the edges at the level of the roots, and
the source by keeping all the edges at the level of the leaves, which includes
the edges above the symbol $\times$.

  * $\diamond$

Given composable morphisms

$\ell\cdot\eta\xlongrightarrow{(F_{1},\mathsf{input}_{1})}m\cdot\eta\xlongrightarrow{(F_{2},\mathsf{input}_{2})}n\cdot\eta$

the composition is given by the pair $(G,\mathsf{input}_{1})$. Here $G$ is
obtained by first grafting $F_{1}$ along the leaves of $F_{2}$ (we attach the
$i^{th}$ copy of $\eta$ in $m\cdot\eta$ to the leaf of $F_{2}$ with the label
$\mathsf{input}_{2}(i)$) and then contracting the edges that are identified.

More generally, a $k$-simplex in $\mathsf{Fin}_{\ast}$

$\langle n_{0}\rangle\xrightarrow{\alpha_{1}}\langle
n_{1}\rangle\xrightarrow{\alpha_{2}}\cdots\xrightarrow{\alpha_{k-1}}\langle
n_{k-1}\rangle\xrightarrow{\alpha_{k}}\langle n_{k}\rangle,$

will be given by a string

$n_{0}\cdot\eta\xrightarrow{(F_{1},\mathsf{input}_{1})}n_{1}\cdot\eta\longrightarrow\cdots\longrightarrow
n_{k-1}\cdot\eta\xrightarrow{(F_{k},\mathsf{input}_{k})}n_{k}\cdot\eta,$

which is encoded by the triple $(F,\mathsf{input}_{1})$, where $F$ is the
forest obtained via grafting the $F_{i}$’s in a similar fashion to what was
done when describing the composition, and $\mathsf{input}_{1}$ labels the
leaves of $F$. This reformulation defines a category isomorphic to
$\mathsf{Fin}_{\ast}$, which we will denote by $\mathbb{F}$.

######  Example 4.3.

Consider the 3-simplex in $\mathbb{F}$

$5\cdot\eta\xrightarrow{F_{1}}4\cdot\eta\xrightarrow{F_{2}}3\cdot\eta\xrightarrow{F_{3}}\eta,$

pictorially represented by the forests

$F_{1}\colon$$\times$$F_{2}\colon$$\times$$\times$$F_{3}\colon$

For the sake of simplicity, we have omitted the labelling for the inputs and
outputs, but it should be understood that they are labelled increasingly from
left to right. The forest $F$ associated to such a 3-simplex is the forest $F$
below

$\times$$\times$$\times$$F\colon$

One can also describe the action of the simplicial face maps
$\partial_{i}\colon N\mathbb{F}_{3}\to N\mathbb{F}_{2}$ on the 3-simplex in
question in terms of the forest $F$ (here we will again ignore the action of
the face maps on the labelling data):

  * $\diamond$

$\partial_{0}F$ is obtained by removing the $\times$ symbol from trees 2 and
3, and applying the root face to tree 4.

  * $\diamond$

$\partial_{1}F$ is obtained by removing the $\times$ symbol from tree 1,
applying the root face to trees 2 and 3, and contracting $w$ in tree 4. When
the root face is applied to trees 2 and 3, the symbol $\times$ propagates to
the newly-obtained trees.

  * $\diamond$

$\partial_{2}F$ is obtained by applying the root face to tree 1, contracting
$x,y$ and $z$ in trees 2 and 3, and removing the stump in tree 4.

  * $\diamond$

$\partial_{3}F$ is obtained by applying the leaf faces in trees 1, 2 and 3.

It is not difficult to deduce from this the general pattern of the face maps
on a generic element of $N\mathbb{F}_{k}$, by removing and contracting certain
"layers" of the associated forest.

From now on we will ignore the information on a $k$-simplex of $N\mathbb{F}$
given by the labelling, and instead think of such a simplex as a certain
forest $F$. In particular, this means that we can see each simplex in
$N\mathbb{F}$ as a dendroidal set, as we explained at the start of the
section. Before delving into the technical results we will need, we will
present some useful definitions.

######  Definition 4.4.

Let $k\geq 1$ and $F$ a $k$-simplex in $N\mathbb{F}$.

  1. (a)

We say a component tree $T$ of $F$ is uprooted if its graphical representation
corresponds to a tree containing the symbol $\times$.

  2. (b)

We write $\partial_{\mathrm{rl}}F\subseteq F$ for the dendroidal subset given
by the union of the faces $\partial_{0}F\cup\partial_{k}F\subseteq F$.

  3. (c)

For $0\leq j\leq n$, we write $\Lambda^{j}F\subseteq F$ for the dendroidal set
given by the union of all faces $\partial_{i}F$ such that $i\neq j$.

The next two lemmas will be the main technical results that will be used in
the next section. We point out that here is where we will make heavy use of
the right cancellation property for inner anodynes, which lets us avoid
complicated combinatorial arguments about the dendroidal category.

######  Lemma 4.5.

Let $k\geq 2$ and $F\in N\mathbb{F}_{k}$. Then the dendroidal inclusion
$\partial_{\mathrm{rl}}F\to F$ is inner anodyne.

###### Proof.

Let us start by making some simplifying assumptions on $F$:

  * $\diamond$

We can assume that $F$ is a tree $T$ since the action of the face maps
$\partial_{0}$ and $\partial_{k}$ can be restricted to each component of $F$.

  * $\diamond$

We can further assume that $T$ is not uprooted: we would then have the
equality $\partial_{0}T=T$ as dendroidal sets and therefore
$\partial_{\mathrm{rl}}T=T$.

  * $\diamond$

If $k=2$ then $\partial_{\mathrm{rl}}T\to T$ is the spine inclusion of $T$,
which is always inner anodyne by [3, Lem. 6.37]. Therefore we may additionally
assume $k\geq 3$.

Before discussing the general case, we will first exemplify what happens when
$k=3$: writing $T$ as a grafting $C_{n}\circ(T_{1},\ldots,T_{n})$ for $n\geq
0$, then the dendroidal set $\partial_{0}F$ is $T_{1}\cup\cdots\cup T_{k}$,
and therefore the inclusion $\partial_{\mathrm{rl}}T\to T$ will correspond to

$j\colon T_{1}\cup\cdots\cup T_{n}\cup\partial_{3}T\longrightarrow T,$

where we note that the trees $T_{1},\ldots,T_{n}$ and $\partial_{3}T$ are
elements of $N\mathbb{F}_{2}$. We can now apply $\partial_{\mathrm{rl}}$ to
each of the components of the domain of $j$, leading to the string of
composable maps

$\partial_{\mathrm{rl}}^{2}T:=\partial_{\mathrm{rl}}T_{1}\cup\cdots\cup\partial_{\mathrm{rl}}T_{n}\cup\partial_{\mathrm{rl}}(\partial_{3}T)\xlongrightarrow{i}T_{1}\cup\cdots\cup
T_{n}\cup\partial_{3}T\xlongrightarrow{j}T.$

The dendroidal inclusion $ji\colon\partial_{\mathrm{rl}}^{2}(T)\to T$ is inner
anodyne, since it coincides with the spine inclusion of $T$. Moreover, $i$ is
also inner anodyne by the induction hypothesis. We can now apply the right
cancellation property for inner anodynes to conclude that $j$ is also inner
anodyne, as we wanted to show.

For the general case, we first note that we can extend the previous definition
of $\partial_{\mathrm{rl}}^{2}T$ to arbitrary higher powers
$\partial_{\mathrm{rl}}^{n}T$ by inductively applying the operator
$\partial_{\mathrm{rl}}$ to each component of $\partial_{\mathrm{rl}}^{n-1}T$.
For a general $T\in N\mathbb{F}_{k}$, we consider now the dendroidal
inclusions

$\partial_{\mathrm{rl}}^{k-1}T\longrightarrow\partial_{\mathrm{rl}}T\longrightarrow
T.$

We see that the composite is again just the spine inclusion, and
$\partial_{\mathrm{rl}}^{k-1}T\rightarrow\partial_{\mathrm{rl}}T$ is inner
anodyne by the induction hypothesis. Consequently, another application of
Theorem 1.3 finishes the proof. ∎

######  Lemma 4.6.

Let $k\geq 2$ and $F\in N\mathbb{F}_{k}$. Then, for each $0<j<k$, the horn
inclusion $\Lambda^{j}F\to F$ is dendroidal inner anodyne.

###### Proof.

The case when $k=2$ is exactly Lemma 4.5, so we can assume that $k\geq 3$ from
now on. Furthermore, by the type of arguments as at the start of the previous
lemma, we can additionally assume that $F$ has no uprooted components.

For $0\leq\ell\leq k-1$, set $\partial_{\leq\ell}F\subseteq\Lambda^{j}F$ to be
the dendroidal subset obtained from $\partial_{\mathrm{rl}}F$ by attaching the
faces $\partial_{i}F$, with $0\leq i\leq\ell$ and $i\neq j$, which leads to a
filtration

$\partial_{\mathrm{rl}}F=\partial_{\leq 0}F\subseteq\partial_{\leq
1}F\subseteq\cdots\subseteq\partial_{\leq k-1}F=\Lambda^{j}F.$

It suffices to show that each stage of this filtration is inner anodyne:
indeed, the previous lemma together with the right cancellation property for
inner anodynes applied to $\partial_{\mathrm{rl}}F\to\Lambda^{j}F\to F$ will
then finish the proof.

The first stage of the filtration can be represented via the following pushout
square in $\mathsf{dSets}$:

${{\partial_{\mathrm{rl}}\partial_{1}F}}$${{\partial_{\mathrm{rl}}F}}$${{\partial_{1}F}}$${{\partial_{\leq
1}F}}$$\scriptstyle{\lrcorner}$

The left map is inner anodyne by Lemma 4.5 and therefore so is
$\partial_{\mathrm{rl}}F\to\partial_{\leq 1}F$. For the higher stages of the
filtration we have instead the description below:

${{\partial_{\leq i-1}\left(\partial_{i}F\right)}}$${{\partial_{\leq
i-1}F}}$${{\partial_{i}F}}$${{\partial_{\leq i}F}}$$\scriptstyle{\lrcorner}$

Since $\partial_{i}F\in N\mathbb{F}_{k-1}$, we conclude that $\partial_{\leq
i-1}\left(\partial_{i}F\right)\to\partial_{i}F$ is inner anodyne, by the
induction hypothesis on both the height $k$ of the forest and on the stage of
the filtration $i$. By the closure of inner anodynes under pushouts, the same
holds for $\partial_{\leq i-1}F\to\partial_{\leq i}F$, as we wanted to show. ∎

###  4.2. The symmetric monoidal envelope of a dendroidal $\infty$-operad

The reason for introducing and discussing the category $\mathbb{F}$ in the
previous section is that it will help us encode the symmetric monoidal
structure of $\mathsf{Env}(\mathbf{P})$. However, this will not be enough for
our purposes, since we also need to keep track of the colours of our operad.
Instead, we will consider a slightly more elaborate version of $\mathbb{F}$,
which we introduce now.

######  Definition 4.7.

The category of decorated forests $\mathbb{F}^{\text{dec}}$ is the category
given by the following data:

  * $\diamond$

An object is given by an $n$-tuple $(M_{1},\ldots,M_{n})$ for $n\geq 0$, where
each $M_{i}$ is the forest $k_{i}\cdot\eta$ for some integer $k_{i}\geq 0$.
Such an $n$-tuple partitions the edges of the forest
$\bigoplus_{i=1}^{n}M_{i}$.

  * $\diamond$

A morphism in $\mathbb{F}^{\text{dec}}$

$(L_{1},\ldots,L_{\ell})\xlongrightarrow{(\beta,F)}(M_{1},\ldots,M_{m})$

is given by a function of finite pointed sets
$\beta\colon\langle\ell\rangle\to\langle m\rangle$, together with a forest $F$
which is a morphism of $\mathbb{F}$. Additionally, these must interact with
each other in the following way:

    1. (a)

The root edges of $F$ are partitioned according to the $M_{i}$’s, and all the
remaining edges of $F$ (these are the leaves of the corollas and the edges of
the uprooted components) are partitioned according to the $L_{j}$’s.

    2. (b)

The set of leaves over the edges in $M_{i}$ is the union of the edges
contained in the $L_{j}$’s satisfying $\beta(j)=i$.

The identity morphism will correspond to seeting $\beta$ to be the
corresponding identity function, and $F$ is a forest of only 1-corollas.

  * $\diamond$

The composition of the morphisms

$(L_{1},\ldots,L_{\ell})\xlongrightarrow{(\beta_{1},F_{1})}(M_{1},\ldots,M_{m})\xlongrightarrow{(\beta_{2},F_{2})}(N_{1},\ldots,N_{n})$

is the pair $(\beta_{2}\beta_{1},F_{2}F_{1})$, where $F_{2}F_{1}$ comes from
the composition in $\mathbb{F}$, see Remark 4.8 for a clarification on how the
grafting is done.

######  Remark 4.8.

As we have done before, when defining the morphisms in
$\mathbb{F}^{\text{dec}}$ we have omitted the information regarding the
function $\mathsf{input}$ that labels the inputs of $F$. However, the set up
of $\mathbb{F}^{\text{dec}}$ gives a canonical choice of such a labelling:
indeed, the leaves of $F$ form the forest of edges
$\bigoplus_{i=1}^{\ell}L_{i}$, which is ordered via the internal ordering of
each $L_{i}$, together with the usual order of the indexing set
$\\{1,\ldots,\ell\\}$. This is the labelling which is assumed when defining
the composition in $\mathbb{F}^{\text{dec}}$.

######  Example 4.9.

One should think of the simplices of $\mathbb{F}^{\text{dec}}$ as being the
same as the simplices of $\mathbb{F}$, except that now each "layer" of edges
in the forest is partitioned in some fashion. As an example, we can consider
the following example of a 3-simplex in $\mathbb{F}^{\text{dec}}$

$(A_{1},A_{2},A_{3})\xrightarrow{(\beta_{1},F_{1})}(B_{1},B_{2},B_{3})\xrightarrow{(\beta_{2},F_{2})}(C_{1},C_{2})\xrightarrow{(\beta_{3},F_{3})}D_{1},$

where each $(\beta_{i},F_{i})$ can be graphically represented as shown below:

$F_{1}\colon$$A_{2}$$B_{1}$$A_{1}$$A_{3}$$B_{2}$$B_{3}$$\times$$F_{2}\colon$$B_{1}$$B_{2}$$C_{1}$$C_{2}$$B_{3}$$\times$$\times$$F_{3}\colon$$C_{1}$$C_{2}$$D_{1}$

The horizontal lines correspond to the partitions of the leaves and edges of
the respective forests, and the omitted information regarding the $\beta_{i}$
can be easily read off from the picture: for instance, $\beta_{2}\colon\langle
3\rangle\to\langle 2\rangle$ is given by $\beta_{2}(1)=\ast$ and
$\beta_{2}(2)=\beta_{2}(3)=1$. The forest $F$ associated to such a 3-simplex
is shown below, together with the corresponding partition of the edges:

$\times$$\times$$\times$$F\colon$$B_{1}$$A_{2}$$B_{2}$$C_{1}$$A_{1}$$A_{3}$$B_{3}$$D_{1}$$C_{2}$

As Example 4.9 shows, we can think of a general $k$-simplex of
$\mathbb{F}^{\text{dec}}$ as a forest $F\in N\mathbb{F}_{k}$ together with a
partition of its edges, and the face/degeneracy maps of
$N\mathbb{F}^{\text{dec}}$ operate on the forest $F$ in the same as they do in
$N\mathbb{F}$. As we will be particularly concerned with how these maps act,
we will often omit the partition information of a $k$-simplex in $N\mathbb{F}$
and only write the associated forest $F$.

######  Definition 4.10.

Let $X$ be a dendroidal set. The symmetric monoidal envelope of $X$ is the
simplicial set $\mathsf{Env}(X)^{\otimes}$ with set of $k$-simplices given by

$\mathsf{Env}(X)^{\otimes}_{k}=\coprod_{F\in
N\mathbb{F}^{\text{dec}}_{k}}X_{F},$

where we write $X_{F}=X_{T_{1}}\times\cdots\times X_{T_{n}}$ whenever $F$ is
the forest $\bigoplus_{i=1}^{n}T_{i}$.

The simplicial face and degeneracy maps act on $\mathsf{Env}(X)^{\otimes}$ via
the simplicial structure on the indexing simplicial set
$\mathbb{F}^{\text{dec}}$. Here we are also using that the simplicial
morphisms act on the forests $F\in N\mathbf{F}_{k}$ via dendroidal maps.

Letting $\mathsf{part}\colon N\mathbb{F}^{\text{dec}}\to N\mathsf{Fin}_{\ast}$
be the functor that retains the information about the partitions, we can see
$\mathsf{Env}(X)^{\otimes}$ as a simplicial set over the nerve of finite
pointed sets via the composite of

$\mathsf{Env}(X)^{\otimes}\longrightarrow
N\mathbb{F}^{\text{dec}}\xlongrightarrow{\mathsf{part}}N\mathsf{Fin}_{\ast},$

where $\mathsf{Env}(X)^{\otimes}\to N\mathbb{F}^{\text{dec}}$ just projects
onto the respective component of the coproduct defining
$N\mathbb{F}^{\text{dec}}$.

######  Proposition 4.11.

Let $X$ be a dendroidal $\infty$-operad. Then the functor
$\mathsf{Env}(X)^{\otimes}\to N\mathsf{Fin}_{\ast}$ exhibits
$\mathsf{Env}(X)^{\otimes}$ as a symmetric monoidal $\infty$-category in the
sense of Lurie.

###### Proof.

Letting $\Phi$ denote the functor $\mathsf{Env}(X)^{\otimes}\to
N\mathsf{Fin}_{\ast}$, we need to check the following properties:

  1. (a)

$\Phi$ is an inner fibration, which is equivalent to showing that
$\mathsf{Env}(X)^{\otimes}$ is an $\infty$-category.

  2. (b)

$\Phi$ is a cocartesian fibration.

  3. (c)

For each $n\geq 1$, the product of the functions $\rho^{j}\colon\langle
n\rangle\to\langle 1\rangle$, defined for each $1\leq j\leq n$ and determined
by the condition $(\rho^{j})^{-1}(1)=\\{j\\}$, induces a map

$\mathsf{Env}(X)^{\otimes}_{\langle
n\rangle}\longrightarrow\prod_{j=1}^{n}\mathsf{Env}(X)^{\otimes}_{\langle
1\rangle}$

which is an equivalence of $\infty$-categories.

For (a) we need to construct horn fillers

${{\Lambda^{j}[k]}}$${\mathsf{Env}(X)^{\otimes}}$${{\Delta[k]}}$

for the inner horn inclusions, that is, when $0<j<k$. We begin by observing
that, by the construction of $\mathsf{Env}(X)^{\otimes}$, there is a similar
associated extension problem for the nerve of $\mathbb{F}^{\text{dec}}$

$\leavevmode\hbox to88.39pt{\vbox
to53.92pt{\pgfpicture\makeatletter\hbox{\hskip
44.19455pt\lower-26.95833pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-44.19455pt}{-26.95833pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
14.6293pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.32376pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\Lambda^{j}[k]}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
14.6293pt\hfil&\hfil\hskip 41.56523pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.25972pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${N\mathbb{F}^{\text{dec}},}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
17.56526pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
14.01042pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.70488pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\Delta[k]}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
14.01042pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-14.73595pt}{10.86115pt}\pgfsys@lineto{8.46407pt}{10.86115pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.66405pt}{10.86115pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-29.56525pt}{2.00143pt}\pgfsys@lineto{-29.56525pt}{-15.19865pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-29.56525pt}{-15.39864pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{2.79985pt,1.59991pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-15.47307pt}{-15.59862pt}\pgfsys@lineto{13.08226pt}{2.34421pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.84673}{0.53204}{-0.53204}{0.84673}{13.25159pt}{2.45059pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
which has a (unique) solution, since it relates to the nerve of a category. As
we have already discussed, one can think of this newly constructed $k$-simplex
in $N\mathbb{F}^{\text{dec}}$ as a forest $F$, with each layer of edges
partitioned in some fashion. Using this language, we are left with arguing
that the following diagram in $\mathsf{dSets}$

$\leavevmode\hbox to67.68pt{\vbox
to48.15pt{\pgfpicture\makeatletter\hbox{\hskip
33.84106pt\lower-24.07608pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-33.84106pt}{-24.07608pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
13.00082pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.69528pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\Lambda^{j}F}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
13.00082pt\hfil&\hfil\hskip 32.84023pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.53471pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${X}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.84026pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.21527pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.90973pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${F}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.21527pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.63942pt}{10.5767pt}\pgfsys@lineto{15.5606pt}{10.5767pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.76057pt}{10.5767pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-20.84024pt}{4.217pt}\pgfsys@lineto{-20.84024pt}{-12.9831pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-20.84024pt}{-13.18307pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{2.79985pt,1.59991pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.42497pt}{-15.6758pt}\pgfsys@lineto{15.63313pt}{4.00906pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.81863}{0.57433}{-0.57433}{0.81863}{15.79684pt}{4.12392pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},$

admits the dashed lift, where $\Lambda^{j}F$ are the horns of Definition 4.4.
By Lemma 4.6 we have that $\Lambda^{j}F\to F$ is a dendroidal inner anodyne,
and consequently the desired morphism exists due to $X$ being an
$\infty$-operad.

For (b), suppose we are given a map of finite pointed sets $\beta\colon\langle
n\rangle\to\langle k\rangle$ together with a lift of its source to
$\mathsf{Env}(X)^{\otimes}$. Such a lift corresponds to an object
$(A_{1},\ldots,A_{n})$ in $\mathbb{F}^{\text{dec}}$, together with an
$A$-tuple $\vec{c}=(c_{1},\ldots,c_{A})\in X_{\eta}^{\times A}$, where
$A=\lvert A_{1}\rvert+\cdots+|A_{n}\rvert$, coming from evaluating $X$ on the
forest $\bigoplus_{i=1}^{n}A_{i}$. We also write $A_{\ast}$ for the sum of the
cardinalities $\lvert A_{i}\rvert$ ranging over $i\in\alpha^{-1}(\ast)$.

We first define a lift $(B_{1},\ldots,B_{k})$ to $\mathbb{F}^{\text{dec}}$ of
the finite pointed set $\langle k\rangle$: simply set
$B_{j}=\bigoplus_{i\in\beta^{-1}(j)}A_{i}$ for each $1\leq j\leq k$, which is
the empty forest whenever $\beta^{-1}(j)=\emptyset$. Let also $F\in
N\mathbb{F}_{1}$ be the forest obtained by first extending the edges of
$\bigoplus_{j=1}^{k}B_{j}$ to 1-corollas, and then adjoining $A_{\ast}$
components of uprooted trees of the form $\eta$.

Having constructed the pair $(\beta,F)$, we define the desired 1-simplex
$\tilde{\beta}$ in $\mathsf{Env}(X)^{\otimes}$ lifting $\beta$ as follows:

  1. (i)

$\tilde{\beta}$ is indexed by the morphism
$(\beta,F)\colon(A_{1},\ldots,A_{n})\longrightarrow(B_{1},\ldots,B_{k})$ in
$\mathbb{F}^{\text{dec}}$ that we defined in the pragraph above.

  2. (ii)

For each $1\leq j\leq k$, the value of $\tilde{\beta}$ on the 1-corollas
coming from $B_{j}$ is the image via the dendroidal map induced from the
degeneracy $C_{1}\to C_{0}$

$\prod_{i\in\beta^{-1}(j)}X_{A_{i}}\longrightarrow\prod_{i\in\beta^{-1}(j)}X_{C_{1}}^{\times\lvert
A_{i}\rvert}$

of the subtuple of $\vec{c}$ indexed by the elements of $A_{i}$.

  3. (iii)

The value of $\tilde{\beta}$ on $A_{\ast}\cdot C_{1}$ is given by the
remaining colours of $\vec{c}$ not mentioned in the previous case.

We claim that $\tilde{\beta}$ is a $\Phi$-cocartesian lift of $\beta$, which
comes down to checking that there is a diagonal lift in the diagram

${{\Lambda^{0}[m]}}$${\mathsf{Env}(X)^{\otimes}}$${{\Delta[m]}}$${N\mathsf{Fin}_{\ast}}$$\scriptstyle{\Phi}$

for $m\geq 2$, whenever the top horizontal map sends the initial edge
$\Delta^{\\{0,1\\}}$ to $\tilde{\beta}$. Unravelling the definitions and in a
similar fashion to what happened when proving part (a), this translates into
showing the existence in $\mathsf{dSets}$ of the dashed arrow $\tilde{x}$ in

${\Lambda^{0}G}$${X,}$${G}$$\scriptstyle{x}$$\scriptstyle{\tilde{x}}$

where $G\in N\mathbb{F}_{m}$ is a forest. Moreover, the initial edge of this
$m$-simplex $(\partial_{2}\cdots\partial_{m-1}\partial_{m})G\in
N\mathbb{F}_{1}$ is $F$, and the induced map $X_{G}\to X_{F}$ should send
$\tilde{x}$ to $\tilde{\beta}$.

We can assume that the forest $F$ only contains copies of $C_{1}$, or
equivalently that $\beta^{-1}(\ast)=\ast$: these components coming from the
fiber of the basepoint will only contribute to $G$ with uprooted trees of the
form $\eta$, and for such components the extension problem is trivial.
Assuming this, one can check that the desired extension is the image of $x$
via the composition of

$X_{\Lambda^{0}G}\xlongrightarrow{(\partial_{m-1}G\to\Lambda^{0}G)^{*}}X_{\partial_{m-1}G}\xlongrightarrow{(\sigma_{m}\partial_{m-1}G\to\partial_{m-1}G)^{*}}X_{\sigma_{m}\partial_{1}G}=X_{G},$

where $\sigma_{m}\colon N\mathbb{F}^{\text{dec}}_{m-1}\to
N\mathbb{F}^{\text{dec}}_{m}$ denotes the last degeneracy map. In the last
step we used the identification $\sigma_{m}\partial_{1}G=G$, which is due to
$F$ being a forest of 1-corollas.

For part (c), we have an isomorphism of categories

(3) $\mathbb{F}^{\text{dec}}_{\langle
n\rangle}\xlongrightarrow{\cong}\prod_{i=1}^{n}\mathbb{F}^{\text{dec}}_{\langle
1\rangle}.$

Here $\mathbb{F}^{\text{dec}}_{\langle n\rangle}$ is the subcategory of
$\mathbb{F}^{\text{dec}}$ over $\langle n\rangle$: a $k$-simplex in the nerve
of this category is a forest of linear trees which has been partitioned into
$n$ subforests, and (3) keeps track of each of these subforests. Using this
description, it readily follows that the induced map

$\mathsf{Env}(X)^{\otimes}_{\langle
n\rangle}\longrightarrow\prod_{i=1}^{n}\mathsf{Env}(X)^{\otimes}_{\langle
1\rangle}$

is an equivalence, as we wanted to show. ∎

######  Proposition 4.12.

Let $\mathbf{P}$ be a coloured operad. Then
$\mathsf{Env}(N\mathbf{P})^{\otimes}$ is the symmetric monoidal
$\infty$-category associated to the (strict) symmetric monoidal category
$\mathsf{Env}(\mathbf{P})$.

###### Proof.

One can easily describe the associated symmetric monoidal category
$\mathsf{Env}(N\mathbf{P})^{\otimes}_{\langle 1\rangle}$ from Definition 4.10
(note that since we are working over the object $\langle 1\rangle$, the
partition information does not exist):

  * $\diamond$

The set of objects of $\mathsf{Env}(N\mathbf{P})^{\otimes}_{\langle 1\rangle}$
is the coproduct $\coprod_{n\geq 0}N\mathbf{P}_{\eta}^{\times n},$ and
consequently an object is just a tuple of colours $(c_{1},\ldots,c_{n})$ of
$\mathbf{P}$, for $n\geq 0$.

  * $\diamond$

A morphism $(c_{1},\ldots,c_{m})\to(d_{1},\ldots,d_{n})$ will be given by an
$n$-tuple

$(p_{1},\ldots,p_{n})\in X_{C_{k_{1}}}\times\cdots\times X_{C_{k_{n}}},$

for integers $k_{i}\geq 0$ satisfying $\sum_{i}k_{i}=m$. Moreover, the
$c_{i}$’s and $d_{j}$’s are the values of $X$ on the leaves and roots of these
corollas, respectively.

This can be equivalently encoded by a function of sets
$f\colon\underline{m}\to\underline{n}$ where $f(i)=j$ if $c_{i}$ and $d_{j}$
belong to the same corolla, and operations $p_{j}$ in $\mathbf{P}$ with output
$d_{j}$ and inputs given by the $c_{i}$’s satisfying $f(i)=j$ ordered
according to $\underline{n}$.

  * $\diamond$

By the proof of part (c) of Proposition 4.11, the monoidal structure is
induced by the concatenation of forests $(F,G)\mapsto F\oplus G$. On
$\mathsf{Env}(N\mathbf{P})^{\otimes}_{\langle 1\rangle}$ this corresponds to
the concatenation of tuples of colours.

A quick comparison with Definition 4.1 readily shows that this coincides with
$\mathsf{Env}(\mathbf{P})$. It is also clear that
$\mathsf{Env}(N\mathbf{P})^{\otimes}$ is the usual construction of a symmetric
monoidal $\infty$-category from a strict symmetric monoidal category,
finishing the proof. ∎

## References

  * BV [73] J. Boardman and R. Vogt.  Homotopy invariant algebraic structures on topological spaces, volume 347.  Springer-Verlag, 1973.
  * CM [11] D.-C. Cisinski and I. Moerdijk.  Dendroidal sets as models for homotopy operads.  Journal of Topology, 4(2):257–299, 2011.
  * HM [22] G. Heuts and I. Moerdijk.  Simplicial and dendroidal homotopy theory.  Springer Nature, 2022.
  * HR [15] P. Hackney and M. Robertson.  On the category of props.  Applied Categorical Structures, 23:543–573, 2015.
  * Lan [63] S. Mac Lane.  Natural associativity and commutativity.  Rice University Studies, 49(4):28–46, 1963.
  * Lur [09] J. Lurie.  Higher Topos Theory.  Princeton University Press, 2009.
  * Mar [08] M. Markl.  Operads and PROPs.  Handbook of Algebra, 5:87–140, 2008.
  * MW [07] I. Moerdijk and I. Weiss.  Dendroidal sets.  Algebraic & Geometric Topology, 7:1441–1470, 2007.
  * Ste [18] D. Stevenson.  Stability for inner fibrations revisited.  Theory and Applications of Categories, 33(19):523–536, 2018.