# Strict stability of extension types

Jonathan Weinberger  Max Planck Institute for Mathematics, Vivatsgasse 7,
53111 Bonn, Germany<EMAIL_ADDRESS>
###### Abstract.

We show that the extension types occurring in Riehl–Shulman’s work on
synthetic $(\infty,1)$-categories can be interpreted in the intended semantics
in a way so that they are strictly stable under substitution. The splitting
method used here is due to Voevodsky in 2009. It was later generalized by
Lumsdaine–Warren to the method of _local universes_.
_MSC2020_ : 03B38 (Primary); 03G30, 18N45, 18N50, 18N60, 55U35 (Secondary)
_Keywords:_ homotopy type theory, simplicial type theory, extension types,
universes, split fibrations, strict substitution stability

I am grateful to the MPIM Bonn for its hospitality during final work on this
project. I thank Thomas Streicher and Ulrik Buchholtz for useful discussions
and explanations. For valuable feedback I am grateful to Emily Riehl and to
Nima Rasekh who also pointed out and corrected some references.

##  1\. Introduction

In this note, we carry out the splitting method described by Voevodsky in
[Voe09, Section 4], [Voe17], and recalled by Streicher [Str14b, Appendix C] to
show that the so-called _extension type_ in Riehl–Shulman’s _simplicial
homotopy type theory_ [RS17] can be interpreted in a way that makes them
strictly stable under substitution.

###  1.1. Synthetic $(\infty,1)$-category theory

In [RS17], Riehl–Shulman introduce simplicial homotopy type theory (sHoTT) as
a domain-specific language (DSL) to reason synthetically about
$(\infty,1)$-categories. As a standard model one can consider the Reedy model
structure on the simplicial presheaf category
$[{{\text{\raisebox{-0.43057pt}{\includegraphics[height=8.61108pt]{simplex}}}}}^{\operatorname{op}},{\mathbf{sSet}}_{\mathrm{Kan}}]$,
where ${\mathbf{sSet}}_{\mathrm{Kan}}$ denotes the category of simplicial sets
${\mathbf{sSet}}=[{{\text{\raisebox{-0.43057pt}{\includegraphics[height=8.61108pt]{simplex}}}}}^{\operatorname{op}},\mathbf{Set}]$
endowed with the Kan model structure. Accordingly, types get interpreted as
simplicial spaces. The syntax makes it possible to internally single out those
types that satisfy the _Segal condition_ (_i.e._ , weak composition of
$1$-arrows) and Rezk completeness (_i.e._ local univalence) which semantically
correspond to the complete Segal _aka_ Rezk spaces, known to implement
$(\infty,1)$-categories [Rez01, JT07, Ber18, RV22]. In general, for a (strict)
shape $\Phi$ [RS17, Section 2] the type $A^{\Phi}$ denotes the type of
functions from $\Phi$ to $A$, thought of as $\Phi$-shaped diagrams in $A$. The
Segal condition (in its internal form, after Joyal) is then expressed by
demanding the induced map $A^{\Delta^{2}}\to A^{\Lambda_{1}^{2}}$ to be a weak
equivalence [RS17, Sections 5 and 10].

###  1.2. Extension types

The theory of Segal and Rezk types makes crucial use of strict simplicial
shapes and _extension types_ [RS17, Section 3], the latter going back to
unpublished work of Lumsdaine–Shulman.111an instance of which is also to be
found as _path types_ in cubical type theory [CCHM18, OP16, Swa18] The
formation is as follows. Given a shape inclusion $\Phi\hookrightarrow\Psi$, a
type family $A:\Psi\to\mathcal{U}$, and a partial section
$a:\prod_{t:\Phi}A(t)$. The _extension type_
$\left\langle\mathchoice{\textstyle\prod_{\Psi}}{\textstyle\prod_{\Psi}}{\scriptstyle\prod_{\Psi}}{\scriptscriptstyle\prod_{\Psi}}A\middle|^{\Phi}_{a}\right\rangle$
consists of all strict totalizations of $a$, _i.e._ , sections
$b:\prod_{t:\Psi}A(t)$ such that $t:\Phi\vdash a(t)\equiv b(t)$, as indicated
in the following diagram:

${A}$${\Phi}$${\Psi}$$\scriptstyle{a}$$\scriptstyle{b}$

One reason why these extension types are important is that situations familiar
from (simplicial and categorical) homotopy theory can be conveniently and
homotopy-invariantly re-expressed in terms of them, such as right
orthogonality up to homotoy. Namely, let $\iota:\Phi\hookrightarrow\Psi$ be a
shape inclusion and $\pi:E\to B$ be a map between two types. In HoTT, we can
assume $\pi$ to be given as the projection
$\pi\equiv\mathrm{pr}_{1}:\big{(}\sum_{b:B}P(b)\big{)}\to B$ for a family
$P:B\to\mathcal{U}$ of $\mathcal{U}$-small types. Then, the shape inclusion
$\iota$ is right orthogonal to $\pi$, _i.e._ , the space of all fillers of any
diagram

${\Phi}$${E}$${\Psi}$${B}$$\scriptstyle{\iota}$$\scriptstyle{\alpha}$$\scriptstyle{\varphi}$$\scriptstyle{\pi}$

is contractible if and only if the proposition

$
\operatorname{isContr}\Big{(}\left\langle\mathchoice{\textstyle\prod_{t:\Psi}}{\textstyle\prod_{t:\Psi}}{\scriptstyle\prod_{t:\Psi}}{\scriptscriptstyle\prod_{t:\Psi}}P\big{(}\alpha(t)\big{)}\middle|^{\Phi}_{\varphi}\right\rangle\Big{)}$

holds.

To be able to literally make such and similar formulations inside our type
theory we reflect the tope into the type layer. This has been described in
[BW21, Section 2.4] and will be justified by our intended semantics, as we
will see next.

Indeed, continuing the program of [RS17], some parts of synthetic
$(\infty,1)$-category theory have recently in simplicial HoTT been developed
in [CRS18, BW21, Wei22, Mar22], and in [WL20] within a (bi-)cubical variant of
the theory. Many of these developments are crucially inspired by results from
Riehl–Verity’s _$\infty$ -cosmos theory_, a very general and powerful account
to model-independent $(\infty,n)$-category theory itself not formulated within
type theory. Hence, several constructions and results in sHoTT can be seen as
a type-theoretic translation of $\infty$-cosmological setting (at the moment
essentially confined to $(\infty,1)$-categorical reasoning, cf. [RS17,
Corollary 8.19]).

###  1.3. Internal $(\infty,1)$-categories

In fact, by Shulman’s far-reaching results [Shu19] about strictification of
univalent universes we can present any $(\infty,1)$-topos222in the sense of
Grothendieck–Rezk–Lurie [Rez10, TV05, Lur09], not necessarily in the sense of
the more recent, more general notion of  _elementary_ $(\infty,1)$-topos
[Shu17a, Ras22] by a suitably strict $1$-categorical structure, a _type-
theoretic model topos (TTMT)_. Hence, simplicial HoTT has models in all TTMTs
of the form
$\mathscr{E}^{{\text{\raisebox{-0.3014pt}{\includegraphics[height=6.02777pt]{simplex}}}}^{\operatorname{op}}}$
for an arbitrary given TTMT $\mathscr{E}$, where types get interpreted as
Reedy fibrant simplicial diagrams, and Segal or Rezk types, resp., as Segal or
Rezk objects, resp., cf. [BdB18, Ras17, RV22, Mar21, MW22, Mar22].

###  1.4. Strict stability of extension types

An axiomatic notion of model of simplicial type theory is given in [RS17,
Appendix A]. They prove that a wide class of model structures give rise to
models of simplicial homotopy type theory with _pseudo-stable_ extension
types. It is pointed out that one can use the splitting methods of Voevodsky
[Voe09, Voe17] and Lumsdaine–Warren [LW15] to rectify this to obtain _strictly
stable_ extension types in the model,  _i.e._ , the type formers commute with
substitutions _on the nose_.

In general, the basic idea behind the splitting is as follows. Given a lex
category $\mathscr{C}$ and a universe
$\pi:\widetilde{\mathcal{U}}\to\mathcal{U}$ in $\mathscr{C}$, one _chooses_
for every morphism $A:\Gamma\to\mathcal{U}$ a pullback:

${{\Gamma.A}}$${{\widetilde{\mathcal{U}}}}$${\Gamma}$${\mathcal{U}}$$\scriptstyle{p_{A}}$$\scriptstyle{A}$$\scriptstyle{q_{A}}$$\scriptstyle{\pi}$$\scriptstyle{\lrcorner}$

This yields a splitting of the full subfibration of the fundamental fibration
$\mathrm{cod}:\mathscr{C}^{[1]}\to\mathscr{C}$ that corresponds to the
universe $\pi$, cf. [Voe09, Section 4, Definition 0.1], [LW15, Section 1],
[Awo18, Subsection 1.1], [Str14b, Appendix C], [Rie22, Definition 2.4.2,
Digression 6.13], and Section 3.2.

###  1.5. Contribution

Our contribution consists in applying the splitting mentioned in Section 1.4
to the extension type formers in simplicial HoTT so as to make them strictly
stable under pullback. We are working w.r.t. to just one fixed universe.
Furthermore, the shapes are taken to be fibrant as well. This simplifies the
setting on a technically level while retaining its applicability to the class
of models of the form
$\mathrm{s}\mathscr{E}:={\mathscr{E}}^{{\text{\raisebox{-0.3014pt}{\includegraphics[height=6.02777pt]{simplex}}}}^{\operatorname{op}}}$
for a TTMT ${\mathscr{E}}$.

The work presented here is also to be found as [Wei22, Chapter 6] of the
author’s doctoral dissertation under the supervision of Thomas Streicher at TU
Darmstadt, Germany.

##  2\. Models of simplicial homotopy theory

###  2.1. Shulman’s type-theoretic model toposes

In [Shu19], Shulman provided the final missing part to establish the far-
reaching conjecture that any Grothendieck $(\infty,1)$-topos gives rise to a
model of homotopy type theory. Indeed, he proved that any such higher topos
can be presented by a model structure in which provides enough univalent
universes, validating propositional resizing, and which are _strictly_ closed
under all desired type formers.333with more general kinds of higher inductive
types being work in progress This had previously been established for certain
classes of special cases. [Shu15b, Shu15a, Shu17b, Cis14] More generally, work
connected to “internal languages” of higher categories is found in [AW09,
GK17, KL18, KS19, Kap17]. An excellent exposition of Shulman’s article is
given in Riehl’s mini-course notes [Rie22].

Given a type-theoretic model topos $\mathscr{E}$, the internal presheaf
category
$\mathrm{s}\mathscr{E}:=[{{\text{\raisebox{-0.43057pt}{\includegraphics[height=8.61108pt]{simplex}}}}}^{\operatorname{op}},\mathscr{E}]$
of simplicial objects in $\mathscr{E}$ is again a type-theoretic model
topos.444with the injective model structure [Shu19, Corollary 8.29] These are
the “standard models” for simplicial homotopy type theory. Inside any such
$\mathrm{s}\mathscr{E}$ we find a copy of the TTMT of spaces $\mathscr{S}$,
which is embedded fibrantly and spatially-discretely via the constant diagram
functor

${{\mathbf{Set}}}$${{\mathscr{E}}}$${\rightsquigarrow}$${{\mathscr{S}}}$${{\mathrm{s}\mathscr{E}\mathrlap{=\mathscr{E}^{{\text{\raisebox{-0.3014pt}{\includegraphics[height=6.02777pt]{simplex}}}}^{\operatorname{op}}}}}}$$\scriptstyle{\Delta_{\mathscr{E}}}$$\scriptstyle{\Gamma_{\mathscr{E}}}$$\scriptstyle{\Delta_{\mathrm{s}\mathscr{E}}}$$\scriptstyle{\Gamma_{\mathrm{s}\mathscr{E}}}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$

_i.e._ , the map given by

$\Delta_{s\mathscr{E}}:\mathscr{S}\hookrightarrow\mathscr{E},\quad
X\mapsto\Big{(}[n]\mapsto\coprod_{X_{n}}\mathbf{1}\Big{)}.$

We adapt the coherence construction used in [KL21, LW15, Awo18, Str14b,
Str14a, LS20], based on [Voe09, Voe17], so that in the model extension types à
la [RS17], going to back to earlier work by Lumsdaine and Shulman, can be
chosen in a way that is strictly stable under pullback.

Our presentation is inspired by [KL21, Awo18] and also [LW15] in method and
style. We define the type formers and the data required from the rules by
performing the corresponding constructions in suitable _generic contexts_.
Substitution then corresponds to precomposition with the reindexing map, and
applying type formers corresponds to postcomposition with an ensuing map
between universes. This implies strict substitution stability on the nose, in
particular avoiding choices of pullbacks (and dealing with the coherences that
would ensue).

This is done with respect to just a single universe as e.g. in [Awo18, Str14a,
Str14b]. Because extension types are similar to $\Pi$-types, the splitting is
also analogous to the method for $\Pi$-types from the aforementioned
sources.555Since the same ideas have successfully generalized from _global_ to
_local universes_ [LW15, Shu19], we believe the same generalization would also
work for strict extension types (which we do not consider in the present text,
however). In particular, a formulation in (an appropriate extension of)
Shulman’s setting [Shu19, Appendix A] should be possible.

We briefly recall Shulman’s setting and results that we are building on,
although we will rarely need to be explicit about the machinery under the hood
from here on.

A _type-theoretic model topos (TTMT)_ $\mathscr{E}$ ([Shu19, Definition 6.1],
[Rie22, Definition 6.1.1]) is given by a Grothendieck $1$-topos $\mathscr{E}$,
together with the structure of a right proper simplicial Cisinski model
category, which is in addition simplicially cartesian closed (_i.e._ ,
reindexing preserves simplicial copowers) and is also equipped with an
appropriate notion of “type-theoretic” fibration.666in Shulman’s terminology,
a _locally presentable_ and _relatively acyclic_ _notion of fibration
structure_ , satisfying in addition a “fullness” condition An immediate
example is given by the prime model of homotopy type theory, the type-
theoretic model topos of spaces $\mathscr{S}$, but there are many more
examples. In particular, the class of TTMTs is closed under typical
operations, such as slicing and small products, as well as passage to diagram
categories and internal localizations. Moreover, any
Grothendieck–Rezk–Lurie-$(\infty,1)$-topos can be presented by a type-
theoretic model topos. As a consequence, the study of Rezk types in simplicial
HoTT can be understood as a synthetic version of internal $\infty$-category
theory in an arbitrary given $(\infty,1)$-topos.

Crucially, any TTMT hosts enough777bounded from below by cardinal strict
fibrant univalent universes [Shu19, Theorem 5.22, Theorem 11.2].888as usual,
in a strong enough meta-theory such as ZFC with inaccessibles Abstractly from
the given fibration structure, the universes can be constructed using a
version of the small object argument [Shu19, Theorem 5.9]. Then a splitting
method due to Voevodsky [Voe09, KL21] akin to Giraud’s  _left adjoint
splitting_ [Gir71, LW15, Str14b] is applied to obtain _strict_ type formers
for these universes.

##  3\. Strict stability of extension types

###  3.1. General ideas

The rules for the extension types from [RS17] are recalled in Appendix A.

We adapt the coherence construction presented in [KL21, LW15, Awo18], based on
[Voe09, Voe17], so that in the model extension types à la [RS17] can be chosen
in a way that is strictly stable under pullback.

Our presentation is close to [KL21, Awo18] in style. We define the type
formers and the data required from the rules by performing the corresponding
constructions in suitable _generic contexts_. Substitution then corresponds to
precomposition with the reindexing map. Applying type formers/operations
corresponds to postcomposition with an ensuing map between universes. This
implies strict substitution stability on the nose.

We work w.r.t. just a single universe, as is also done in [Awo18]. The
extension types of [RS17, Figure 4] are both syntactically and semantically
similar to $\Pi$-types: Intuitively, the extension type
$\left\langle\mathchoice{\textstyle\prod_{\psi}}{\textstyle\prod_{\psi}}{\scriptstyle\prod_{\psi}}{\scriptscriptstyle\prod_{\psi}}A\middle|^{\varphi}_{a}\right\rangle$
consists of sections $b:\prod_{\psi}A$ that on the subshape
$\varphi\rightarrowtail\psi$ coincide with the given section $a$ in the sense
of _judgmental_ equality. Hence, they can be seen as a kind of “$\Pi$-types
with side conditions” (for functions whose domain is a tope, _a priori_ a
_pre_ -type).

Since in the case of ordinary $\Pi$-types the splitting method has been
generalized from _global_ to _local universes_ [LW15, Shu19], we believe the
same should also work for strict extension types (which we do not consider in
the present text, however). This has also been claimed in [RS17, Appendix
A.2].

In particular, a formulation in (an appropriate extension of) Shulman’s
setting [Shu19, Appendix A] should then be possible.

In contrast to most of [RS17, Appendix A] we will work completely internally
to the topos, disregarding the extra “non-fibrant” structure made explicit in
a _comprehension category with shapes_ [RS17, Definition A.5].

This is justified, because shapes are reflected into types by a newly added
rule, cf. [RS17, Section 2.4]:

$\inferrule{I\;\mathrm{cube}\\\
t:I\vdash\varphi\;\mathrm{tope}}{(t:I\;|\;\varphi)\;\mathrm{type}}$

In the model, this is validated because the simplicial shapes turn up as
(spatially-discrete) fibrant objects, cf. Section 2.1.

In sum, this allows us to focus the presentation on the splitting of the
extension types, without having to deal with also splitting the extra layers,
introducing universes for “cofibrations” or similar.999Even though all of this
should be possible if desired, cf. also the remarks about strict stability in
[RS17, Appendix A.2].

We will work in a classical meta-theory with global choice and universes.
Sometimes we use the internal extensional type theory (ETT) of the topos for
an easy-to-parse denotation of the objects presenting generic contexts. This
is along the lines of the presentation in [Awo18] and also [KL21, LW15].

As in [RS17, Theorem A.16], in the (injective) model structure of the TTMT
presenting $\mathrm{s}\mathscr{E}$ we interpret the extension types as
ordinary $1$-categorical pullbacks of Leibniz cotensors. Since the model
structure at hand is type-theoretic [Shu15b, Definition 2.12] the Leibniz
cotensors are fibrations, so are all their reindexings, which in particular
includes the (dependent) extension types.101010In the case of non-fibrant
shapes, the Leibniz cotensor is still a fibration because the model structure
is cartesian monoidal, cf. [RS17, Section 1, Section A.2]. In particular, the
ensuing pullbacks are homotopy pullbacks, cf. also [Lur09, Proposition A.2.4.4
and Remark A.2.4.5].

In the non-dependent case the extension type $\left\langle\psi\to
A\middle|^{\varphi}_{a}\right\rangle$ is thus given simply by (ordinary,
$1$-categorical) the pullback: For the dependent case the construction will
have to be relativized as we will see later on.

We want to show that the interpretation of the extension types can be chosen
in a strictly pullback-stable way. In particular, after [RS17, Definition
A.10, Theorem A.16] given a type family $A\twoheadrightarrow\Gamma\times\psi$
and a partial section $a:\Gamma\times\varphi\to_{\Gamma\times\psi}A$
substitution of the extension type111111Here and in the following, notation
such as $\Pi(A,B)$ or $\langle\Pi[\varphi][A]|^{\varphi}_{a}\rangle$ instead
of $\prod_{A}B$,
$\left\langle\mathchoice{\textstyle\prod_{\psi}}{\textstyle\prod_{\psi}}{\scriptstyle\prod_{\psi}}{\scriptscriptstyle\prod_{\psi}}A\middle|^{\varphi}_{a}\right\rangle$
designates the (strictly stable) type formers (to be) defined in the
interpretation, in line with [RS17, KL21, KL21, Awo18].
$\langle\Pi[\varphi][A]|^{\varphi}_{a}\rangle$ is only considered along (type)
context morphisms $\sigma:\Delta\to\Gamma$, leaving the shape inclusion
$j:\varphi\rightarrowtail\psi$ fixed. Hence, we will understand the type
former of the extension type as a _family_ of type formers ${\mathrm{Ext@}j}$,
given by

${\mathrm{Ext@}j}(A,a):=\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle$

indexed by the shape inclusions $j$.121212Note that, _a posteriori_ this also
yields stability w.r.t. to reindexing along cube context morphisms $\tau:J\to
I$ pulling back shape inclusions $j:\varphi\to_{I}\psi$: By their defining
universal property, which only involves a condition on reindexings of the type
context $\Gamma$, the (pseudo-stable) extension types from [RS17, Definition
A.10] are determined uniquely up to isomorphism. The splitting then yields
uniqueness up to equality. Then, considering reindexings along shape maps does
not lead out of this class, so the choice remains strictly stable.

The strict stability result can then be phrased as the following theorem:

######  Theorem 3.1 (Strict stability of extension types).

Let ${\mathscr{E}}$ be a type-theoretic model topos, and consider the
interpretation of simplicial homotopy type theory à la [RS17, Shu19] in the
type-theoretic model topos $\mathrm{s}\mathscr{E}$. Then, a fixed splitting of
the standard type formers induced by the universal fibration
$\pi:\widetilde{\mathcal{U}}\to\mathcal{U}$ for small fibrations yields an
interpretation of the extension types ${\mathrm{Ext@}j}$ (where
$j:\varphi\to_{I}\psi$ is a fixed shape inclusion relative to some cube $I$)
that is strictly stable under pullback. This means, for families
$A:\Gamma\times\psi\to\mathcal{U}$ and partial sections
$a:\Gamma\times\varphi\to_{\Gamma\times\psi}A$ we have:

$\displaystyle\sigma^{*}\big{(}{\mathrm{Ext@}j}(A,a)\big{)}$
$\displaystyle={\mathrm{Ext@}j}(\sigma^{*}A,\sigma^{*}a)$
$\displaystyle\sigma^{*}\big{(}{{\lambda\mathrm{@}j}}_{A,a}(b)\big{)}$
$\displaystyle={{\lambda\mathrm{@}j}}_{\sigma^{*}A,\sigma^{*}a}(\sigma^{*}b)$
$\displaystyle\sigma^{*}\big{(}{\mathrm{app@}j}_{A,a}(f,s)\big{)}$
$\displaystyle={\mathrm{app@}j}_{\sigma^{*}A,\sigma^{*}a}(\sigma^{*}f,\sigma^{*}s)$

In what we follows, we establish the proof of this theorem by splitting the
extension type formers, assuming all the necessary and pre-established logical
and model-categorical structure in the background.

###  3.2. Global universe splitting

Depending on the precise setup—in particular with extra shape layers—one might
have to use e.g. the local universe method [LW15] to strictify the _pseudo_
-stable tope logic beforehand [RS17, Definition A.7, Remark A.8]. But we will
neglect this here, as mentioned before, since we are staying inside the given
model structure on the topos, so it is enough just to a consider a splitting
of this.

A family in simplicial type theory is modeled by a composition

$A\twoheadrightarrow\Gamma\twoheadrightarrow\Phi\rightarrowtail\Xi,$

where $\Phi\rightarrowtail\Xi$ plays the role of a shape inclusion. Let
$\pi:\widetilde{\mathcal{U}}\to\mathcal{U}$ be the type-theoretic universe in
$\mathrm{s}\mathscr{E}$ (strictly à la Tarski, closed under all standard type
formers) which classifies small Reedy fibrations and which exists by [Shu19,
Corollary 8.29]. This means in particular we are considering the injective
model structure on internal presheaves, which in the case of the base
coincides with the Reedy model structure, cf. also [Cis14, Shu15a].

We just have to split w.r.t. the universe
$\pi:\widetilde{\mathcal{U}}\to\mathcal{U}$. This is done after Streicher
[Str14b, Appendix C] and Voevodsky [Voe09, Voe17] in the following way:

Using meta-theoretic global choice, for each family $A:\Gamma\to\mathcal{U}$,
we select a distinguished square

${{\Gamma.A}}$${{\widetilde{\mathcal{U}}}}$${\Gamma}$${\mathcal{U}}$$\scriptstyle{p_{A}}$$\scriptstyle{A}$$\scriptstyle{q_{A}}$$\scriptstyle{\pi}$$\scriptstyle{\lrcorner}$

A map from $B:\Delta\to\mathcal{U}$ and $A:\Gamma\to\mathcal{U}$ is given by a
square:

${{\Delta.B}}$${{\Gamma.A}}$${\Delta}$${\Gamma}$$\scriptstyle{p_{B}}$$\scriptstyle{\sigma}$$\scriptstyle{q_{\sigma}}$$\scriptstyle{p_{A}}$

which is split cartesian if and only if $B=A\circ\sigma$ and $q_{B}=q_{A}\circ
q_{\sigma}$:

${{\Delta.B}}$${{\Gamma.A}}$${{\widetilde{\mathcal{U}}}}$${\Delta}$${\Gamma}$${\mathcal{U}}$$\scriptstyle{p_{B}}$$\scriptstyle{\sigma}$$\scriptstyle{A}$$\scriptstyle{q_{\sigma}}$$\scriptstyle{p_{A}}$$\scriptstyle{q_{A}}$$\scriptstyle{\pi}$$\scriptstyle{\lrcorner}$$\scriptstyle{q_{B}}$$\scriptstyle{B}$$\scriptstyle{\lrcorner}$

This then necessarily implies that the left-hand side is a pullback as well.
Since the identites involved are strict equalities between objects and
morphisms involving distinguished squares, this models substitution up to
equality on the nose by defining $\sigma^{*}A:=A[\sigma]:=A\circ\sigma$.

When defining the generic contexts à la [KL21], we often define them in the
internal extensional type theory (ETT) of the topos, as done in [Awo18, LW15].
In particular, given a map $f:B\to A$ the endofunctor defined via the adjoint
triple

$ \sum_{f}\dashv f^{*}\dashv\prod_{f}$

as

$ P_{f}(X)=\sum_{A\to 1}\Big{(}\prod_{f}(B^{*}(X))\Big{)}$

in the internal language ETT reads as

$P_{f}(X)=\sum_{a:A}X^{B_{a}},$

where $B_{a}=f^{*}a$.

Moreover, for $A:\Gamma\to\mathcal{U}$ we allow ourselves to abbreviate
$A:=\Gamma.A=\widetilde{\mathcal{U}}_{A}=\pi^{*}A$, as is commonly done.

For the universal fibration $\pi:\widetilde{\mathcal{U}}\to\mathcal{U}$, the
total object denotes the generic context

$ \widetilde{\mathcal{U}}=\sum_{A:\mathcal{U}}A=\llbracket
A:\mathcal{U},a:A\rrbracket.$

We show how to define a strictly stable choice of extension types à la [Awo18,
Proposition 2.4]. To illustrate the analogy, we give a brief recollection how
to define the generic contexts for the formation and introduction rule.

###  3.3. Recollection: Strictly stable $\Pi$-types

The generic context for the $\Pi$-formation rule is given, in the internal
language, by the type

$\mathcal{U}^{\Pi}:=\sum_{A:\mathcal{U}}\mathcal{U}^{A}=\llbracket
A:\mathcal{U},B:A\to\mathcal{U}\rrbracket,$

and the generic context for the introduction rule is given by

$
\mathcal{U}^{\lambda\mathrm{@}j}:=\sum_{A:\mathcal{U}}\sum_{B:A\to\mathcal{U}}\prod_{a:A}B(a)=\llbracket
A:\mathcal{U},B:A\to\mathcal{U},t:(a:A)\to B(a)\rrbracket,$

which captures the _generic dependent term_.

The idea is that a map $\langle A,B\rangle:\Gamma\to\mathcal{U}^{\Pi}$
precisely captures the input data for the $\Pi$-type former.

The universe then admits $\Pi$-types (cf.  _$\Pi$ -structure_, cf. [KL21,
Definition 1.4.2, Theorem 1.4.15]) if there exist maps
$\Pi:\mathcal{U}^{\Pi}\to\mathcal{U}$,
$\lambda:\mathcal{U}^{\lambda}\to\mathcal{U}$ making the square

${{\mathcal{U}^{\lambda}}}$${{\widetilde{\mathcal{U}}}}$${{\mathcal{U}^{\Pi}}}$${{\mathcal{U}}}$$\scriptstyle{\Pi}$$\scriptstyle{\lambda}$

commute, and moreover rendering as a pullback. These maps implement the
formation and introduction rule, hence we take the maps

$ \Pi:\mathcal{U}^{\Pi}\to\mathcal{U},~{}\Pi(A,B):=\prod_{A}B,\quad
\lambda:\mathcal{U}^{\Pi}\to\mathcal{U},~{}\lambda(A,B,t):=\Big{\langle}\prod_{A}(B),t\Big{\rangle}$

induced from the structure of the ambient category as a type-theoretic model
category.131313Concretely, for fibrations $p_{A}:\Gamma.A\to\Gamma$,
$p_{B}:\Gamma.A.B\to\Gamma.A$ we define $\Pi(A,B):=\prod_{p_{A}}(p_{B})$ via
the pushforward functor $\prod_{p_{A}}\vdash(p_{A})^{*}$ which in this setting
preserves fibrations.

In particular, for the formation rule, strict stability under pullback follows
from strict commutation of the diagram

${\Delta}$${\Gamma}$${{\mathcal{U}^{\Pi}}}$${\mathcal{U}}$$\scriptstyle{\langle
A,B\rangle}$$\scriptstyle{\Pi}$$\scriptstyle{\sigma}$$\scriptstyle{\prod_{\sigma^{*}A}\sigma^{*}B}$$\scriptstyle{\langle\sigma^{*}A,\sigma^{*}B\rangle}$$\scriptstyle{\prod_{A}B}$

as elaborated in [Awo18].

We now treat the extension types from [RS17] in a similar fashion.

###  3.4. Strictly stable extension types: Generic contexts

Recall the rules from [RS17, Figure 4].

To form an extension type, we start with a context fibered-over-shapes

$\Gamma\twoheadrightarrow\Phi\rightarrowtail\Xi$

and a _separate_ 141414The semantic reason for this is explained right before
[RS17, Theorem A.17]. Cf. also the explanation about the rules at the
beginning of [RS17, Section 2.2] shape inclusion

$\psi\rightarrowtail\varphi\rightarrowtail I.$

The extension type ist then formed for a pair $\langle A,a\rangle$ of a type
and a partial section

(1)
$A:\Gamma\times\psi\twoheadrightarrow\Phi\times\psi\rightarrowtail\Xi\times
I,\quad a:\Gamma\times\varphi\to_{\Gamma\times\psi}A$

In fact, the defining universal property for the extension types [RS17,
Definition A.10] asks for substitution (pseudo-)stability of $A$ and $a$ along
morphisms $\sigma:\Delta\to\Gamma$. Hence, we in fact consider a _family_ of
type formers $({\mathrm{Ext@}j})_{j:\varphi\rightarrowtail_{I}\psi}$ indexed
externally by the shape inclusions $j:\varphi\to\psi$, so that

$({\mathrm{Ext@}j})(A,a)=\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle.$

Thus, the input data to form the extension type ${\mathrm{Ext@}j}$ should be
represented using a suitable generic context $\mathcal{U}^{{\mathrm{Ext@}j}}$
as a morphism

$\langle A,a\rangle: \Gamma\to\mathcal{U}^{{\mathrm{Ext@}j}}$

with $\langle A,a\rangle$ as in (1).151515Note that we are suppress the
further structure $\Gamma\twoheadrightarrow\Phi\rightarrowtail\Xi$ here, in
line with [RS17, Definition A.10]. In analogy to the case of $\Pi$-types, we
form the generic contexts by

(2) $\displaystyle\mathcal{U}^{{\mathrm{Ext@}j}}$
$\displaystyle:=\sum_{A:\mathcal{U}^{\psi}}j^{*}A,$ (3)
$\displaystyle\mathcal{U}^{{\lambda\mathrm{@}j}}$
$\displaystyle:=\sum_{A:\mathcal{U}^{\psi}}\sum_{a:j^{*}A}a^{*}(A^{\psi}).$

###  3.5. Strictly stable extension types: Formation and introduction

The formation and introduction rule are, top to bottom, Rule 1 and 2, resp.,
in [RS17, Figure 4] (or cf. Figure 1).

Then, at stage $\Gamma$ the object $\mathcal{U}^{{{\lambda\mathrm{@}j}}}$
consists of triples $\langle A,a,b\rangle$ as in

${A}$${{\Gamma\times\varphi}}$${{\Gamma\times\psi}}$$\scriptstyle{\Gamma\times
j}$$\scriptstyle{a}$$\scriptstyle{b}$

_i.e._ , strictly $a=b\circ(\Gamma\times j)$. Considering the projection
$\mathcal{U}^{{{\lambda\mathrm{@}j}}}\to\mathcal{U}^{{\mathrm{Ext@}j}}$ the
fiber at an instance $\langle A,a\rangle$ is exactly the semantic extension
type

${\mathrm{Ext@}j}(A,a):=\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle$

defined by the _split_ 161616 _i.e._ ,
$\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle$ and its projection to $\Gamma$
have been _chosen_ cartesian square, after [RS17, Theorem A.16]:

${\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle}$${{A^{\psi}}}$${\Gamma}$${{A^{\varphi}\times_{(\Gamma\times\psi)^{\varphi}}(\Gamma\times\psi)^{\psi}}}$$\scriptstyle{\langle
a,\eta\rangle}$$\scriptstyle{\lrcorner}$

In particular, the right vertical map is a fibration,171717If shapes are taken
to be fibrant, this already follows from type-theoretic-ness of the model
structure. Otherwise one would have to use that the model structure is
cartesian monoidal as in [RS17, Lemma A.4]. so the object
${\mathrm{Ext@}j}(A,a)$ is fibrant.

Note that in the extensional type theory of the ambient topos one could
describe the extension type also as the $\Sigma$-type

$ \sum_{b:\psi\to A}(b\circ j\equiv a),$

where $(-_{1})\equiv(-_{2})$ stands for the extensional identity type.

Now, in analogy to [KV18, Theorem 1.4.15], we define the map
${\mathrm{Ext@}j}:\mathcal{U}^{{\lambda\mathrm{@}j}}\to\widetilde{\mathcal{U}}$
by the universal property of the extension type. The generic context
$\mathcal{U}^{{\lambda\mathrm{@}j}}$ consists of triples $\langle
A,a,b\rangle$ s.t.

${{A^{\psi}}}$${\Gamma}$${{A^{\varphi}\times_{{\Gamma\times\psi}^{\varphi}}(\Gamma\times\psi)^{\psi}}}$$\scriptstyle{b}$$\scriptstyle{\langle
a,\eta\rangle}$

where $\eta:\Gamma\to(\Gamma\times\psi)^{\psi}$ denotes the transpose of the
identity of $\Gamma\times\psi$. Now, we define the generic $\lambda$-term of
the extension type as the gap map $({{\lambda\mathrm{@}j}})(b):=\widehat{b}$
of the pullback:

${\Gamma}$${\langle\Pi[\psi][A]|^{\varphi}_{a}\rangle}$${{A^{\psi}}}$${\Gamma}$${{A^{\varphi}\times_{{\Gamma\times\psi}^{\varphi}}(\Gamma\times\psi)^{\psi}}}$$\scriptstyle{\langle
a,\eta\rangle}$$\scriptstyle{b}$$\scriptstyle{\widehat{b}}$$\scriptstyle{\lrcorner}$

Then, the square

${{\mathcal{U}^{{\lambda\mathrm{@}j}}}}$${\widetilde{\mathcal{U}}}$${{\mathcal{U}^{\mathrm{Ext@}j}}}$${\mathcal{U}}$$\scriptstyle{{\mathrm{Ext@}j}}$$\scriptstyle{{{\lambda\mathrm{@}j}}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$

being a pullback precisely captures the universal property as dicussed in
[RS17, Definition A.10, Theorem A.16]. In the terminology of [KL21, Theorem
2.3.4] this means that the projection
$\mathcal{U}^{{{\lambda\mathrm{@}j}}}\to\mathcal{U}^{{\mathrm{Ext@}j}}$ is the
_universal dependent extension type_ over $\mathcal{U}^{{\mathrm{Ext@}j}}$. In
particular, in presence of the splitting it is a _chosen_ small fibration.
Thus, as illustrated e.g. in [Awo18, Remark 2.6] we obtain strict pullback
stability: everything in

${\Delta}$${\Gamma}$${{\mathcal{U}^{{\mathrm{Ext@}j}}}}$${\mathcal{U}}$$\scriptstyle{\langle
A,a\rangle}$$\scriptstyle{{\mathrm{Ext@}j}}$$\scriptstyle{\sigma}$$\scriptstyle{({\mathrm{Ext@}j})(\sigma^{*}A,\sigma^{*}a)}$$\scriptstyle{\langle\sigma^{*}A,\sigma^{*}a\rangle}$$\scriptstyle{({\mathrm{Ext@}j})(A,a)}$

commutes strictly on the nose because we have split the model structure from
the get-go, yielding as desired

${\mathrm{Ext@}j}(A,a)\circ\sigma={\mathrm{Ext@}j}(A\sigma,a\sigma).$

Similarly, and using that the generic lifts $b$ are given by gap maps of
(strict) pullbacks we obtain

${\lambda\mathrm{@}j}(A,a,b)\circ\sigma={\mathrm{Ext@}j}(A\sigma,a\sigma,b\sigma).$

###  3.6. Strictly stable extension types: Elimination and computation

The elimination and computation rule are Rule 3 and 4, resp., in [RS17, Figure
4] (or cf. Figure 2).

To interpet the elimination rule, note first that the exponential $A^{\psi}$
comes with a (chosen) evaluation map:

${{A^{\psi}\times_{\Gamma}(\Gamma\times\psi)}}$${A}$${\Gamma}$$\scriptstyle{\mathrm{ev}}$

By pulling this back along the (chosen) map from the extension type, we obtain
a map

$\mathrm{ev}:{\mathrm{Ext@}j}(A,a)\times_{\Gamma}(\Gamma\times\psi)\to_{\Gamma}A,$

fibered over $\Gamma$. Now,we want to define application ${\mathrm{app@}j}$ of
a function $f:\Gamma\to_{\Gamma}{\mathrm{Ext@}j}(A,a)$ to a section
$s:\Gamma\to_{\Gamma}\Gamma\times\psi$. Analogously to [KL21, Theorem 1.4.15],
we take the composition:

${\Gamma}$${{{\mathrm{Ext@}j}(A,a)\times_{\Gamma}(\Gamma\times\psi)}}$${A}$${\Gamma}$$\scriptstyle{\langle
f,s\rangle}$$\scriptstyle{\mathrm{ev}}$$\scriptstyle{{\mathrm{app@}j}(f,s)}$

This validates the rule, since ${\mathrm{app@}j}(f,s):\Gamma\to_{\Gamma}A$, as
desired. For substitution along $\sigma:\Delta\to\Gamma$, consider the
following diagram involving chosen fibrations and split cartesian squares:

${{{\mathrm{Ext@}j}(\sigma^{*}A,\sigma^{*}a)\mathrlap{\times_{\Delta}(\Delta\times\psi)}}}$${{{\mathrm{Ext@}j}(A,a)\times_{\Gamma}(\Gamma\times\psi)}}$${{\sigma^{*}A}}$${A}$${\Delta}$${\Gamma}$$\scriptstyle{{\mathrm{app@}j}(\sigma^{*}f,\sigma^{*}s)}$$\scriptstyle{\langle\sigma^{*}f,\sigma^{*}a\rangle}$$\scriptstyle{{\mathrm{app@}j}(f,s)}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$$\scriptstyle{\langle
f,a\rangle}$

This uniquely defines the map ${\mathrm{app@}j}(\sigma^{*}f,\sigma^{*}s)$, and
by construction

$\sigma^{*}{\mathrm{app@}j}(f,s)={\mathrm{app@}j}(\sigma^{*}f,\sigma^{*}s). $

Furthermore the desired computation rule holds, saying that for a term $s$ in
the smaller tope $\varphi$, one judgmentally has ${\mathrm{app@}j}(f,s)\equiv
a[s]$. This is established by the commutation of the diagram:

${A}$${{\Gamma\times\varphi}}$${{\Gamma\times\psi}}$${\Gamma}$$\scriptstyle{\Gamma\times
j}$$\scriptstyle{a}$$\scriptstyle{s}$$\scriptstyle{f}$$\scriptstyle{{\mathrm{app@}j}(f,s)}$

The $\beta$\- and $\eta$-rule (cf. [RS17, Figure 4]) can be proven to hold
similarly (Rule 5 and 6, resp., in [RS17, Figure 4], or cf. Figure 3).

##  4\. Outlook

We have used Veovdosky’s splitting method from [Voe09, Section 4, Definition
0.1] to split the extension type formers from Riehl–Shulman’s synthetic
$(\infty,1)$-category theory [RS17].

Doing so, we have only worked using a single universe. We believe there to be
no essential problems generalizing this line of reasoning to the case of a
hierarchy of universes, cf. [LW15, Shu19, RS17]. We also worked in a
simplified technical setting with fibrant shapes, blurring the lines to the
pre-type layers which are treated quite explicitly in [RS17, Appendix A].
While this can be justified semantically, one could still try to adapt the
splitting to a setting more faithful to the original theory [RS17] and its
fibered structure/multi-part contexts. Already in [RS17] it is suggested that
it should be possible to do so along the lines of [LW15].

Yet another line of investigation could consist of trying to capture extension
types in the recent $2$-categorical framework of Coraglia–Di Liberti [CDL21].

##  Appendix A Rules for extension types

The rules for the extension types of sHoTT have been taken from [RS17, Figure
4]. In simplicial HoTT, a general typing judgment has the form

$\Xi\;|\;\Phi\;|\;\Gamma\vdash A\;\mathrm{type}$

where $\Xi$ denotes a cube context, $\Phi$ a shape context, and $\Gamma$ a
usual type context.

*[right = (Ext-Form)]{t:I∣ϕ} shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ
Ξ∣Φ⊢Γ ctx
Ξ,t:I ∣Φ,ψ∣Γ⊢A type
Ξ,t:I ∣Φ,ϕ∣Γ⊢a:A Ξ∣Φ∣Γ⊢⟨∏t:I ∣ψ A —^ϕ_a⟩ type*[right = (Ext-Intro)]{t:I∣ϕ}
shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ
Ξ∣Φ⊢Γ ctx
Ξ,t:I ∣Φ,ψ∣Γ⊢A type
Ξ,t:I ∣Φ,ϕ∣Γ⊢a:A

Ξ,t:I ∣Φ,ψ∣Γ⊢b:A
Ξ,t:I ∣Φ,ϕ∣Γ⊢b≡a Ξ∣Φ∣Γ⊢λt^I∣ψ. b : ⟨∏t:I ∣ψ A —^ϕ_a⟩

Figure 1. Extension types: formation and introduction

*[right = (Ext-Elim)]{t:I∣ϕ} shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ

Ξ∣Φ∣Γ⊢f:⟨∏t:I ∣ψ A —^ϕ_a⟩
Ξ⊢s:I
Ξ∣Φ⊢ψ[s/t] Ξ∣Φ∣Γ⊢f(s) : A*[right = (Ext-Comp)]{t:I∣ϕ} shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ

Ξ∣Φ∣Γ⊢f:⟨∏t:I ∣ψ A —^ϕ_a⟩
Ξ⊢s:I
Ξ∣Φ⊢ϕ[s/t] Ξ∣Φ∣Γ⊢f(s) ≡a[s/t]

Figure 2. Extension types: elimination and computation

*[right = (Ext-$\beta$)]{t:I∣ϕ} shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ
Ξ∣Φ⊢Γ ctx
Ξ,t:I ∣Φ,ψ∣Γ⊢A type
Ξ,t:I ∣Φ,ϕ∣Γ⊢a:A

Ξ,t:I ∣Φ,ψ∣Γ⊢b:A
Ξ,t:I ∣Φ,ϕ∣Γ⊢b≡a
Ξ⊢s:I
Ξ∣Φ⊢ψ[s/t] Ξ∣Φ∣Γ⊢(λt^I∣ψ. b)(s) ≡b[s/t]*[right = (Ext-$\eta$)]{t:I∣ϕ} shape
{t:I∣ψ} shape
t:I ∣ϕ⊢ψ

Ξ∣Φ∣Γ⊢f:⟨∏t:I ∣ψ A —^ϕ_a⟩
Ξ∣Φ∣Γ⊢f ≡λt^I∣ψ. f(t)

Figure 3. Extension types: $\beta$-conversion and $\eta$-abstraction

## References

  * [AW09] Steve Awodey and Michael A. Warren, _Homotopy theoretic models of identity types_ , Mathematical Proceedings of the Cambridge Philosophical Society 146 (2009), no. 1, 45–55.
  * [Awo18] Steve Awodey, _Natural models of homotopy type theory_ , Mathematical Structures in Computer Science 28 (2018), no. 2, 241–286.
  * [BdB18] Pedro Boavida de Brito, _Segal objects and the Grothendieck construction_ , An alpine bouquet of algebraic topology, Contemp. Math., vol. 708, Amer. Math. Soc., [Providence], RI, 2018, pp. 19–44. MR 3807750
  * [Ber18] Julia E. Bergner, _The homotopy theory of $(\infty,1)$-categories_, London Mathematical Society Student Texts, Cambridge University Press, 2018.
  * [BW21] Ulrik Buchholtz and Jonathan Weinberger, _Synthetic fibered $(\infty,1)$-category theory_, 2021, arXiv:2105.01724.
  * [CCHM18] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, _Cubical type theory: a constructive interpretation of the univalence axiom_ , 21st International Conference on Types for Proofs and Programs (TYPES 2015), LIPIcs. Leibniz Int. Proc. Inform., Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018.
  * [CDL21] Greta Coraglia and Ivan Di Liberti, _Context, Judgement, Deduction_ , arxiv:2111.09438.
  * [Cis14] Denis-Charles Cisinski, _Univalent universes for elegant models of homotopy types_ , 2014, arXiv:1406.0058.
  * [CRS18] Evan Cavallo, Emily Riehl, and Christian Sattler, _On the directed univalence axiom_ , 2018, Talk at AMS Special Session on Homotopy Type Theory, Joint Mathematics Meething, San Diego.
  * [Gir71] Jean Giraud, _Cohomologie non abélienne_ , Die Grundlehren der mathematischen Wissenschaften, Band 179, Springer-Verlag, Berlin-New York, 1971\. MR 0344253
  * [GK17] David Gepner and Joachim Kock, _Univalence in locally cartesian closed $\infty$-categories_, Forum Mathematicum 29 (2017), no. 3, 617–652.
  * [JT07] André Joyal and Myles Tierney, _Quasi-categories vs Segal spaces_ , Contemporary Mathematics 431 (2007), no. 277-326, 10.
  * [Kap17] Krzysztof Kapulkin, _Locally cartesian closed quasi-categories from type theory_ , J. Topol. 10 (2017), no. 4, 1029–1049. MR 3743067
  * [KL18] Krzysztof Kapulkin and Peter LeFanu Lumsdaine, _The homotopy theory of type theories_ , Adv. Math. 337 (2018), 1–38. MR 3853043
  * [KL21] by same author, _The simplicial model of Univalent Foundations (after Voevodsky)_ , Journal of the European Mathematical Society 23 (2021), no. 6, 2071–2126.
  * [KS19] Krzysztof Kapulkin and Karol Szumiło, _Internal languages of finitely complete $(\infty,1)$-categories_, Selecta Math. (N.S.) 25 (2019), no. 2, Paper No. 33, 46. MR 3943478
  * [KV18] Krzysztof Kapulkin and Vladimir Voevodsky, _Cubical approach to straightening_ , 2018, http://www.math.uwo.ca/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf.
  * [LS20] Peter LeFanu Lumsdaine and Michael Shulman, _Semantics of higher inductive types_ , Math. Proc. Cambridge Philos. Soc. 169 (2020), no. 1, 159–208. MR 4120789
  * [Lur09] Jacob Lurie, _Higher Topos Theory_ , Annals of Mathematics Studies, no. 170, Princeton University Press, 2009.
  * [LW15] Peter Lefanu Lumsdaine and Michael A. Warren, _The local universes model: An overlooked coherence construction for dependent type theories_ , ACM Trans. Comput. Logic 16 (2015), no. 3.
  * [Mar21] Louis Martini, _Yoneda’s lemma for internal higher categoriess_ , 2021, https://arxiv.org/abs/2103.17141.
  * [Mar22] César Bardomiano Martínez, _Limits and colimits of synthetic $\infty$-categories_, 2022, arXiv:2202.12386.
  * [MW22] Louis Martini and Sebastian Wolf, _Limits and colimits in internal higher category theory_ , 2022, https://arxiv.org/abs/2111.14495.
  * [OP16] Ian Orton and Andrew M. Pitts, _Axioms for modelling cubical type theory in a topos_ , 25th EACSL annual conference and 30th workshop on computer science logic, CSL’16, Marseille, France, August 29 – September 1, 2016\. Proceedings, Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik, 2016, Id/No 24, p. 19 (English).
  * [Ras17] Nima Rasekh, _Cartesian fibrations and representability_ , November 2017, To appear at HHA. arXiv:1711.03670.
  * [Ras22] Nima Rasekh, _A theory of elementary higher toposes_ , 2022, arXiv:1805.03805.
  * [Rez01] Charles Rezk, _A model for the homotopy theory of homotopy theory_ , Trans. Amer. Math. Soc. 353 (2001), no. 3, 973–1007.
  * [Rez10] Charles Rezk, _Toposes and homotopy toposes_ , 2010, Unpublished note. http://www.math.uiuc.edu/~rezk/homotopy-topos-sketch.pdf.
  * [Rie22] Emily Riehl, _On the $\infty$-topos semantics of homotopy type theory_, 2022, Lecture notes from CIRM Luminy, Logic and Higher Structures workshop. https://emilyriehl.github.io/files/semantics.pdf.
  * [RS17] Emily Riehl and Michael Shulman, _A type theory for synthetic $\infty$-categories_, Higher Structures 1 (2017), no. 1, 147–224.
  * [RV22] Emily Riehl and Dominic Verity, _Elements of $\infty$-Category Theory_, Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2022.
  * [Shu15a] Michael Shulman, _The univalence axiom for elegant Reedy presheaves_ , Homology Homotopy Appl. 17 (2015), no. 2, 81–106. MR 3421464
  * [Shu15b] by same author, _Univalence for inverse diagrams and homotopy canonicity_ , Math. Structures Comput. Sci. 25 (2015), no. 5, 1203–1277. MR 3340541
  * [Shu17a] Michael Shulman, _Elementary $(\infty,1)$-Topoi_, 2017, $n$-Category Café blog post. https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html.
  * [Shu17b] Michael Shulman, _Univalence for inverse EI diagrams_ , Homology Homotopy Appl. 19 (2017), no. 2, 219–249. MR 3723769
  * [Shu19] Michael Shulman, _All $(\infty,1)$-toposes have strict univalent universes_, 2019, arXiv:1904.07004.
  * [Str14a] Thomas Streicher, _A model of type theory in simplicial sets: a brief introduction to Voevodsky’s homotopy type theory_ , J. Appl. Log. 12 (2014), no. 1, 45–49. MR 3166196
  * [Str14b] by same author, _Semantics of Type Theory Formulated in Terms of Representability_ , 2014, Unpublished, https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/natmod.pdf.
  * [Swa18] Andrew Swan, _Separating path and identity types in presheaf models of univalent type theory_ , 2018, arXiv:1808.00920.
  * [TV05] Bertrand Toën and Gabriele Vezzosi, _Homotopical algebraic geometry. I: Topos theory_ , Adv. Math. 193 (2005), no. 2, 257–372 (English).
  * [Voe09] Vladimir Voevodsky, _Notes on type systems_ , 2009, Unpublished, https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/expressions_current.pdf.
  * [Voe17] by same author, _The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories_, Theory Appl. Categ. 32 (2017), Paper No. 4, 113–121. MR 3607210
  * [Wei22] Jonathan Weinberger, _A Synthetic Perspective on $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects_, Ph.D. thesis, Technische Universität, Darmstadt, 2022, https://doi.org/10.26083/tuprints-00020716, pp. xxi+177.
  * [WL20] Matthew Z. Weaver and Daniel R. Licata, _A constructive model of directed univalence in bicubical sets_ , Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (New York, NY, USA), LICS ’20, Association for Computing Machinery, 2020, pp. 915–928.


#  : A Mutation Testing Approach for Chatbots

Michael Ferdinando Urrico<EMAIL_ADDRESS>University of Milano-
BicoccaMilanItaly ,  Diego Clerissi<EMAIL_ADDRESS>University of
Milano-BicoccaMilanItaly and  Leonardo Mariani<EMAIL_ADDRESS>University of Milano-BicoccaMilanItaly

(2024)

###### Abstract.

Mutation testing is a technique aimed at assessing the effectiveness of test
suites by seeding artificial faults into programs. Although available for many
platforms and languages, no mutation testing tool is currently available for
conversational chatbots, which represent an increasingly popular solution to
design systems that can interact with users through a natural language
interface. Note that since conversations must be explicitly engineered by the
developers of conversational chatbots, these systems are exposed to specific
types of faults not supported by existing mutation testing tools.

In this paper, we present , a mutation testing tool for conversational
chatbots. addresses mutations at multiple levels, including conversational
flows, intents, and contexts. We designed the tool to potentially target
multiple platforms, while we implemented initial support for Google Dialogflow
chatbots. We assessed the tool with three Dialogflow chatbots and test cases
generated with Botium, revealing weaknesses in the test suites.

Chatbot Testing, Mutation Testing, Botium, Dialogflow

††journalyear: 2024††copyright: rightsretained††conference: 2024 IEEE/ACM 46th
International Conference on Software Engineering: Companion Proceedings; April
14–20, 2024; Lisbon, Portugal††booktitle: 2024 IEEE/ACM 46th International
Conference on Software Engineering: Companion Proceedings (ICSE-Companion
’24), April 14–20, 2024, Lisbon, Portugal††doi: 10.1145/3639478.3640032††isbn:
979-8-4007-0502-1/24/04††ccs: Software and its engineering Software testing
and debugging††ccs: Human-centered computing Natural language interfaces

##  1\. Introduction

The widespread adoption of conversational chatbots (e.g., 88% of people had at
least a conversation with a chatbot in 2022 (Fokina, 2023)), also known as
virtual assistants or conversational agents, in various domains (e.g.,
e-commerce, booking, tech support, healthcare, and more) (Adamopoulou and
Moussiades, 2020a; Shawar and Atwell, 2007; Grudin and Jacques, 2019) raised
the need of dedicated testing methodologies and tools (Botium, 2023; Bespoken,
2023; QBox, 2023; Ruane et al., 2018; Guichard et al., 2019; Bravo-Santos et
al., 2020; Bozic et al., 2019; Božić, 2022) to assess their effectiveness.

Mutation testing is a popular validation strategy that can be used to assess
the effectiveness of test suites and test case generation techniques (Jia and
Harman, 2010). It is a fault-based testing technique that consists of
producing many faulty versions of a software under test, called mutants, by
systematically introducing artificial faults in the software. The faults are
introduced through mutation operators, designed to change the software
according to patterns that represent possible faults. For instance, an
operator may replace the name of a variable in an expression with another one
to represent the case of a wrongly referred variable. The effectiveness of
test suites is assessed by measuring the rate of mutants that they can reveal,
that is, the percentage of mutants that fail (i.e., killed, according to the
mutation testing terminology (Jia and Harman, 2010)) when executed with the
test suite.

In order to apply mutation testing in a given context, it is necessary to
define a set of operators that can modify the relevant language elements and
entities. Conversational chatbots, differently from other software, implement
a number of components with a specific structure, even spanning multiple
diverse languages, to encode the supported conversations. For instance,
chatbots implemented with Google Dialogflow (Dialogflow, 2023) are composed of
several JSON files that specify both the sentences that a chatbot can use and
the possible flows of conversation that the chatbot can follow, text files
with alternative sentences, and webhooks to trigger external functions. This
case is the same for all the chatbot platforms (e.g., Rasa (Rasa, 2023) and
Amazon Lex (Lex, 2023)), where conversations and interactions are implemented
with specific language elements.

Currently, there is _no mutation testing tool that can properly target the
elements that implement the conversations_ , taking the semantics of the
mutated element into consideration. On the other hand, conversations need to
be carefully validated since they are the main and only interface used by
chatbots to interact with the outside world.

Figure 1. Chatbot structure meta-model adapted from Cañizares et al.
(Cañizares et al., 2022).

In this paper, we introduce , to be best of our knowledge the first mutation
testing tool for chatbots. is characterized by a general-purpose technology-
agnostic design, inspired by the meta-model proposed by Cañizares et al.
(Cañizares et al., 2022), that can be exploited to virtually address any
chatbot platforms. When a specific platform has to be addressed, the
technology-dependent interfaces, which provide the operations to locate the
items to be mutated in a given platform, have to be implemented. Our first
prototype version of the tool implements 24 mutation operators specifically
designed for chatbots and provides support to Google Dialogflow (Dialogflow,
2023), which is among the most popular chatbot platforms.

We preliminary validated our tool with three Dialogflow chatbots, applying all
the supported mutations, and observed how the test suites generated with
Botium (Botium, 2023), a state-of-the-art automated test generation framework
for chatbots, perform in detecting mutants. Results show that the test suites
were capable of killing only between 28% and 37% of the mutants, indicating
how test case generation tools for chatbots need to be improved to better
cover the space of the possible conversations.

The paper is organized as follows. Section 2 describes , its architecture and
the supported mutation operators. Section 3 presents the procedure we followed
to conduct our empirical evaluation and discusses the results. Section 4
discusses the related work. Finally, Section 5 provides final remarks.

##  2\. Approach

The mutation operators implemented in are inspired by the chatbot meta-model
originally proposed by Cañizares et al. (Cañizares et al., 2022), which
specifies general platform-agnostic chatbot concepts and features, derived by
analyzing 15 chatbot development platforms (Pérez-Soler et al., 2021a).

Figure 1 shows the meta-model. A Chatbot is represented as a class composed of
Intents (i.e., the possible goals of a user), Entities (i.e., the data types
that can be used in a conversation), Actions (i.e., the possible responses of
a chatbot), and conversational Flows (i.e., the possible user-bot interaction
flows). As chatbots are intended to be multi-language, Intents declare the
TrainingPhrases used to train the chatbot for each supported language.
TrainingPhrases can use Parameters, typed according to the supported entities.
Entities can be Simple (i.e., a literal with synonyms), Complex (i.e., a
composition of other entities and literals), or Regex (i.e., values derived
from regular expressions). In response to a user request, a chatbot performs
an Action, which can be of type Text (i.e., a plain text response), Image
(i.e., a graphical object to interact with, shown to the user), a HTTPRequest
and HTTPResponse (i.e., an action invoking an external service to respond to
the user), or Empty (i.e., no action is performed). Finally, a conversational
Flow determines the sequence of interactions between the user and the chatbot,
alternatively activating Intents and Actions. We added the notions of name,
lifespan, and parameters of the context data (i.e., the memory of the chatbot)
associated with each conversational flow to the meta-model, since these are
also important concepts that determine how conversations work in multiple
platforms.

We annotated Figure 1 to indicate the 24 operators currently supported by . We
list the name of the operator in a callout text, and we highlight the area of
the meta-model affected by the operator. We defined operators targeting all
the main entities and features that play a relevant role in a conversation.
Unlike traditional data mutation techniques, implements operators carefully
designed to manage the complexity of the target platform, to identify the
software element exactly corresponding to the conceptual element presents in
the meta-model.

The operators defined in drastically differ from traditional mutation
operators affecting statements, such as array index manipulations or decision
mutation operators. Instead, the implemented operators address the
peculiarities of conversational agents. In fact, each operator defined on the
meta-model may implement changes of different nature depending on the specific
chatbot technology. For instance, changing the flow of a conversation requires
changing the values stored in the JSON contexts objects for DialogFlow, while
they can be directly altered by changing YAML configuration files in Rasa.

The implemented operators represent faults that may originate from the
imprecise design of the conversations, such as, mistakenly swapping the name
of one parameter with another one in a response, forgetting to propagate the
context from one intent to another, or not setting a mandatory parameter as
required. We briefly present below the list of supported operators, and the
tool. For a more detailed view of the operators and the tool, please refer to
the project repository111https://gitlab.com/Michael-Urrico/defectinjector-
java.

###  2.1. Mutant Operators

We list below the mutant operators grouped by the entity that is affected by
the operators, according to Figure 1.

Chatbot:  (1) changeChatbotLanguage: replace a chatbot supported language with
another existing222To generate more realistic mutations, we defined the
semantics of replace operators like replace * with another existing * (e.g.,
changeChatbotLanguage) as replacing the value of the target property with
another existing value of the same property, rather than using a randomly
generated value (e.g., replacing the name of an intent with another existing
intent name). We plan to add the generation of random values in the future.
language,  (2) removeChatbotIntent: remove a chatbot intent,  (3)
removeChatbotEntity: remove a chatbot entity,  (4) removeChatbotFlow: remove a
chatbot flow.

Flow:  (1) changeFlowInContextName: replace a flow input context name with
another existing name,  (2) removeFlowInContextName: remove a flow input
context name,  (3) changeFlowOutContextName: replace a flow output context
name with another existing name,  (4) removeFlowOutContextName: remove a flow
output context name,  (5) changeFlowOutContextLifespan: replace a flow output
context lifespan with a random value between 1 and 3, different from the
original one,  (6) removeFlowOutContextParameter: remove a flow output context
parameter.

Intents:  (1) changeIntentName: replace an intent name with another existing
name,  (2) toggleIntentFallback: switch an intent ”fallback” flag to
true/false,  (3) removeIntentFallback: remove an intent ”fallback” flag,  (4)
changeIntentPriority: replace an intent priority with a random value between 0
and 1,000,000 (max priority value) different from the original one,  (5)
removeIntentParameter: remove an intent parameter.

Parameters:  (1) changeParameterName: replace a parameter name with another
existing name,  (2) removeParameterName: remove a parameter name,  (3)
toggleParameterIsRequired: switch a parameter ”isRequired” flag to true/false,
(4) removeParameterPrompt: remove a parameter prompt.

Inputs:  (1) changeSEntityName: replace an entity name with another existing
name,  (2) removeSEntityName: remove an entity name,  (3) changeSInputValue:
replace an input value with a random string,  (4) changeSInputSynonym: replace
an input synonym with a random string,  (5) changeTActionValue: replace a
textual action value with a random string.

Figure 2. architecture.

###  2.2. Tool

The architecture of the tool is shown in Figure 2. Its core component is a
MutationManager that is responsible of running the individual mutators
available in the tool. Each mutator is implemented as an abstract operator,
responsible of actuating the change, and an abstract finder, responsible of
finding the code element that must be changed by the operator. These abstract
components are refined for the target platform. Our prototype supports
Dialogflow chatbots. In order to find the elements to mutate, knows how to
search within the files that compose a chatbot and process them.

The tool takes in input multiple XML configuration files that specify the
target folder that hosts the code of the chatbot, the type of desired output
(a full copy of the mutated chatbot, or only a copy of the modified files),
and the set of operators that must be applied. The output consists of a set of
mutated chatbots, either including the full executable code of the bot or only
the modified files, and a report file with the list of seeded mutations.

##  3\. Empirical Evaluation

Table 1. Subject Chatbots.

Name |  Domain |  # Int./Ent./Act. |  # Tests
---|---|---|---
AppointmentScheduler (Pérez-Soler et al., 2021a)a |  Booking |  3/3/19 |  21(0)
Device (Pérez-Soler et al., 2021a)b |  Home Automation |  11/2/11 |  95(28)
Nutrition (Pérez-Soler et al., 2020; Bravo-Santos et al., 2020)c |  Food & Health |  4/7/18 |  46(1)

  * a

https://github.com/priyankavergadia/AppointmentScheduler-GoogleCalendar

  * b

https://dialogflow.cloud.google.com/ (prebuilt)

  * c

https://github.com/viber/apiai-nutrition-sample

We preliminarily evaluated by generating mutants for Dialogflow chatbots, and
assessing the effectiveness of the test cases generated with the Botium test
case generation tool (Botium, 2023), which is a white-box testing technique
developed by Botium GmbH in 2018, widely used in both industrial and academic
contexts (Bravo-Santos et al., 2020; Li et al., 2022; Pérez-Soler et al.,
2021b). Note that here a test is a conversation, with specific expectations on
the responses of the chatbot. The conversations automatically generated by
Botium cover the user-bot scenarios that could be derived from the
implementation of the chatbot under test. In the case of Dialogflow,
conversations are derived from the JSON files that encode the possible
requests and responses.

As subjects, we selected three third-party Dialogflow chatbots of different
domains and features, that have been used in previous studies (Pérez-Soler et
al., 2021a; Bravo-Santos et al., 2020; Pérez-Soler et al., 2020). Table 1
summarizes their characteristics (i.e., name, domain, and number of
intents/entities/actions), and the sizes of the test suites generated by
Botium.

For each chatbot, we first ran Botium in generation mode in order to generate
our baseline regression test suite. We then used Botium in execution mode,
repeating five times each test suite, in order to detect and discard any
spuriously failing test or flaky test case333”A flaky test is a test that both
passes and fails periodically without any code changes.” (Zheng et al., 2021),
that Botium may have generated and that could invalidate our results. We
report, between parentheses in Table 1, the number of discarded tests.

Table 2. Mutants killed over total by Botium test suites.

Chatbots | # Killed/# Equivalent/# Generated (% Killed)
---|---
Chatbot | Flows | Intents | Parameters | Inputs | Total
AppointmentScheduler | 4/0/5 (80%) | - | 4/5/12 (57%) | 0/0/3 (0%) | 0/0/7 (0%) | 8/5/27 (36%)
Device | 12/0/19 (63%) | 3/2/12 (30%) | 11/17/44 (41%) | 0/0/8 (0%) | 0/0/6 (0%) | 26/19/89 (37%)
Nutrition | 5/2/12 (50%) | - | 3/7/16 (33%) | 0/0/6 (0%) | 1/16/23 (14%) | 9/25/57 (28%)

We applied to each chatbot, generating mutants with all the operators listed
in Section 2.1, applying each mutation to every entity instance present in the
target chatbot. For instance, the removeChatbotIntent operator was applied to
every intent present in a tested chatbot, generating mutants each one with a
different intent removed. Some mutations were not applicable to all chatbots
because of missing properties to mutate (e.g., removing a context parameter
from a chatbot with no context). We finally independently deployed each mutant
on Dialogflow and tested it with the Botium test suite. Table 2 reports the
numbers and percentages of non-equivalent444An equivalent mutant is a mutant
that cannot be killed by any test case (Jia and Harman, 2010). We manually
inspected the generated mutants to establish their equivalence to the original
program, comparing the differences between the original and mutated properties
and detecting those that had no impact on the behavior of the chatbot (e.g.,
changing the priority of an intent when there are no other intents to compete
with). mutants killed by the test suites, grouped per type of mutated element.

Results show that the test suites were capable of killing only between 28% and
37% mutants in total.

Mutations affecting the chatbot structure, like intent or entity removal, as
well as those affecting intents properties, are easier to reveal (50%-80% for
Chatbot category, 33%-57% for Intents), with the exception of those targeting
the fallback mechanism, which is activated when the bot cannot understand the
message of the user. The application of toggleIntentFallback operator to an
intent may introduce tricky behaviors in chatbots, which are sometime
detected, but are not always covered by the generated test cases, as they are
mainly covering the positive scenarios. On the other hand, changing the
priority of intents mainly produces equivalent mutants, as intents are rarely
in competition in terms of which one is supposed to be activated first when a
certain user request is formulated.

Mutations targeting the Flows category are difficult to be revealed (30% in
the Device chatbot), since they require the construction of lengthy and
articulated conversations that Botium often fails to create. This group of
mutations requires further investigation on more complex chatbots, as the
conversational flows cannot be mutated if intents are self-contained. Finally,
the mutations targeting parameters and inputs remain mostly undetected (0% for
the Parameters category, and 14% at best for Inputs).

These initial results obtained with show how there is still a significant gap
to be addressed in terms of the capability of test generation tools to
exercise chatbot conversations thoroughly.

##  4\. Related Work

Conversational chatbots are increasingly exploited in various contexts (e.g.,
Web, Mobile) to support users 24/7 in a plethora of activities (e.g., booking,
home banking, etc.) (Adamopoulou and Moussiades, 2020a, b). Despite their
increasing level of adoption, the dedicated quality assurance solutions are
still limited (Li et al., 2022; Bravo-Santos et al., 2020). Indeed, they are
often restricted to individual modules (e.g., the automated speech recognition
systems (Iwama and Fukuda, 2019; Qin et al., 2019; Asyrofi et al., 2020)), or
they heavily rely on human knowledge and fixtures (Vasconcelos et al., 2017;
Bozic et al., 2019; Božić, 2022), or are limited to performance evaluation
metrics (Deriu et al., 2021; QBox, 2023; Chatbottest, 2023).

Support to test automation mainly consists of frameworks for the automation of
test execution. They include solutions to test Alexa skills (Simulator, 2023),
Rasa chatbots (Rasa, 2023), and to generically address end-to-end
conversational agents (Playwright, 2023; Bespoken, 2023). The commercial tool
Botium (Botium, 2023) represents an initial effort in the design of automated
functional testing tools for chatbots. Input mutation is further addressed in
Charm (Bravo-Santos et al., 2020), and by Guichard et al. (Guichard et al.,
2019), by building paraphrases of user queries generated by another tool
(Ruane et al., 2018). Bozic et al. face the oracle problem of chatbot testing
via metamorphic relations, involving input transformations, such as synonyms
replacements and words removal (Božić, 2022).

The lack of mutation testing solutions for conversational chatbots limits the
number of faults against which techniques can be assessed, generating
difficulties with large scale experimentation. To address this gap, this paper
proposes , a mutation testing tool specifically designed to target the
conversations implemented by chatbots.

##  5\. Conclusion

Mutation testing is an important solution to extensively validate test suites
and testing techniques, as it ensures that the software under test is
thoroughly exercised. So far, no mutation testing tool that can target the
conversations implemented by chatbots have been defined, hindering the
opportunity to systematically validate test suites against a large number of
faults.

In this paper, we presented , a mutation testing tool for chatbots. Our tool
targets Google Dialogflow chatbots and implements operators to alter the main
elements that may impact a conversation, including intents, conversational
flows, entities, and contexts. We reported an initial validation of our tool
that shows how the state-of-the-art Botium test generation technique may fail
at revealing several mutations, calling for solutions that can more thoroughly
validate conversations.

As future work, we aim at exploiting our platform-agnostic architecture to
support additional chatbot platforms, such as Amazon Lex and Rasa, and to
cover additional elements of the meta-model. Further, we plan to add more
variants of the existing operators (e.g., adding operators that mutate
properties with random values), and to finally exploit to perform large scale
fault-based assessment of the existing test case generation tools for
chatbots.

###### Acknowledgements.

This work has been partially funded by the Engineered MachinE Learning-
intensive IoT systems (EMELIOT) national research project, which has been
funded by the MUR under the PRIN 2020 program (Contract nr. 2020W3A5FY).

## References

  * (1)
  * Adamopoulou and Moussiades (2020a) Eleni Adamopoulou and Lefteris Moussiades. 2020a.  Chatbots: History, technology, and applications.  _Machine Learning with Applications_ 2 (2020), 100006.
  * Adamopoulou and Moussiades (2020b) Eleni Adamopoulou and Lefteris Moussiades. 2020b.  An overview of chatbot technology. In _IFIP International Conference on Artificial Intelligence Applications and Innovations (AIAI)_. Springer, 373–383.
  * Asyrofi et al. (2020) Muhammad Hilmi Asyrofi, Ferdian Thung, David Lo, and Lingxiao Jiang. 2020.  CrossASR: Efficient differential testing of automatic speech recognition via text-to-speech. In _Proceedings of the 2020 IEEE International Conference on Software Maintenance and Evolution (ICSME)_. IEEE, 640–650.
  * Bespoken (2023) Bespoken. 2023.  _Bespoken Documentation_.  https://read.bespoken.io/ Visited: October 2023.
  * Botium (2023) Botium. 2023.  _Botium Documentation_.  https://botium-docs.readthedocs.io/en/latest/ Visited: October 2023.
  * Božić (2022) Josip Božić. 2022.  Ontology-based metamorphic testing for chatbots.  _Software Quality Journal (SQJ)_ 30, 1 (2022), 227–251.
  * Bozic et al. (2019) Josip Bozic, Oliver A Tazl, and Franz Wotawa. 2019.  Chatbot testing using AI planning. In _Proceedings of the 2019 IEEE International Conference On Artificial Intelligence Testing (AITest)_. IEEE, 37–44.
  * Bravo-Santos et al. (2020) Sergio Bravo-Santos, Esther Guerra, and Juan de Lara. 2020.  Testing chatbots with Charm. In _Proceedings of the 13th International Conference on the Quality of Information and Communications Technology (QUATIC)_. Springer, 426–438.
  * Cañizares et al. (2022) Pablo C Cañizares, Sara Pérez-Soler, Esther Guerra, and Juan de Lara. 2022.  Automating the measurement of heterogeneous chatbot designs. In _Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing (SAC)_. ACM, 1491–1498.
  * Chatbottest (2023) Chatbottest. 2023.  _Chatbottest_.  https://chatbottest.com/ Visited: October 2023.
  * Deriu et al. (2021) Jan Deriu, Alvaro Rodrigo, Arantxa Otegi, Guillermo Echegoyen, Sophie Rosset, Eneko Agirre, and Mark Cieliebak. 2021.  Survey on evaluation methods for dialogue systems.  _Artificial Intelligence Review_ 54 (2021), 755–810.
  * Dialogflow (2023) Dialogflow. 2023.  _Dialogflow Documentation_.  https://cloud.google.com/dialogflow/docs Visited: October 2023.
  * Fokina (2023) Maryia Fokina. 2023.  _The Future of Chatbots: 80+ Chatbot Statistics for 2023_.  https://www.tidio.com/blog/chatbot-statistics/ Visited: October 2023.
  * Grudin and Jacques (2019) Jonathan Grudin and Richard Jacques. 2019.  Chatbots, humbots, and the quest for artificial general intelligence. In _Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems_. ACM, 1–11.
  * Guichard et al. (2019) Jonathan Guichard, Elayne Ruane, Ross Smith, Dan Bean, and Anthony Ventresque. 2019.  Assessing the robustness of conversational agents using paraphrases. In _Proceedings of the 2019 IEEE International Conference On Artificial Intelligence Testing (AITest)_. IEEE, 55–62.
  * Iwama and Fukuda (2019) Futoshi Iwama and Takashi Fukuda. 2019.  Automated testing of basic recognition capability for speech recognition systems. In _Proceedings of the 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)_. IEEE, 13–24.
  * Jia and Harman (2010) Yue Jia and Mark Harman. 2010.  An analysis and survey of the development of mutation testing.  _IEEE Transactions on Software Engineering (TSE)_ 37, 5 (2010), 649–678.
  * Lex (2023) Amazon Lex. 2023.  _Amazon Lex Documentation_.  https://docs.aws.amazon.com/lex/ Visited: October 2023.
  * Li et al. (2022) Xiaomin Li, Chuanqi Tao, Jerry Gao, and Hongjing Guo. 2022.  A Review of Quality Assurance Research of Dialogue Systems. In _Proceedings of the 2022 IEEE International Conference On Artificial Intelligence Testing (AITest)_. IEEE, 87–94.
  * Pérez-Soler et al. (2020) Sara Pérez-Soler, Esther Guerra, and Juan De Lara. 2020.  Model-driven chatbot development. In _Proceedings of the 39th International Conference on Conceptual Modeling (CM)_. Springer, 207–222.
  * Pérez-Soler et al. (2021a) Sara Pérez-Soler, Esther Guerra, and Juan de Lara. 2021a.  Creating and migrating chatbots with CONGA. In _2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-C)_. IEEE, 37–40.
  * Pérez-Soler et al. (2021b) Sara Pérez-Soler, Sandra Juarez-Puerta, Esther Guerra, and Juan de Lara. 2021b.  Choosing a chatbot development tool.  _IEEE Software_ 38, 4 (2021), 94–103.
  * Playwright (2023) Playwright. 2023.  _Playwright_.  https://playwright.dev/ Visited: October 2023.
  * QBox (2023) QBox. 2023.  _QBox_.  https://qbox.ai/ Visited: October 2023.
  * Qin et al. (2019) Yao Qin, Nicholas Carlini, Garrison Cottrell, Ian Goodfellow, and Colin Raffel. 2019.  Imperceptible, robust, and targeted adversarial examples for automatic speech recognition. In _Proceedings of the International Conference on Machine Learning (ICML)_. PMLR, 5231–5240.
  * Rasa (2023) Rasa. 2023.  _Rasa Documentation_.  https://rasa.com/docs/ Visited: October 2023.
  * Ruane et al. (2018) Elayne Ruane, Théo Faure, Ross Smith, Dan Bean, Julie Carson-Berndsen, and Anthony Ventresque. 2018.  Botest: A framework to test the quality of conversational agents using divergent input examples. In _Proceedings of the 23rd International Conference on Intelligent User Interfaces Companion (IUI-C)_. ACM, 1–2.
  * Shawar and Atwell (2007) Bayan Abu Shawar and Eric Atwell. 2007.  Chatbots: Are they really useful?  _Journal for Language Technology and Computational Linguistics_ 22, 1 (2007), 29–49.
  * Simulator (2023) Alexa Simulator. 2023.  _Alexa Simulator Documentation_.  https://developer.amazon.com/en-US/docs/alexa/devconsole/alexa-simulator.html Visited: October 2023.
  * Vasconcelos et al. (2017) Marisa Vasconcelos, Heloisa Candello, Claudio Pinhanez, and Thiago dos Santos. 2017.  Bottester: Testing conversational systems with simulated users. In _Proceedings of the Brazilian Symposium on Human Factors in Computing Systems_. ACM, 1–4.
  * Zheng et al. (2021) Wei Zheng, Guoliang Liu, Manqing Zhang, Xiang Chen, and Wenqiao Zhao. 2021.  Research progress of flaky tests. In _Proceedings of the IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)_. IEEE, 639–646.