Simplicial type theory extends homotopy type theory with a directed path type which internalizes
the notion of a homomorphism within a type. This concept has significant applications both within
mathematics—where it allows for synthetic (higher) category theory—and programming
languages—where it leads to a directed version of the structure identity principle. In
this work, we construct the first types in simplicial type theory with non-trivial
homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to
obtain triangulated type theory in order to construct the universe of discrete types
$\Space$. We prove that homomorphisms in this type correspond to ordinary functions of types ,
that $\Space$ is directed univalent.

The construction of $\Space$ is foundational for both of the aforementioned applications of
simplicial type theory. We are able to define several crucial examples of categories and to
recover important results from category theory. Using $\Space$, we are also able to define various
types whose usage is guaranteed to be functorial. These provide the first complete examples of
the proposed directed structure identity principle.

§ INTRODUCTION

Homotopy type theory () is a type theory for synthetic $\infty$-groupoid theory; it shapes
every type into an object equipped with a proof-relevant coherent equivalence relation which is
silently manipulated and respected by every construction in type theory. While the motivation for
this interpretation comes squarely from homotopy theory,
<cit.> have proven to be useful even for those
interested only in type theory and, especially, in proof assistants.

Proof assistants are well-tuned to support replacing equal elements by equal elements, where
equality is reified by the intensional identity type within type theory. Accordingly, if two
distinct terms can be identified, they can be swapped out for each other in large proofs without
further effort. In , the identity type becomes far richer and, in particular, elements of the
universe become identified whenever they are equivalent. Accordingly, users of proof assistants
based on  can swap out , an implementation of the integers well-suited for reasoning
with an equivalent version tuned for efficient computation without additional effort.  This offers
the same convenience to types that function extensionality grants functions.
<cit.>, for instance, show that this can be used to internalize some applications
of parametricity but, crucially, without eliminating standard models which do not support the full
apparatus of parametricity.

A type theory for groupoids makes it far easier to manipulate equality, but what about formalization
challenges which are fundamentally asymmetric? For a toy example, consider an algorithm traversing a
list to sum its elements $\Con{sum} : \prn{A : \Con{Monoid}} \to \Con{List}\,A \to A$. Univalence
and one of its important consequences, the structure identity principle, tell us that $\Con{sum}$
must respect monoid isomorphisms. But far more is true: $\Con{sum}$ commutes with all monoid
homomorphisms. To prove this we must firstReq(1) formulate how a monoid homomorphism
$f : A \to B$ induces a map $\Con{List}\,f : \Con{List}\,A \to \Con{List}\,B$ and
secondReq(2) show that $\Con{sum} \circ \Con{List}\,f = f \circ \Con{sum}$.  Neither
task follows from univalence as $f$ need not be invertible and univalence handles only symmetric

§.§ A type theory for categories

The above example would be possible in a version of type theory where types encoded not just
groupoids but categories: a directed type theory. That is, each type would come equipped with
a notion of homomorphism (along with composition, ) and each term in the type theory would be
bound to automatically respect homomorphisms , be functorial.  Aside from the benefits to
formalization, it is particularly desirable to find a directed version of  where types would
encode $\infty$[Specifically, $(\infty,1)$-categories: categories whose morphisms form an
$\infty$-groupoid.]-categories <cit.>;
$\infty$-category theory is an important area of mathematics but whose foundations are well-known to
be cumbersome. It is conjectured that directed homotopy theory could serve as the basis for a more
usable and formalizable foundation of this field. Many such theories (both homotopical and not) have
been studied over the years <cit.>.

A key obstruction to this program is that ($\infty$-)categories do not behave well enough to support
a model of type theory where every type is a category. For instance, $\Pi$-types do not always exist
because the category of categories is not locally cartesian closed. Most directed type theories
therefore change how type theory works to , allow only certain kinds of $\Pi$-types and
dependence. We will focus on a different approach introduced by <cit.>: simplicial
type theory (). The key insight is to not require that every type is an
$\infty$-category, but instead a more flexible object from which we can carve out genuine
$\infty$-categories using two definable predicates.

extends  with a new type to probe the implicit categorical structure each type
possesses: the directed interval $\Int$. <cit.> further equip it with the
structure of a bounded linear order $\prn{\land,\lor,0,1}$. One can then use $\Int$ to access , the
morphisms $a$ to $b$ in $A$ by studying ordinary functions within type theory $f : \Int \to A$ such
that $f\prn{0} = a$ and $f\prn{1} = b$.

evidence <cit.>
suggests that simplicial type theory approaches the desired usable foundations for $\infty$-category
theory. A number of definitions and theorems from classical $\infty$-category theory have been
ported to  and the proofs are shorter and more conceptual. Even better, Kudasov's
experimental proof assistant  <cit.> for  has shown that the arguments for
, the Yoneda lemma are simple enough to be formalized and machine-checked <cit.>.

For the remainder of this paper, we shall be concerned only with $\infty$-categories and
constructions upon them. Accordingly, hereafter we largely drop the “$\infty$-” prefix and speak
simply of categories, groupoids,  except in those few situations where it would cause

Simplicial type theory, a reprise
A brief description of simplicial type theory is in order.  As mentioned, every type $A$ in
has a notion of homomorphism: functions $\Int \to A$. However, in arbitrary types these do not
really behave like homomorphisms , they need not compose.

Suppose we are given $f,g : \Int \to A$ such that $f\,1 = g\,0$. A composite $h$ ought to be a
homomorphism such that $h\,0 = f\,0$ and $h\,1 = g\,1$, but not every such $h$ satisfying just these
conditions ought to be a composite. In particular, further data is required to connect $h$ with $f$
and $g$. Classically, all of this is encoded by a 2-simplex $H$ (see the left diagram in
<ref>). Inside simplicial type theory, we represent such 2-simplices as maps
$\Delta^2 \to A$ where $\Delta^2 = \Compr{\prn{i,j} : \Int \times \Int}{i \ge j}$ (c.f., <ref>).

\[
\begin{tikzpicture}[diagram]
\node (A) {$f\prn{0}$};
\node[above right = 1cm and 2cm of A] (B) {$f\prn{1}$};
\node[right = 4cm of A] (C) {$g\prn{1}$};
\node[above right = 0.35cm and 2cm of A] (D) {$H$};
\path[->] (A) edge node[above] {$f$} (B);
\path[->] (B) edge node[above] {$g$} (C);
\path[->] (A) edge node[below] {$h$} (C);
\end{tikzpicture}
\qquad
\begin{tikzpicture}[diagram]
\fill[pattern=north west lines] (0.5,0.05) -- (3.7,0.05)  -- (3.7,0.85) -- (0.5,0.05);
\node[] (A) at (0,0) {(0,0)};
\node [right = 4cm of A] (B) {(1,0)};
\node [above = 1cm of A] (C) {(0,1)};
\node [above right = 1cm and 4cm of A] (D) {(1,1)};
\path[->] (A) edge (B);
\path[->] (A) edge (C);
\path[->] (C) edge (D);
\path[->] (B) edge (D);
\path[->] (A) edge (D);
\end{tikzpicture}
\]

Illustrations of simplices

In particular, a 2-simplex $H : \Delta^2 \to A$ witnesses that $H\prn{-,0}$ and $H\prn{1,-}$ can be
composed to obtain $\lambda i.\,H\prn{i,i}$. It is convenient to isolate the subtype
$\Lambda^2_1 = \Compr{\prn{i,j}}{i = 1 \lor j = 0} \subseteq \Delta^2 \subseteq \Int \times
\Int$. Unfolding, a map $\Lambda^2_1 \to A$ corresponds to a pair of composable arrows $f,g$.
Accordingly, every pair of composable arrows in $A$ admits a unique composite , $A$ is
Segal if $\prn{\Delta^2 \to A} \Equiv \prn{\Lambda^2_1 \to A}$.

Segal types already possess enough structure to behave like categories  it follows that
composition is associative and unital just from the Segal condition. Unfortunately, they may suffer
from an excess of data: they come equipped with two notions of sameness. Namely, $a,a' : A$ may be
regarded as the same when $a = a'$ or when there is an invertible homomorphism from $a$ to
$a'$. In keeping with our pursuit of the directed structure identity, we shall be interested in
types where these coincide  where $A \to \Sum{f : A^\Int}\IsIso\prn{f}$ is an equivalence. We
say such a type is Rezk if it is Segal and satisfies this condition. An important result of
<cit.> is that Rezk types adequately model the standard notion of
$\infty$-category <cit.>.[In fact, combined with general results on
<cit.> they model internal $\infty$-categories in an
$\infty$-topos <cit.>.]

Directed univalence
However, simplicial type theory is not a panacea for replacing classical $\infty$-category
theory. Presently, it is really only suitable for studying “formal” questions and, surprisingly,
it is not possible to construct a non-trivial closed Rezk type within . Crucially,
lacks an equivalent to the category of groupoids (the $\infty$-categorical version of the
category of sets). Not only does this mean that  faces severe limitations on what theorems can
be stated, it is presently impossible to exploit directed path types when formalizing.
Returning to our original example with $\Con{sum}$,  would automatically handle
firstReq(1) and secondReq(2) if there was a type of monoids
$\Con{Monoid}$ where directed paths were monoid homomorphisms, but such a definition is presently
out of reach.

Our central contribution is to overcome these challenges by extending  with new reasoning
principles and constructing a Rezk type $\Space$ whose objects correspond to groupoids (, Rezk
types where every homomorphism is invertible) and whose homomorphisms are functions. This last
requirement is termed directed univalence:

A universe $\Space$ is directed univalent if $\Int \to \Space$ is isomorphic to
$\Sum{A\,B : \Space} A \to B$.

Before discussing our approach, we survey a few consequences of this result. Once $\Space$ is
available, a number of applications of  snap into focus. For instance, one can isolate
subcategories of $\Space$ such as the category of sets $\Space_{\le 0}$ and the category of
propositions $\Space_{\le -1}$. Using the ordinary constructions of type theory, one can parlay
these into our aforementioned category of monoids:

\[
\Con{Monoid} =
\Sum{A : \Space_{\le 0}} \Sum{\epsilon : A} \Sum{\cdot : A \times A \to A}
\Con{isAssociative}\prn{\cdot} \times \Con{isUnit}\prn{\cdot,\epsilon}
\]

The only difference in this definition from the standard one seen in ordinary type theory is the
replacement of $\Uni$ by $\Space_{\le 0}$. However, with just this change we are able to prove the
following result:
If $F,G : \Con{Monoid} \to \Space$ and $\alpha : \prn{A : \Con{Monoid}} \to F\prn{A} \to G\prn{A}$
then $\alpha$ is natural  if $f : A \to B$ is a monoid homomorphism,
$\alpha\prn{B} \circ f = f \circ \alpha\prn{A}$.

In particular, choosing $F = \Con{List}$, $G = \ArrId{}$, and $\alpha = \Con{sum}$ yields our
desired earlier example.

Replacing $\Con{Monoid}$ with $\Con{Ring}$, one could derive a similar theorem to argue that given
numerical algorithm $f : (R : \Con{Ring}) \to R^n \to R$ then the parity of its output (when applied
to $\mathbb{Z}$) depends on the parity of its inputs, as $f$ commutes with the map
$\mathbb{Z} \to \mathbb{Z}/2$. These are instances of a directed version of the structure
identity principle (SIP) <cit.>: if $C$ is a type
of algebraic structures, its homomorphisms coincide with classical morphisms of those
structures. Consequently every term and type using $C$ is therefore automatically bound to be
functorial and respect these classical morphisms. It was observed by , <cit.> that
directed SIP could be used to ease formalization efforts and we provide the first complete examples
of this and by proving directed SIP occurs for a wide class of structures.

More broadly, just as  allowed us to internalize parametricity results based on equivalence
relations,  allows us to internalize parametricity arguments based on naturality. From this,
we can also recover a classic result:
If $f : \prn{A : \Space} \to A \to A$ then $f = \lambda A\,a.\,a$.

We may summarize these results by the slogan “$\Space$ is a type which must be used
covariantly.” In particular, any type depending on $\Space$ (or types derived from it)
must be functorial in this argument.

Recreating parametricity arguments, however, is far from the only use of $\Space$. Just as we
defined $\Con{Monoid}$, we can define various categories critical for $\infty$-category theory, such
as the category of partial orders, the simplex category, the category of finite sets,  Using
these, we present the first steps towards formalizing higher algebra (one of the main
applications of $\infty$-category theory) within type theory. Higher algebra is most often
encountered by type theorists in the form of the coherence problem and, from this point of
view, using $\Space$ we are able to give definitions of infinitely coherent monoids, groups,
Fundamentally, having just $\Space$ available throws open the door to defining a wide variety of
derived categories and all the applications this entails.

§.§ Constructing S

In a certain sense, the difficulty with $\Space$ to  is not so much in its addition—we could
always postulate a type $X : \Uni$ along with terms for the Segal and Rezk axioms, declare it to be
$\Space$, and call it a day! The challenge comes in finding a complete API for $\Space$ within
that, when established, allows us to prove all expected results and completely specifies
$\Space$. This is where $\infty$-categories prove substantially more complex than $1$-categories. It
no longer suffices to specify objects and morphisms to define $\Space$, we must also specify the
higher simplices needed for coherent composition. Thus, even if we set aside the distasteful nature
of simply adding axioms to construct $\Space$, we would be left with the task of adding an
infinite number of axioms on top of , directed univalence to fully specify its
behavior. This is a famous problem of $\infty$-category theory where nearly all constructions must
be carried out indirectly through heavy machinery.

Our main theorem therefore is to construct $\Space$ internally and thereby provide a complete API
for its use. We do this by adapting the methods of <cit.> to prove one of the most
widely-used results in $\infty$-category theory, the straightening–unstraightening
equivalence <cit.>, inside of type theory. Roughly, we define
$\Space$ and prove that the type $X \to \Space$ is equivalent to the subtype of $X \to \Uni$ spanned
by amazingly covariant families. That is, a map $X \to \Space$ corresponds to a type family
over $X$ which is covariant in $X$ as well as the context , amazingly
covariant <cit.>.

We show that all the central properties of $\Space$ follow from this description. For instance, we
are able to show that $\Space$ is closed under the expected operations (limits, colimits, dependent
sums, and certain dependent products) and, most importantly, we prove the directed univalence axiom.

§.§ Extending simplicial type theory to triangulated type theory

The central challenge is giving an adequate definition of amazingly covariant families: types
$\Gamma \vdash A : X \to \Uni$ which are covariant not only in $X$, but the entire context
$\Gamma$. This second condition, however, cannot be expressed inside of simplicial type
theory. Similar situations have arisen in many contexts within
<cit.> and, as in prior work, we address this lack of expressivity by extending simplicial
type theory by a collection of modalities to capture amazing covariance.

In fact, even without amazing covariance we are led to modal simplicial type theory or indeed, modal
versions of any type theory seeking to internalize directed univalence. The reason why can be summed
up in a single word: contravariance. It is all well and good to have a type whose use is
automatically covariant, but many important operations (, $X \mapsto X \to \Bool$) are simply
not covariant, and some ( $X \mapsto X \to X$) are neither co- nor contravariant. As it stands,
$\Space$ can only be used covariantly and so we cannot express these important and natural
operations. To rectify this, we extend  with modalities which allow us to express
contravariant dependence on $\Space$ as well as invariant dependence. Both of these
modalities have central positions within synthetic category theory: the first sends a category to
its opposite and the second sends a category to its underlying groupoid of objects. While neither
operation can be realized as a function $\Uni \to \Uni$ <cit.>, both of these
operations can be included as modalities <cit.>.

Having accepted that some modalities are necessary for simplicial type theory, it is then natural to
ask what other modalities must be added in order to internally define amazing covariance and
$\Space$.  Following <cit.>, we would like to include a modality which behaves like the
right adjoint to $A \mapsto \prn{\Int \to A}$; the so-called amazing right adjoint to $\Int \to
-$. In , the intended model (cubical sets) had such a modality but in the standard model of
simplicial type theory, no such right adjoint exists. Accordingly, we could add such a modality to
simplicial type theory, but we would have no means by which to justify it. In order to address this,
we must also weaken the standard model of simplicial type theory and, with it, the assumed structure
on $\Int$. Rather than postulating a totally ordered $\Int$, we only ask that $\Int$ be a bounded
distributive lattice where $0 \neq 1$. Semantically, this corresponds to shifting from simplicial
spaces—the standard model—to the larger category of cubical[Technically, we work within
the category of Dedekind cubical spaces. See <ref>.] spaces. Within this new
category, the necessary right adjoint exists and we can justify the addition of the necessary
modality. In order to manipulate these new modalities and relaxed interval, we also axiomatize
several general facts from the cubical spaces model. All told, we work within a version of
<cit.> (to account for modalities) and with a less structured
interval $\Int$. We term the result triangulated type theory .

Within , we isolate simplicial types, those which
believe the interval to be totally ordered. Simplicial types “embed”  into  and
we are eventually interested only in these types (in fact, mostly in simplicial Rezk types).
However, the presence of non-simplicial types is crucial to allow for the constructions needed to
define $\Space$—even though $\Space$ will itself turn out to be simplicial Rezk.

Finally, we note that while  enjoys canonicity <cit.>, adding
axioms (univalence, $\Int$, ) obstructs computation and so canonicity does not hold for
. Accordingly,  is closer to “book ” <cit.> than cubical type
theory <cit.>. We leave it to future work to develop computational versions of
our new axioms and integrate existing computational accounts of univalence in

§.§ Contributions

We contribute , a modal extension of simplicial type theory, and use it to construct a
directed univalent universe of groupoids $\Space$. In so doing, we construct the first non-trivial
examples of categories within simplicial type theory. More specifically:

* We identify several general and reusable reasoning principles with which to extend .

* We prove that $\Space$ satisfies (directed) univalence, as well as the Segal and Rezk

* We construct full subcategories purely internally and isolate important subcategories
of $\Space$.

* We build numerous important classical examples of categories , presheaves, spectra,
partial orders, and other (higher) algebraic categories from $\Space$.

Finally, we crystallize a conjectured directed structure identity principle which can be
used to recover various parametricity arguments as well as automatically discharge functoriality
goals and proof obligations. We give the first complete example applications of this principle.

We have endeavored throughout this paper to provide as many proofs as space allows. This is not
only for the sake of rigor, but because a major contribution of our synthetic approach with both
and  is the comparative simplicity of the proofs. Crucially, no knowledge of
$\infty$-categories or the semantics of homotopy type theory is required by our key
arguments. Even the most complex arguments in <ref> take up only half of page and are
possible to follow to those experienced with (modal) type theory. Ideally, we would substantiate
this claim by formalizing our arguments in a proof assistant, but there is presently no suitably
general implementation of modal type theory.

For interesting and helpful discussions around the material of this work we would like to thank
Mathieu Anel,
Steve Awodey,
Fredrik Bakke,
Lars Birkedal,
Tim Campion,
Evan Cavallo,
Felix Cherubini,
Denis-Charles Cisinski,
Jonas Frey,
Rune Haugseng,
Sina Hazratpour,
André Joyal,
Dan Licata,
Louis Martini,
Hoang Kim Nguyen,
Nima Rasekh,
Emily Riehl,
Maru Sarazola,
Christian Sattler,
Michael Shulman,
Jonathan Sterling,
Thomas Streicher,
Chaitanya Leena Subramaniam,
Paula Verdugo,
Dominic Verity,
Florrie Verity,
Matthew Weaver,
and Sebastian Wolf.

Daniel Gratzer was supported in part by a Villum Investigator grant (no. 25804), Center for Basic
Research in Program Verification (CPV), from the VILLUM Foundation. Ulrik Buchholtz acknowledges the support
of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo,
Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19, during which early stages of this work have been carried out. Jonathan Weinberger is grateful to the US Army Research Office for the support of this work under MURI Grant W911NF-20-1-0082. He also acknowledges the support of CAS and and the hospitality of Bjørn Ian Dundas and Marc Bezem on the occasion of several guest visits of the HoTT-UF project.

§ A PRIMER ON SIMPLICIAL AND MODAL TYPE THEORY

Before diving into the construction of the universe of groupoids, we recall some of the
details of simplicial type theory from <cit.> and its modal extension. In both cases,
these can be understood as extensions of homotopy type theory.

Accordingly, we begin by recalling “book ” as described by the <cit.>. Briefly, we
will be extending intensional Martin-Löf type theory with a cumulative hierarchy of universes
$\Uni[0] : \Uni[1] : \dots$. We will follow  and write $a =_A b$ (or simply $a = b$) for the
identity type. Given $p : a = b$, we will write $p_* : B\prn{a} \to B\prn{b}$ for the transport
function induced by $p$ in any type family $B : A \to \Uni$. We will hereafter assume that all
universes $\Uni[i]$ satisfy Voevodsky's univalence axiom. That is, the following canonical map is an

\[
\Con{ua} : \prn{A\,B : \Uni[i]} \to \prn{A = B} \to \prn{A \Equiv B}
\]

We also recall three definitions from the HoTT book <cit.> which we shall use repeatedly:

\begin{gather*}
\IsContr,\IsProp,\IsSet : \Uni \to \Uni;
\quad \IsContr\,A = \Sum{a : A} \Prod{b : B} a = b,
\\
\IsProp\,A = \Prod{a\,b : A} \IsContr\prn{a = b},
\quad
\IsSet\,A = \Prod{a\,b : A} \IsProp\prn{a = b}
\end{gather*}

These predicates respectively isolate (1) types which behave like $\Unit$, (2) types which behave
like a proposition, and (3) types which behave like a set by satisfying the unicity of identity
proofs. Each of these induce subtypes of the universe , $\Prop = \Sum{A : \Uni} \IsProp\,A$.
More generally, these are cases $0,1,2$ of the predicate $\Con{hasHLevel} : \Nat \to \Uni \to \Prop$
which measures to what extent a type has non-trivial identity types between identity types between
identity types

§.§ Simplicial type theory and basic category theory

The basic definition of simplicial type theory is a straightforward extension of :

Core simplicial type theory  extends homotopy type theory with the following:

* A directed interval type $\Int : \HSet$

* The operations and equations shaping $\Int$ into a bounded distributive lattice

In order to simplify our discussion as well as the eventual definition of triangulated type
theory (<ref>), we present a slight variation on  compared with its normal
definition. Accordingly, we have added $\Int$ as an axiom rather than a piece of judgmental
structure as in <cit.>. This results in fewer definitional equalities than , but
requires no additional rules over homotopy type theory to specify. We leave it to future work to
incorporate all the convenience features of <cit.> alongside the extensions we present

Using the lattice structure on $\Int$, we can now specify the common simplicial shapes used to model
composition in $\infty$-category theory  $\Delta^n$:

\[
\Delta^0 \defeq \Unit
\qquad
\Delta^{n+1} \defeq
\Compr{\prn{i_1, \ldots, i_{n+1}} : \Int^{n+1}}{i_1 \ge i_2 \geq \ldots \geq i_{n+1}}
\]

One can also give general descriptions of the boundaries $\partial \Delta^n$ and the $(n,k)$-horns
$\Lambda_k^n$, for $n \geq 0$ and $0 \leq k \leq n$ <cit.>. We use these to
define categories and related structures.

Given $a,b : A$, the type of homomorphisms or arrows from $a$ to $b$ is given by

\[
\hom_A(a,b) \defeq (a \to_A b) \defeq (a \to b) \defeq \Sum{f : \Int \to A} f\,0 = a \times f\,1 = b
\]

For convenience, we suppress the forgetful map $\hom_A(a,b) \to \prn{\Int \to A}$.

We can relativize the notion of homomorphisms to dependent types:

Given $a,b : A$ and $f : \hom_A(a,b)$, for a type family $P : A \to \Uni$, a dependent
homomorphism from $x : P\,a$ and $y : P\,b$ over $f$ is given by

\[
\hom_f^P(x,y)
\defeq (x \to_f^P y)
\defeq (x \to_f y)
\defeq
\Sum{\varphi : \prn{i : \Int} \to P\prn{f\,i}}
(\prn{\Proj[2]\,{f}}_*\prn{\tilde{f}\,0} = x)
\times
(\prn{\Proj[3]\,{f}}_*\prn{\tilde{f}\,1 }= y)
\]

Note that we must transport by the identifications $\Proj[2]{f} : f\prn{0} = a$ and
$\Proj[3]{f} : f\prn{0} = b$.

We recall the following definition of pre-categories  Segal types from the introduction:

$A : \Uni$ is Segal if the canonical map
$i : (\Delta^2 \to A) \to (\Lambda_1^2 \to A)$ is an equivalence.

If $A$ is Segal and $f : a \to_A b$, $g : b \to_A c$, we write $g \circ f$ for
$\lambda t.\,\prn{i^{-1}\prn{f,g}}\,\prn{t,t}$  the long edge of the triangle obtained by
extending $\prn{f,g} : \Lambda^2_1 \to A$ to $\Delta^2 \to A$. This operation is automatically
associative and constant functions $\Int \to A$ (identity homomorphisms) are units for $\circ$.

We say an arrow $f  : a \to_A b$ in a Segal type $A$ is an isomorphism if the following type
is inhabited: $\IsIso(f) \defeq \Sum{g\,h : b \to a} (g \circ f = \ArrId{a}) \times (f \circ h = \ArrId{b})$.

Note that $\IsIso(f)$ is a proposition and we denote the induced subtype of $a \to_A b$ by
$a \cong_A b$. With the definition of isomorphism to hand, we can properly define categories
and groupoids:

If $A$ is Segal, we say $A$ is category/Rezk-complete if the following map
(defined by path induction) is an equivalence: $\IdToIso : \prn{a,b:A} \to \prn{a = b} \to \prn{a \cong b}$

A type $A$ is groupoid or a space or $\Int$-null if
$\prn{a = b} \to \prn{a \to b}$ is an equivalence.[The terminology $\Int$-null stems from
<cit.>; it is equivalent to requiring $\IsEquiv\prn{A \to \prn{\Int \to A}}$.]

A type is a groupoid if and only if it is a category where every arrow is an isomorphism.

Intuitively, a type is Rezk when it satisfies a kind of univalence condition: isomorphism is
identity. In the intended model of , they correspond to complete Segal spaces, in turn, model
$(\infty,1)$-categories semantically. Op. cit. further show that maps between Segal
types are automatically functors  they preserve composition and identities.

§.§ Multimodal type theory

As mentioned in <ref>, we must extend type theory with various modalities
in order to define $\Space$. We shall do this by “rebasing” simplicial type theory atop
<cit.>, a general framework for modal type theory. Prior to
discussing the union of these type theories, we give a brief overview of  in this section and
refer the reader to <cit.> or <cit.>. We will
give an explanation of  as it is used in this paper: in the informal pen-and-paper style that
we use type theory generally. We therefore avoid getting bogged down in the discussion of the
various ways  modifies contexts, substitutions, and other building blocks of type theory.

First,  is a framework for modal type theories: a user picks a mode theory—a 2-category
describing their modalities—and  produces a syntax for working with this collection of
modalities. For this exposition, let us fix $\Mode$ an arbitrary 2-category where we think of
objects $m,n$ as type theories connected by the 1-cells/modalities $\mu,\nu$. The 2-cells
$\alpha,\beta$ encode transformations between modalities enabling us to control , whether $\mu$
is a comonad.  includes a modal type for each $\mu$ in the mode theory and these modal types
are 2-functorial. For , we use a mode theory with only a single mode and so we restrict
our attention to modalities and 2-cells.

The basic modification  makes to the type theory is to change the form of variables in the
context. A context is no longer simply a telescope of bindings $x : A$. Instead, each declaration is
annotated by a pair of modalities $\DeclVar{x}{\mu/\nu}{A}$. The annotation $\mu/\nu$ signifies that
$x$ was constructed under the $\mu$ modality and, presently, we are working to
construct an element of the $\nu$ modality. Both halves of this annotation restrict how variables
are used to prevent terms from illegally escaping or entering modalities and, roughly, we are
allowed to use a variable when they cancel.

xμ/μA ∈Γ

[Γ, xμ/A]bxBx

Note we have presented only the relevant and simpler substitution rule allowing us to discharge an
assumption with the “denominator” of an annotation is the identity. There is no alteration the
actual definition of substitution from ordinary capture-avoiding substitution in type theory.

In a declaration $\DeclVar{x}{\mu/\nu}{A}$ we shall often omit $\mu$ or $\nu$ if they are the
identity , $\DeclVar{x}{\mu}{A}$ or $y : B$ rather than $\DeclVar{x}{\mu/\ArrId{}}$ or

These annotations are also used to introduce the modal types associated with each $\mu$.
For instance, suppose we have a modality $\mu$ and we intend to form the modal type
$\Modify[\mu]{A}$. This is well-formed in context $\Gamma$ just when $A$ is well-formed in the
context $\Gamma/\mu$ , the context formed by replacing each declaration
$\DeclVar{x}{\xi/\nu}{A}$ in $\Gamma$ with a new declaration
$\DeclVar{x}{\xi/\nu\circ\mu}{A}$. Similarly, we can form an element of the modal type
$\MkMod[\mu]{a} : \Modify[\mu]{A}$ in context $\Gamma$ just when $a : A$ in the context

The elimination rule for $\Modify[\mu]{-}$ papers over the difference between
$\DeclVar{a}{\nu\circ\mu/\ArrId{}}{A}$ and

[Γ, xν/[μ]A]Ba

[Γ, xν∘μ/A]bxB[μ]x/a

Already, these rules are sufficient to prove the following facts that we shall use ubiquitously:

If $\IsTy[\Gamma/\nu\circ\mu]{A}$ then
$\Modify[\nu]{\Modify[\mu]{A}} \Equiv \Modify[\nu\circ\mu]{A}$ and if $\IsTy{B}$ then
$\Modify[\ArrId{}]{B} \Equiv B$.

It remains to discuss how 2-cells $\Mor[\alpha]{\mu}{\nu}$ integrate into . Roughly, each
$\alpha$ introduces a function $\Modify[\mu]{-} \to \Modify[\nu]{-}$. In order to make this
well-formed,  includes an operator $-^{\alpha}$ acting on both types and terms (formally
realized as a special substitution):

This operator is really a substitution and so it commutes past all connectives to accumulate at
variables—akin to weakening in systems designed with De Bruijn indices.[Just as
substitutions must account capture, $-^\alpha$ must account for the addition of $\Gamma/\mu$ so
that  $\MkMod[\mu]{a}^\alpha = \MkMod[\mu]{a^{\alpha\Whisker\mu}}$.] As a result, variables
are often written $x^\alpha$, signifying that they have been “shifted” from a $/\mu$-annotation to
a $/\nu$-annotation.

If $\Mor[\alpha]{\mu}{\nu}$ and $\IsTy[\Gamma/\mu]{A}$ then there is a map
$\Coe^\alpha : \Modify[\mu]{A} \to \Modify[\nu]{A^\alpha}$.

In the formal definition of , one takes $\Gamma/\mu$ as a new primitive form of context
$\LockCx{\Gamma}$ and annotates variables only with the $\mu$ of $\mu/\nu$; the denominator is
encoded by composing all the $\brc{\nu_i}$ that follow the occurrence of a variable in
$\Gamma$. This distinction is largely unimportant for using  though it
influences how we structure one of the axioms of  in <ref>.

We shall also have occasion to use the convenience feature of modalized dependent products
$\prn{\DeclVar{a}{\mu}{A}} \to B\prn{a}$ which abstract over $\DeclVar{a}{\mu}{A}$ directly rather
than $\DeclVar{a}{\ArrId{}}{\Modify{A}}$ to allow us to avoid immediately pattern-matching on $a$.
In particular, $\prn{\DeclVar{a}{\mu}{A}} \to B\prn{a}$ is equivalent to
$\prn{\DeclVar{a}{\ArrId{}}{\Modify{A}}} \to \prn{\LetMod{a}[a_0]{B\prn{a_0}}}$.

§ TRIANGULATED TYPE THEORY

Our goal is to combine multimodal and simplicial type theory in order to follow <cit.>
and build a directed univalent universe of groupoids. As mentioned in the introduction, however, the
crucial modality (the amazing right adjoint to $\Int \to -$) simply does not exist in the standard
model of simplicial type theory. Thus, while we could perfectly well combine these two systems, the
resulting combination of reasoning principles could not be justified.

In order to explain our eventual solution and crystallize the problem, it is helpful to recall the
intended semantics of simplicial type theory: simplicial spaces. Up to the complexity needed to
model homotopy type theory, these are simplicial sets , presheaves on $\SIMP$, the category of
finite, inhabited total linear orders. Already within this category, we can observe the problem: the
interval is realized by $\Yo{\brk{1}}$, the presheaf representing the total order $0 \le 1$, and
exponentiation by $\Yo{\brk{1}}$ does not have a right adjoint.[This is easiest to check by
observing that it does not commute with pushouts.] However, there is a closely related category to
$\SIMP$ which has also received a great deal of attention by type theorists interested in cubical
type theory: the category of (Dedekind) cubes $\CUBE$ or the full subcategory of partial orders
spanned by $\brc{0 \le 1}^n$ for all $n$.

Crucially, $\CUBE$ enjoys two properties which make it interesting for simplicial type theorists:
there is a fully faithful functor $\PSH{\SIMP} \to \PSH{\CUBE}$ which preserves the interval and
admits both left and right adjoints <cit.> and within
$\PSH{\CUBE}$ exponentiating by the interval is a left adjoint.

Accordingly, we introduce a relaxation of simplicial type theory intended to capture (the
homotopical version of) $\PSH{\CUBE}$. Within this type theory, we can recover simplicial type
theory by studying those types which are in the image of the aforementioned embedding alongside the
amazing right adjoint necessary for constructing our sought-after universe <cit.>.

Concretely, we work within a version of  instantiated with several modalities, further
extended by a bounded distributive lattice $\Int : \HSet$ which serves as our weakened version of
the interval, and a handful of axioms. In particular, we no longer assume that $\Int$ is totally
ordered, this is our central deviation from simplicial type theory.

§.§ The definition of triangulated type theory

We now define triangulated type theory, beginning with the underlying instance of

§.§.§ The mode theory

As mentioned in <ref>,  must be instantiated by a mode theory. In our case, we
shall require only one mode $m$ which we shall think of as cubical spaces $\PSH[\SSET]{\CUBE}$. We
shall then add the following modalities

* A pair of modalities $\GM,\SM$ internalizing the global sections comonad and its right adjoint.

* A pair of modalities $\PM,\AM$ internalizing the path space ($\Yo{0 \le 1} \to -$) and its
right adjoint.

* A modality $\OM$ internalizing the “opposite.”

Intuitively, $\Modify[\GM]{-}$ deletes all (higher) homomorphisms from a type, leaving only the
underlying type of objects (its groupoid core). This modality recovers only the discrete categories
and so it is often referred to as the discrete modality <cit.>. On
the other hand, $\Modify[\SM]{-}$ deletes all homomorphisms, but then adds in a unique (higher)
homomorphism between every pair of objects. We shall eventually force $\Modify[\PM]{-}$ to behave
like $\Int \to -$ and accordingly $\Modify[\AM]{-}$ is the amazing right adjoint to this
operation. Finally, $\Modify[\OM]{-}$ reverses all (higher) homomorphisms in a type.

We require a number of equations and natural transformations to force these modalities to behave as
expected. In particular, we require the following 2-cells and equations on modalities:

∘= ∘= ∘= ∘= ∘= ∘=

ϵ_ : ∘→
η_ :  →∘ϵ_ : ∘→
η_ :  →∘

Finally, we impose equations on these 2-cells to ensure that (1)
$\prn{\GM,\SM,\epsilon_{\GM \Adjoint \SM},\eta_{\GM \Adjoint \SM}}$
$\prn{\PM,\AM,\epsilon_{\PM \Adjoint \AM},\eta_{\PM \Adjoint \AM}}$ form adjunctions, and (2) the
(co)join of the (co)monad induced by $\GM \Adjoint \SM$ is the identity.

We will frequently omit the subscripts on the four generating 2-cells. We will often entirely
suppress $\epsilon_{\GM \Adjoint \SM} : \GM \to \ArrId{}$ as this causes no ambiguity.

§.§.§ The interval

As mentioned previously, we require an interval in order to capture the simplicial (or, in our case,
cubical) structure. In order to marry this interval with the amazing right adjoint modality
$\AM$, we do this by adding an axiom along with a new rule to :

[The interval]

There exists a bounded distributive lattice $\prn{\Int : \HSet,\land,\lor,0,1}$.

[Relating $\PM$ and $\Int$]

We extend  with the following rule:

\[
\inferrule{
\IsCx{\Gamma}
\EqCx{\Gamma/\PM}{\Gamma, i : \Int}
\]

<ref> is a more substantive change than merely adding a constant to type
theory as it imposes a genuinely new definitional equality on contexts. It is, however, less
invasive than it may appear at first glance. Recall that in the formal definition of ,
$\Gamma/\PM$ is realized not as an admissible operation on contexts but a genuinely new context
former $\LockCx{\Gamma}[\PM]$ and variables are encoded in a locally-nameless style. Therefore, both
the mysterious appearance of $i$ and the appearance of an admissible operation in a definitional
equality is merely an artifact of presenting a rule of our formal system with the more informal
notation adopted throughout this paper.  We note that while this definitional equality is very
convenient to work with, it can be replaced with weaker typal equalities constraining
$\Modify[\PM]{-}$ directly. We use <ref> only to obtain the following pair
of results:

If $\IsTy[\Gamma/\PM]{A}$ and $\IsTm{i}{\Int}$, there is a substitution
$\Gamma \to \Gamma/\PM$ inducing a type $\IsTy{A \cdot i}$.

There is an isomorphism between $\Modify[\PM]{A}$ and $\prn{i : \Int} \to A \cdot i$.

Our next axiom controls the behavior of the opposite modality on $\Int$:
[Opposite of $\Int$]

There is an equivalence $\neg : \Modify[\OM]{\Int} \to \Int$ which swaps $0$ for $1$ and $\lor$ for $\land$.

§.§.§ The simplicial monad

Before moving on to the list of additional axioms that form , we must take a moment to discuss
an additional construct: the simplicial monad. As motivation, while we have already noted that the
interval is not totally ordered, there is a large number of types which “act as though it
is.” The simplicial monad isolates and classifies these types.

More precisely, a type is simplicial if it satisfies the following predicate:

\[
\IsSimp\prn{A} =
\prn{i\,j : \Int} \to
\IsEquiv\prn{\lambda a\,z.\,a : A \to \prn{i \le j \lor j \le i \to A}}
\]

If a type $A$ satisfies $\IsSimp$, this acts as a license to totally order elements of the interval
whenever we are constructing an element of $A$. Furthermore, as the name suggests, simplicial types
are those which come from simplicial rather than cubical sets (see <ref>).

There is an idempotent lex monad $\prn{\Simp : \Uni \to \Uni,\eta,\mu}$ such that:

* For every $A : \Uni$, $\IsSimp\prn{\Simp A}$ holds.

* If $B$ is simplicial, then $\eta^* : \prn{\Simp A \to B} \to \prn{A \to B}$ is an

* $\Simp$ commutes with dependent sums and the identity type.

We refer to $\Simp$ as the simplicial monad[The notation $\Simp$ is chosen
deliberately: simplicial types are those which believe the square $\Int \times \Int$ (along with
all hypercubes) comes from gluing together a pair of triangles
$\Delta^2 \Pushout{\Int} \Delta^2$.] and write $\Uni[\Simp]$ for the subtype
$\Sum{A : \Uni} \IsSimp\prn{A}$.

We reserve the words “category” and “groupoid” for types which are simplicial in addition to
satisfying the Segal/Rezk conditions from . Accordingly,  category signifies a
type which is simplicial, Segal, and Rezk complete.

§.§.§ Additional axioms

Finally, we require a handful of additional axioms which either improve the behavior of modalities
generally or form a more tight correspondence between our system and our intended model. We offer
some intuition for each axiom and note that each is validated by the intended model described in

Our first axiom is the famous univalence axiom giving us access to homotopy type
theory <cit.>:

We assume that each universe $\Uni[i]$ is univalent.

Next, we require that modalities commute with identity types:
[Crisp induction]

For every $\mu$, the canonical map $\MkMod{a} = \MkMod{b} \to \Modify{a = b}$ is an

After these fairly general reasoning principles, we now have a sequence of more
simplicial-specific axioms. The first of these links the global sections modality to the
interval. In particular, it states that the global sections of a type always form a groupoid.
[$\Int$ detects discreteness]

If $\DeclVar{A}{\GM}{\Uni}$ then $\Modify[\GM]{A} \to A$ is an equivalence ($A$ is
discrete) if and only if $A \to \prn{\Int \to A}$ is an equivalence ($A$ is $\Int$-null).

The next axiom states that the global points of $\Int$ itself are just $0$ and $1$ and that $0 \neq 1$:
[Global points of $\Int$]

The canonical map $\Bool \to \Int$ is injective and $\Bool \Equiv \Modify[\GM]{\Int}$.

In our intended model, various properties can be proven by “testing” them at the representable
presheaves $\Yo{\brc{0 \le 1}^n}$. We include a version of this idea as an axiom in our
theory. Namely, we assert that maps between global types can be tested for invertibility at
[Cubes separate]

A map $\DeclVar{f}{\GM}{A \to B}$ is an equivalence if and only if the following holds:

\[
\prn{\DeclVar{n}{\GM}{\Nat}} \to \IsEquiv\prn{f_* : \Modify[\GM]{\Int^n \to A} \to \Modify[\GM]{\Int^n \to B}}
\]

This follows from another possible axiom, cubes detect continuity,
following <cit.>. Note that if $A$ and $B$ are simplicial, one can derive a version of
<ref> which replaces $\Int^n$ with $\Delta^n$.

It is relatively easy to characterize maps out of $\Simp A$ as they are closely related to maps out
of $A$ itself. It is much harder, however, to characterize $X \to \Simp A$. Our next axiom states
that in certain favorable cases these, too, coincide with the corresponding situation for $A$:
[Simplicial stability]

If $\DeclVar{A}{\GM}{\Uni}$ then the following map is an equivalence for all $\DeclVar{n}{\GM}{\Nat}$:

\[
\eta_* : \Modify[\GM]{\Delta^n \to A} \to \Modify[\GM]{\Delta^n \to \Simp A}
\]

Finally, while simplicial type theory allows us to prove many interesting facts about maps out of
the interval, it is far more difficult to prove properties about $X \to \Int$. In order to balance
the scales, we follow <cit.> and add an axiom characterizing these maps in certain
special cases. Prior to stating this principle, we require the following definition:

A map $\Int \to A$ of bounded distributive lattices is a finitely presented (fp)
$\Int$-algebra if it is merely equivalent to the canonical map
$\Int \to \Int\brk{x_1, \dots, x_n}/\gl{t_1 = s_1, \dots, t_m = s_m}$ for some $n,m$.

The definition of a homomorphism of bounded distributive lattices (a map which commutes with
$0,1,\land,\lor$) extends to a notion of homomorphism between fp $\Int$-algebras $\Hom[\Int]{A}{B}$
by further requiring the underlying map to commute with the maps $\Int \to A$ and $\Int \to B$.

Given an fp $\Int$-algebra $f : \Int \to A$ the following map is an equivalence:

\[
\lambda a\,f.\,f\prn{a} : A \to \prn{{\Hom[\Int]{A}{\Int}} \to \Int}
\]

Triangulated type theory  is  with mode $\Mode$ extended by

§.§ Duality and Delta{n}

<ref> has a number of remarkable consequences for $\Int$. While these are not specific to
directed univalent universes, they allow us to construct the first non-trivial categories inside

Evaluation at $0,1$ is an embedding $\prn{\Int \to \Int} \to \Int \times \Int$ with image

We first will argue via <ref> that $\Int\brk{x}$ is equivalent to $\Int \to \Int$ via the
evaluation map. To see this, let us note that $\Int \to \Int\brk{x}$ is an $\Int$-algebra by
definition, and $\Hom[\Int]{\Int\brk{x}}{\Int} \Equiv \Int$. Accordingly, by <ref>, the
map $\Con{eval} : \Int\brk{x} \to \prn{\Int \to \Int}$ is an equivalence.

By the 2-for-3 principle of equivalences, it then suffices to show that evaluating a polynomial at
$0$ and $1$ induces an embedding $\Int\brk{x} \to \Int \times \Int$ whose image is $\Delta^2$. An
inductive argument allows us to conclude that $\Con{eval}\prn{p,-}$ is a monotone map from
$\Int \to \Int$ and so evaluation of polynomials at endpoints factors through $\Delta^2$. We
therefore are reduced to showing that this map is an equivalence.  To see this, we observe that
any polynomial in one variable can be placed in the following normal form:
$p = \Con{eval}\prn{p,0} \lor x \land \Con{eval}\prn{p,1}$ whereby the conclusion is immediate.

In light of the equivalence used in the proof of Phoa's principle, we will no longer distinguish
between polynomials in one variable $\Int\brk{x}$ and functions $\Int \to \Int$.

* The evaluation map from $\Int^n \to \Int$ to monotone maps $\Bool^n \to \Int$ is an

* The evaluation map from $\Delta^n \to \Int$ to monotone maps $\brk{0 \le \dots \le n} \to \Int$ is an

In the above, we have regarded $\Bool$ as a 2-element partial order $\False \le \True$.

Both claims follow from induction on $n$ and repeated application of Phoa's principle.

Our cube category is equivalent by Birkhoff duality to the category of flat finite bounded
distributive lattices <cit.>.  <ref> is in some sense a
manifestation of this fact.

$\Int$ is simplicial.

To show that $\Int \to \prn{\prn{i\le j\lor j\le i} \to \Int}$ is an equivalence,
it suffices, by <ref>,
to consider $\DeclVar{f,g}{\GM}{\Int^n \to \Int}$ and show that the following is an equivalence:

\[
\Modify[\GM]{\Int^n \to \Int} \to
\Modify[\GM]{
\Compr{\vec x:\Int^n}{f(\vec x) \le g(\vec x) \lor g(\vec x) \le f(\vec x)} \to \Int
\]

Using <ref>, we can extend an element of the codomain to a total function
$\Int^n \to \Int$ provided we can specify its behavior on $\vec x : \Bool^n$. The
proposition $f(\vec x)\le g(\vec x) \lor g(\vec x)\le f(\vec x)$ holds for all $\vec x : \Bool^n$
using <ref> and so such an extension always exists and is necessarily unique.

$\Delta^n$ is a category.

Since there are no invertible morphisms in $\Delta^n$, it is trivially Rezk-complete and, as a
retract of $\Int^n$, it is simplicial. Therefore, it suffices to show that $\Delta^n$ is Segal.

To this end, let us consider $\Lambda^2_1 \to \Delta^n$. This is equivalent to a pair of maps
$f,g : \Int \to \Delta^n$ such that $f\prn{1} = g\prn{0}$. Next, by the Phoa principle
$f,g : \Int \to \Delta^n \to \Int^n$ are fully determined by $n$-tuples of pairs ,
$\prn{\Proj[k]\prn{f\prn{0}} \le \Proj[k]\prn{f\prn{1}}}_{k \le n}$. In total then, we are given
$n$-many 3-tuples:

\[
\prn{\Proj[k]\prn{f\prn{0}} \le \Proj[k]\prn{f\prn{1}} = \Proj[k]\prn{g\prn{0}} \le \Proj[k]\prn{g\prn{1}}}_{k \le n}
\]

By <ref>, these are 2-simplices in $\Delta^n$ and so
every horn has a unique extension as required.

We note that <ref> is already a significant step forward for : it
is the first result constructing an explicit example of a non-discrete category within the system.

§.§ Reasoning with modalities in Triangulated Type Theory

A number of useful results in  are immediate corollaries of standard results from
combined with one of the axioms. We record some of the most important results in this section for
future use and to give a flavor for how modalities can be used to enhance simplicial reasoning.

By general results about adjoint modalities from  <cit.>, we obtain
the following:

* If $\DeclVar{A}{\ArrId{}}{\Uni}$, $\DeclVar{B}{\AM}{\Uni}$ there is an equivalence
$\Modify[\AM]{\prn{\prn{i : \Int} \to A^\eta \cdot i} \to B} \Equiv \prn{A \to
\Modify[\AM]{B}}$.

* If $\DeclVar{A}{\ArrId{}}{\Uni}$, $\DeclVar{B}{\OM}{\Uni}$ there is an equivalence
$\Modify[\OM]{\Modify[\OM]{A} \to B} \Equiv \prn{A \to \Modify[\OM]{B}}$.

* If $\DeclVar{A}{\ArrId{}}{\Uni}$, $\DeclVar{B}{\SM}{\Uni}$ there is an equivalence
$\Modify[\SM]{\Modify[\GM]{A^\eta} \to B} \Equiv \prn{A \to \Modify[\SM]{B}}$.

There are also a dependent versions where ,

This result is, in some sense, the entire purpose of : it is the rule that allows transposing
across the adjunction $\prn{\Int \to -} \Adjoint \Modify[\AM]{-}$. This rule, in turn, is the key
ingredient required to carry out the construction of $\Space$ following <cit.>.

We record two useful consequences of the transposition principle for $\OM \Adjoint \OM$ and $\SM \Adjoint \GM$:

$\Modify[\OM]{-}$ commutes with colimits.

Evaluation at endpoints $\prn{\Int \to \Modify[\SM]{A}} \to \prn{\Bool \to \Modify[\SM]{A}}$ is an

To give an example of how these reasoning principles can be used, we show how they can be used to
enhance our stock of simplicial types.

Given $\DeclVar{A}{\OM}{\Uni}$ if $\Modify[\OM]{\IsSimp\prn{A}}$ then $\IsSimp\prn{\Modify[\OM]{A}}$.

Fix $i,j : \Int$ such that we must show
$\Modify[\OM]{A} \to \prn{i \le j \lor j \le i \to \Modify[\OM]{A}}$ is an equivalence. Using
<ref>, the codomain is equivalent to $\Modify[\OM]{\Modify[\OM]{i \le j \lor j \le i} \to A}$.
By <ref>, $\Modify[\OM]{i \le j \lor j \le i}$ is
$\neg \MkMod[o]{i} \ge \neg \MkMod[o]{j} \lor \neg \MkMod[o]{j} \ge \neg \MkMod[o]{i}$ and the
conclusion follows immediately from our assumption $\Modify[\OM]{\IsSimp\prn{A}}$.

If $\DeclVar{A}{\GM}{\Uni}$ is discrete then $A$ is simplicial.

Assume $A$ is discrete, , $A \to A^\Int$ is an equivalence.  Since cubes
separate by <ref>, it suffices to show for all polynomials
$p,q : \Int\brk{\vec x}$ in $n$ variables $\vec x$ that the map $A \to (\varphi(\vec x) \to A)$ is
an equivalence, where $\varphi(\vec x) := p(\vec x)\le q(\vec x) \lor q(\vec x)\le p(\vec x)$.

In turn, it suffices to give an $\Int$-homotopy $h$ connecting the constant map at $0$ to the
identity on $\varphi(\vec x)$, for each $\vec x:\Int^n$. We notice that the straight-line homotopy
$h(\vec x,t) = \vec x\land t$ from $0$ to $\vec x$ works: We have to show for each $\vec x$ with
$\varphi(\vec x)$ that $\varphi(\vec x\land t)$ holds, for each $t$.  But notice that $\varphi(0)$
is true, as any pair of constants among $0,1$ are comparable.  By <ref>,
$\varphi(\vec x\land t)$ then holds for all $t$.

Using the adjunction $\GM \Adjoint \SM$, we can prove that ,
$\Nat \Equiv \Modify[\GM]{\Nat}$ <cit.>. Accordingly, by <ref>:

$\Nat$ and $\Bool$ are both simplicial and $\Int$-null  groupoids.

The result analogous to <Ref> for Rezk-complete Segal types does not hold, falsifying a conjecture of
<cit.>. In particular, $\Delta^2 \Pushout{\Int} \Delta^2$ can be shown to be
Rezk-complete and Segal, but is not simplicial. This same example shows that the requirement that
$A$ be annotated with $\GM$ is necessary: as a family over $\Int \times \Int$ the type
$\Delta^2 \Pushout{\Int} \Delta^2$ is fiberwise a proposition—explicitly, it is
$\lambda i\,j.\,i \le j \lor j \le i$—and therefore it is fiberwise $\Int$-null. If we could
apply <ref> without the $\GM$-annotation we could conclude that
each fiber $i \le j \lor j \le i$ was simplicial. Combined with the fact that $\Int \times \Int$
is simplicial, this leads again to the false conclusion that $\Delta^2 \Pushout{\Int} \Delta^2$ is

§.§ The cubical spaces model

is intended to be an internal language for cubical spaces  $\PSH{\CUBE}$ (or rather its $\infty$-categorical
engagement). In order to make this precise, we construct a model of  inside a
model category which presents the relevant $\infty$-category in order to link type theory (a
1-categorical object) with an
$\infty$-category <cit.>. For , this model
category is the injective model structure on simplicial presheaves $\PSH[\SSET]{\CUBE}$. That
is, types in  are interpreted as certain families of presheaves over $\CUBE$ valued in
$\SSET = \PSH{\CUBE}$. It is helpful to view the simplicial sets layer as “mixing in” homotopy
theory with ordinary presheaves over $\CUBE$. This result largely follows from combining
off-the-shelf results about models of  and models of . First, we require the following

Homotopy type theory has a model in $\PSH[\SSET]{\CUBE}$ where types are interpreted as injective

We use the model theory of  <cit.> to
extend this model to :

with mode theory $\Mode$ has a model in $\PSH[\SSET]{\CUBE}$ where

* $\GM \Adjoint \SM$ is interpreted by the global sections and codiscrete functors on this

* $\OM$ is interpreted by precomposition with the involution $\CUBE \to \CUBE$.

* $\PM \Adjoint \AM$ is interpreted by the adjunction $\prn{-}^\Int \Adjoint \prn{-}_\Int$.

In order to apply these off-the-shelf results we must show that all the functors interpreting
modalities appropriately preserve types  are right Quillen. This is true for all but the global
sections functor, which is not right Quillen for the injective model structure. Fortunately, it is
right Quillen for the projective model structure, and an unpublished argument due to Shulman
shows that this, combined with his cobar construction <cit.>, suffices to
interpret even this problematic modality. We omit the details of these computations for reasons of

Finally, we must show that this model of  validates the axioms necessary for . Each
verification is a routine computation, with many following immediately from the corresponding fact
about ordinary presheaves $\PSH{\CUBE}$. The only exception to this is <ref>, which is
follows from its proof for ordinary presheaves by <cit.>. All told, we conclude
the following:

has a model in $\PSH[\SSET]{\CUBE}$ where types are injective fibrations and modalities are
interpreted as described above.

Crucially, within this model simplicial types are precisely those belonging to the subtopos
$\PSH[\SSET]{\SIMP}$. Consequently, the adequacy result from <cit.> applies and we
conclude that this model shows that any fact proven about categories and groupoids inside of
is a valid proof for the standard definition of $\infty$-categories.

Categories in  adequately model $\infty$-categories.

§ COVARIANT AND AMAZINGLY COVARIANT FAMILIES

In <ref>, we saw how groupoids were defined internally as those types satisfying
$\Con{isGroupoid}\,A = \IsEquiv\prn{A \to A^\Int}$ was an equivalence. We might hope this induces a
directed univalent universe of groupoids directly, by considering
$\Uni_{\Con{grp}} = \Sum{A : \Uni} \Con{isGroupoid}\,A$. However, this is far from our desired
universe. Most glaringly, while $F : A \to \Uni_{\Con{grp}}$ is a family of groupoids over $A$, this
family is not required to respect the category structure of $A$ in any way. In fact, one may show
that a map $F : \Int \to \Uni_{\Con{grp}}$ is akin to an unstructured relation between $F\prn{0}$
and $F\prn{1}$ and nothing like the function required for directed univalence. In order to rectify
this and define $\Space$, we shall require a theory of families of groupoids where a morphism
$f : a \to a'$ in $A$ induces a functor of groupoids $F\prn{a} \to F\prn{a'}$. <cit.>
termed these covariant families and they are further studied by <cit.>. As
mentioned in the introduction, we shall also require a modal version of covariant families
$F : A \to \Uni$ which are covariant not only in $A$ but also in the entire context.

§.§ Covariant families and transport

We begin by recalling the definition of a covariant family from <cit.>.

A family $A : X \to \Uni$ is covariant if the following proposition holds:

\[
\IsCovFam\prn{F} =
\Prod{x : \Int \to X}
\Prod{a_0 : A\prn{x\,0}}
\IsContr\prn{
\Sum{a_1 : A\prn{x\,1}} \prn{a_0 \to_x a_1}
\]

While not strictly necessary, we will assume that the base of a covariant family $A$ is a Segal
type unless explicitly noted otherwise.

Given a type family $A : X \to \Uni$, we shall write $\tilde{A}$ for the total type
$\Sum{x : X} A\prn{x}$.

Given $\phi : \IsCovFam\prn{A : X \to \Uni}$ and $f : x_0 \to x_1$ then there is an induced
transport map $A\prn{f} : A\prn{x_0} \to A\prn{x_1}$. Moreover, transport maps respect composition
and identities.

Roughly, one defines $A\prn{f}\prn{a_0} = \Proj[1]{\Proj[1]\prn{\phi\,f\,a_0}}$. We leave it to
the reader to check that this has the appropriate type and that the expected identities are

It is often helpful to rephrase covariant families in terms of orthogonality conditions:

A family $A : X \to \Uni$ is covariant if and only if the projection map $\tilde{A} \to X$ is
right orthogonal to $\EmbMor{\brc{0}}{\Int}$ , if
$\prn{\tilde{A}}^\Int \to \prn{\tilde{A}}^{\brc{0}} \times_{X^{\brc{0}}} X^\Int$ is an

To cultivate intuition for this definition, we recall another result from <cit.>.

Given $\phi : \IsCovFam\prn{A : X \to \Uni}$ and $x : X$, the fiber $A\prn{x}$ is a groupoid.

§.§ Amazing covariance

We now refine our search from a universe of groupoids to a universe of covariant fibrations.
That is, we wish to define some universe $\Space$ such that a map $A \to \Space$ corresponds (in
some sense) to a covariant fibration over $A$. Let us leave this correspondence imprecise for now
and consider the behavior $\Space$.

In light of <ref>, the points of $\Space$ will be
covariant over $\ObjTerm{}$  groupoids. However, elements $f : \Int \to \Space$ will
become richer: they are covariant fibrations $B \to \Int$ therefore consist not only of a pair of
groupoids $B_0,B_1$ over $0$ and $1$, but also include a transport function $B_0 \to B_1$
(<ref>). Phrased differently, a homomorphism $F : \Int \to \Space$
contains an ordinary function $F\prn{0} \to F\prn{1}$.

Clearly this is a step towards directed univalence over $\Sum{A : \Uni} \Con{isGroupoid}\,A$, but it
is far from obvious how to define such a type $\Space$. In particular, while we have sketched how
behavior ought to differ between elements of $\Space$ compared with functions $\Int \to \Space$ and
so on, we cannot really cleanly divide elements of $\Space$ from functions into $\Space$ within type
theory! An element of $\Space$ is formed in a context $\Gamma$ and if that contexts contains a
variable $i : \Int$, then this is the same as a function $\Int \to \Space$.

There is an even more straightforward way to see why this causes a problem. Suppose we attempt to
define another subtype of $\Uni$ to isolate this universe of covariant fibrations
$\Sum{A : \Uni} \Con{isCov}\prn{A}$. A cursory inspection reveals this to be nonsense: being
covariant is not a property of $A$, it is a property of a family of types $A : X \to \Uni$. So in
this `definition', what exactly is $A$ covariant over?

It is here that modalities are vital: $A$ should be covariant with respect to the entire ambient
context. This is not something that can be expressed in standard type theory, but with the amazing
right adjoint to $\Int \to -$ we are able to define such a subtype.

Types covariant over $\Gamma$
We define a predicate on types $\IsACov : \Uni \to \Prop$ which encodes whether a type is covariant
over the entire context following <cit.>. We note that this predicate is a refinement of
<cit.> which capitalizes on the existence of the amazing right adjoint as a proper
modality. The construction of this predicate proceeds in three steps:

* We begin by observing that, when specialized, $\IsCovFam$ has the type
$\prn{\Int \to \Uni} \to \Prop$.

* As this is a closed term, we may apply <ref> to obtain a function
$\Uni \to \Modify[\AM]{\Prop}$.

* Finally, we postcompose with the dependent $\AM$ modality which sends
$\Modify[\AM]{\Prop} \to \Prop$.

All told, we obtain a predicate $\Uni \to \Prop$ which encodes whether a given type is covariant
over the entire context. Unfolding, this predicate sends $A$ to
$\Modify[\AM]{\IsCovFam\prn{\lambda i.\,A^\eta \cdot i}}$ where $A^{\eta}$ moves $A$ from the
context $\Gamma$ to $\Gamma.\brc{\AM}.\brc{\PM} = \Gamma.\brc{\AM}.\Int$ and
$- \cdot i$ realizes the $\Int$ hypothesis with $i$.

A type is said to be amazingly covariant when it satisfies the following predicate:

\[
\IsACov\prn{A} = \Modify[\AM]{\IsCovFam\prn{\lambda i.\,A^\eta \cdot i}}
\]

We begin by substantiating the claim that $\IsACov\prn{A}$ implies that $A$ is truly covariant over
all variables in the context.

Given $F : X \to \Sum{A : \Uni} \IsACov\prn{A}$, the type family $F_0 = \Proj[1] \circ F$ is a

We will write $\Uni[\ACov]$ for the subtype $\Sum{A : \Uni} \IsACov\prn{A}$.

We must show $\IsCovFam\prn{F_0}$. We begin by noting that
$\phi = \Proj[2] \circ F$ has the following type:

\[
\phi : \prn{x : X} \to \IsACov\prn{F_0\prn{x}}
\]

Using a dependent version of <ref>, we therefore obtain an element
of the following type:

\[
\phi' : \Modify[\AM]{
\prn{x : \prn{i : \Int} \to X^\eta \cdot i}
\to
\IsCovFam\prn{\lambda i.\,\prn{F_0^\eta \cdot i}\,\prn{x\,i}}
\]

By weakening, we may regard $\phi'$ as an element of the type
$\Int \to \Modify[\AM]{\dots}$ or, equivalently,
$\phi'' : \Modify[\PM \circ \AM]{\dots}$. We use $\Coe^{\epsilon}$ to remove
$\Modify[\PM \circ \AM]{-}$ from this type, and a tedious if mechanical calculation of the
action $-^{\epsilon}$ yields
$\Coe^\epsilon\,\phi'' : \prn{x : \Int \to X} \to \IsCovFam\prn{\lambda i.\,F_0\prn{x\,i}}$ as

We emphasize that in the above $\Uni[\ACov]$ does not “know about” $X$. In
particular, this is a subtype of $\Uni$ such that any map into this subtype induces covariant

Finally, the additional burden of being covariant over the context does not apply when working under
$\Modify[\GM]{-}$, a reflection of the fact of $\Modify[\GM]{A}$ is “a proof of $A$ not depending on
the context.”

If $\DeclVar{X}{\GM}{\Uni}$ and $\DeclVar{A}{\GM}{X \to \Uni}$ then
$\Modify[\GM]{\prn{x : X} \to \IsACov\prn{A\prn{x}}} = \Modify[\GM]{\IsCovFam\prn{A}}$.

§.§ Closure properties of amazing covariance

Given the strength of $\IsACov$, the reader may wonder how one every proves that $\IsACov\prn{A}$
for any element $A : \Uni$. In this section, we give a partial answer by building up a stock of
amazingly covariant types. We shall see in <ref> that these results undergird the closure
properties of our directed univalent universe. Our main is the result the following:

In what follow, let us assume that $A,A_0,A_1 : \Uni$ and $B : A \to \Uni$.

* If $\DeclVar{X}{\GM}{\Uni}$ then $\IsACov\prn{\Modify[\GM]{X}}$.

* If $i : \Int$ then $\IsACov\prn{i = 1}$.

* If $\IsACov\prn{A}$ and $a,b : A$ then $\IsACov\prn{a = b}$.

* If $\IsACov\prn{A}$ and $\prn{a : A} \to \IsACov\prn{B\prn{a}}$ then
$\IsACov\prn{\Sum{a : A} B\prn{a}}$.

* If $\IsACov\prn{A_0}$, $\IsACov\prn{A_1}$ and $f,g : A_0 \to A_1$ then
$\IsACov\prn{\Coeq\prn{f,g}}$.[Here $\Coeq\prn{f,g}$ denotes the coequalizer of $f,g$
realized as a higher-inductive type <cit.>.]

Moreover, $\IsACov$ is closed under $\Pi$-types provided modalities are used to
manage the variance swap:

* If $\DeclVar{C}{\OM}{\Uni}$ and $D : \MFn[\OM]{A}{\Uni}$ such that $\Modify[\OM]{\IsACov\prn{C}}$
and $\prn{\DeclVar{c}{\OM}{C}} \to \IsACov\prn{D\prn{c}}$ then
$\IsACov\prn{\prn{\DeclVar{c}{\OM}{C}} \to D\prn{c}}$.

We record a useful special case of (5) which follows from the involative property of $\Modify[\OM]{-}$:

If $\DeclVar{X}{\GM}{\Uni}$, $B : X \to \Uni$ such that $\Prod{x : X} \IsACov\prn{B\prn{x}}$
then $\IsACov\prn{\Prod{x : X} B\prn{x}}$.

For reasons of space, we will not prove each closure property listed in the above theorem, but
instead limit ourselves to two representative cases: (2) and (4).

If $i : \Int$ then $\IsACov\prn{i = 1}$.

To prove this result, we shall switch to a more general goal,
$\Modify[\GM]{ \prn{i : \Int} \to \IsACov\prn{i = 1}}$, which can then be specialized to yield the
original result.  Using <ref>, it suffices to construct an element of
$\Modify[\GM]{\prn{f : \Int \to \Int} \to \IsCovFam\prn{\lambda j.\,f\prn{j} = 1}}$

Since we have no additional hypotheses in this proof, we may forget the $\Modify[\GM]{-}$ and assume
$f : \Int \to \Int$. By <ref>, $\Int$ is an h-set and so $\IsCovFam\prn{f\prn{j} = 1}$ is
equivalent to showing that $f\prn{0} = 1$ implies that $f\prn{1} = 1$  that $f$ is
monotone. This is an immediate consequence of <ref>.

If $\IsACov\prn{A}$ and $\prn{a : A} \to \IsACov\prn{B\prn{a}}$ then $\IsACov\prn{\Sum{a : A} B\prn{a}}$.

Let us begin by applying the dependent version of <ref> to our assumption
$\prn{a : A} \to \IsACov\prn{B\prn{a}}$ such that it becomes the following:

\[
\Modify[\AM]{
\prn{a : \prn{i : \Int} \to A^\eta \cdot i}
\to
\IsCov\prn{\lambda i.\, \prn{B^\eta \cdot i}\,\prn{a\,i}}
\]

Applying the elimination and introduction rules for $\Modify[\AM]{-}$, the following now
suffices: if $A : \Int \to \Uni$ and $B : \prn{i : \Int} \to A\prn{i} \to \Uni$ such that
$\IsCov\prn{A}$ and $\IsCov\prn{\lambda i.\,B\,i\,\prn{a\,i}}$ then
$\IsCov\prn{\lambda i.\,\Sum{a : A\,i} B\,i\,a}$. This statement is proven by <cit.>.

Both proofs exhibit proof strategies that are common when working with $\IsACov$ in : either
reducing to a generic global case where various modalities can be simplified or performing several
small modal manipulations and then applying standard and non-modal arguments.

§ THE DIRECTED UNIVALENT UNIVERSE

With our preliminary work on amazing covariance in place, we are now in a position to define our
directed univalent universe of groupoids $\Space$ and establish its core properties. To a first
approximation, $\Space$ consists of types which are (1) amazingly covariant and (2) simplicial. The
former condition is needed to ensure directed univalence,  while the latter is really only
needed to ensure that $\Space$ captures the standard category of groupoids.

We define $\Space$ to be $\Sum{A : \Uni[\Simp]}{\IsACov\prn{A}}$.

In particular, $\Space$ is the subtype of $\Uni$ formed by intersecting $\Sum{A : \Uni} \IsACov\prn{A}$
and $\Sum{A : \Uni} \IsSimp\prn{A}$. We note that $\Space$ can be fully characterized without
reference to $\ACov$:[Theoretically, every result about $\Space$ can be proven using this
characterization. We will not endeavor to do so and instead optimize for more readable proofs.]

If $A : X \to \Uni[\Simp]$ lifts to $\Space$, it is covariant. If
$\DeclVar{A}{\GM}{X \to \Uni[\Simp]}$, this is a bi-implication.

$\DeclVar{A}{\GM}{\Uni}$ factors through $\Space$ if and only if it is a groupoid.

Moreover, by <ref> along with the closure results from
<cit.>, we conclude:

As a subtype of $\Uni$, $\Space$ is (1) univalent (2) closed under dependent sums, equality, and
$i = 1$ (3) closed under the two modalized forms of $\Pi$-types indicated by

Thus, we already have established that $\Space$ is a subuniverse of $\Uni$ spanned by
groupoids. What remains is to prove directed univalence , to characterize $\Int \to \Space$. To
this end, we will first prove two important lemmas for constructing elements of $\Space$. With these
in place, we shall show that $\Space$ is not only closed under various connectives, but also
simplicial, Segal, Rezk, and directed univalent. Our main result can be summed up as follows

$\Space$ is a directed univalent category.

§.§ The two key lemmas

Before we can prove that $\Space$ is directed univalent, we require a better understanding of when
two maps $\Int \to \Space$ are equivalent. In particular, suppose we are given
$f,g : \Int \to \Space$. We already know that $\Space$ is univalent and so $f$ and $g$ are equal
when there is an equivalence $\alpha : \prn{i : \Int} \to f\prn{i} \to g\prn{i}$. Accordingly, it
suffices to find conditions to establish that $\alpha\prn{i}$ is an equivalence for each $i :
\Int$. Our first result shows that this holds everywhere if it holds at $0$ and $1$. In other
words, to check that a natural transformation $\alpha$ is an equivalence, it suffices to check that
it is an equivalence at each object. We prove a slight generalization of this result which
applies to any $\Delta^\ell$ rather than just $\Delta^1$.

We denote $\prn{1, \dots, 1, 0, \dots 0} : \Delta^\ell$ with $k$ copies of $1$ followed by
$\ell - k$ copies of $0$ by $\bar{k}$.

Fix $\DeclVar{\ell}{\GM}{\Nat}$ and suppose that $\Mor[f,g]{\Delta^\ell}{\Space}$ and
$\alpha : \prn{\delta : \Delta^\ell} \to f\,\delta \to g\,\delta$ then $\alpha$ is invertible if
and only if $\Mor[\alpha\,\bar{k}]{f\,\bar{k}}{g\,\bar{k}}$ is invertible for all $k \le \ell$.

We begin by generalizing to apply <ref>. To this end, fix the following global

\begin{align*}
&X =
\Sum{F\,G : \Delta^\ell \to \Space}\Sum{\alpha : \prn{\delta:\Delta^\ell} \to F\,\delta \to G\,\delta}
\prn{k : \Nat_{\le \ell}} \to \IsEquiv\prn{\alpha\,\bar{k}}
\\
&Y =
\Sum{F\,G : \Delta^\ell \to \Space}\Sum{\alpha : \prn{\delta:\Delta^\ell} \to F\,\delta \to G\,\delta}
\Prod{\delta : \Delta^{\ell}}\IsEquiv\prn{\alpha\prn{\delta}}
\end{align*}

It suffices to show that the forgetful map $Y \to X$ is an equivalence and so, by
<ref>, we must show that for each $\DeclVar{n}{\GM}{\Nat}$ the map
$\Modify[\GM]{\Int^n \to Y} \to \Modify[\GM]{\Int^n \to X}$ is an equivalence. For clarity, we write
$\Gamma = \Int^n$ and $\Gamma' = \Int^n \times \Delta^{\ell}$ in what follows.

We now unfold this slightly. Fix $\DeclVar{F,G}{\GM}{\Gamma' \to \Space}$ along with
$\DeclVar{\alpha}{\GM}{\prn{\prn{v,\delta} : \Gamma'} \to F\prn{v,\delta} \to G\prn{v,\delta}}$ and
$\DeclVar{e}{\GM}{\prn{v : \Gamma}\prn{k : \Nat_{\le \ell}} \to
\IsEquiv\prn{\alpha\prn{v,\bar{k}}}}$. We must show the following:

\[
\Modify[\GM]{\prn{\prn{v,\delta} : \Gamma'} \to \IsEquiv\prn{\alpha\prn{v,\delta}}}
\]

We can reorient $F,G$ as global families $\Mor[\pi_F,\pi_G]{\tilde{F},\tilde{G}}{\Gamma'}$. That
both $F,G$ factor through space implies that they are both covariant fibrations and, therefore,
orthogonal to the maps $\brc{0} \to \Int^m$ for any $\DeclVar{m}{\GM}{\Nat}$. Note, too, that from
this viewpoint, $\alpha$ is a map $\tilde{\alpha} : \tilde{F} \to \tilde{G}$ over $\Gamma'$ such
that pulling back along $\prn{\ArrId{},\bar{k}} : \Gamma \to \Gamma'$ induces an equivalence. We
must show that $\tilde{\alpha}$ is an equivalence.

By another application <ref>, to show that $\tilde{\alpha}$ is an equivalence
we must show it induces an equivalence
$\Modify[\GM]{\Int^m \to \tilde{F}} \Equiv \Modify[\GM]{\Int^m \to \tilde{G}}$. By orthogonality, we
note that
$\Modify[\GM]{\Int^m\to\tilde{F}} \Equiv \Modify[\GM]{\tilde{F} \times_{\Gamma'} \prn{\Int^m \to
\Gamma'}}$.  Consequently, it suffices to show that the following map is an equivalence:

\[
\Modify[\GM]{\tilde{F} \times_{\Gamma'} \prn{\Int^m \to \Gamma'}} \to
\Modify[\GM]{\tilde{G} \times_{\Gamma'} \prn{\Int^m \to \Gamma'}}
\]

We may refactor this using the various properties of $\Modify[\GM]{-}$ to obtain the following
equivalent map:

\[
\Sum{\DeclVar{v}{\GM}{\Int^m \to \Gamma}}
\Sum{\DeclVar{\theta}{\GM}{\Int^m \to \Delta^{\ell}}}
\Modify[\GM]{F\prn{v\prn{\vec{0}},\theta\prn{\vec{0}}}}
\to
\Sum{\DeclVar{v}{\GM}{\Int^m \to \Gamma}}
\Sum{\DeclVar{\theta}{\GM}{\Int^m \to \Delta^{\ell}}}
\Modify[\GM]{F\prn{v\prn{\vec{0}},\theta\prn{\vec{0}}}}
\]

Finally, $\theta\prn{\vec{0}}$ is an element of $\Modify[\GM]{\Delta^{\ell}}$ and is therefore
equal to $\bar{k}$ for some $k$ by <ref>. For any $k$, the map is an equivalence
as it is derived from $\alpha$ and our conclusion follows.

<cit.> axiomatized their cobar modality to formulate and postulate a special
case of this lemma (their equivalence axiom). In our case, no such steps are required as
this result follows from <ref>.

To ensure that elements of $\Space$ are indeed groupoids, $A : \Uni$ lands in the subtype $\Space$
only when it is $A$ simplicial in addition to being amazingly covariant. Often, it is easiest to do
this by proving that $A$ is amazingly covariant and then applying $\Simp$ to $A$ to obtain a
simplicial type. In order for this to be possible, however, we must know that applying $\Simp$ to an
amazingly covariant type results in an amazingly covariant type. The next lemma proves (a
generalization of) this fact.

Let us note that the canonical maps $\Uni[\ACov] \to \Uni$ and $\Simp \Uni \to \Uni$ induce a map
$\DepSimp \Proj : \Simp \Uni[\ACov] \to \Uni$. Showing that $\Simp A$ is amazingly covariant if $A$
is amazingly covariant corresponds to showing that $\DepSimp \circ \eta$ factors through
$\Space$. We prove this by proving the following stronger result:

$\DepSimp \Proj : \Simp \Uni[\ACov] \to \Uni$ factors through $\Space$.

Given that the composite $\DepSimp \Proj : \Simp \Uni[\ACov] \to \Uni$ mentions no free variables
and (by construction) factors through $\Uni[\Simp]$, it suffices by
<ref> to show that $\DepSimp \Proj$ is covariant.

For concision, we write $X = \Simp \Uni[\ACov]$ and $\tilde{X}$ for $\Sum{A : X} \DepSimp A$. We
must show that the map given by evaluating at $0$ induces an equivalence between
$\Int \to \tilde{X}$ and $\prn{\Int \to X} \times_{X} \tilde{X}$. Using <ref>
along with the observation that these types are all simplicial, it suffices to show that the
following map is an equivalence for all $\DeclVar{n}{\GM}{\Nat}$:

\[
\Modify[\GM]{\Delta^n \times \Int \to \tilde{X}}
\to
\Modify[\GM]{
\Delta^n
\to
\prn{\Int \to X} \times_{X} \tilde{X}
\]

In other words, we must show that $\Delta^n \times \brc{0} \to \Delta^n \times \Int$ is
globally orthogonal to $\tilde{X} \to X$. By standard simplicial
combinatorics <cit.>, $\Delta^n \times \Int$ is the colimit of a collection of
simplices $\Delta^{n + 1}$. Using this and the left-cancellation property of the class of left
maps in an orthogonality problem, it suffices to show that for all $\DeclVar{m}{\GM}{\Nat}$ that is
right orthogonal to $\brc{\prn{0,\dots,0}} \to \Delta^m$. All told then, it suffices to show the
following canonical map is an equivalence:

\[
\Modify[\GM]{\Delta^m \to \tilde{X}}
\to
\Modify[\GM]{
\prn{\Delta^m \to X} \times_{X} \tilde{X}
\]

By <ref>, we may “remove the $\Simp$” from $X$ and $\tilde{X}$ and so
this type is equivalent to the following:

\[
\Modify[\GM]{\Delta^m \to \Sum{A : \Uni[\ACov]} A}
\to
\Modify[\GM]{
\prn{\Delta^m \to \Uni[\ACov]} \times_{\Uni[\ACov]} \prn{\Sum{A : \Uni[\ACov]} A}
\]

This, finally, is an equivalence because $\prn{\Sum{A : \Uni[\ACov]} A} \to \Uni[\ACov]$ is a
covariant (<ref>).

$\Space$ is closed under coequalizers in $\Uni[\Simp]$.

By <ref>, $\Uni[\ACov]$ is closed under coequalizers $\Coeq\prn{f,g}$
and so <ref> ensures the $\Simp \Coeq\prn{f,g}$ lands in $\Space$
as well. By <cit.>, this is the coequalizer in $\Uni[\Simp]$.

§.§ S is directed univalent, Segal, Rezk, and simplicial

We are now able to show that $\Space$ satisfies all the desired properties for a universe of
groupoids. We begin by showing that we have, at last, constructed a directed univalent universe.

First, we note that <ref> merely states that there is some isomorphism between two
types. We are already in a position to construct one of these two maps:

There is a function $\MorToFun$ from $\Int \to \Space$ to $\Sum{A\,B : \Space} A \to B$.

Given $F : \Int \to \Space$, by <ref> this induces a
covariant family $F_0 : \Int \to \Uni$. We then define
$\MorToFun\prn{F} \defeq \prn{F_0\,0,F_0\,1,F_0\,\ArrId{}}$ where the last component is induced by

$\MorToFun$ is an equivalence.

Prior to proving this result, we will construct a putative inverse to $\MorToFun$.

Given $A,B : \Space$ and $f : A \to B$, $\Glue\prn{A,B,f} : \Int \to \Space$ is
$\lambda i.\,\Sum{b : B} i = 0 \to f^{-1}\prn{b}$.

$\Glue$ is the directed version of the glue type from cubical type
theory <cit.>. We have no need to add it as a
primitive in our setting: this was necessary in cubical type theory toachieve certain definitional
equalities, but we are pervasively working up to equivalence. We note that $\Glue\prn{f}$ factors
through $\Space$ by virtue of (2–4) of <ref> along
<ref> which ensures that $\Modify[\OM]{\neg j = 1} = \prn{j = 0}$.

Given $A,B,f$ as above, $\Glue\prn{A,B,f}\,0 = A$, $\Glue\prn{A,B,f}\,1 = B$, and
$\Glue\prn{A,B,f}\,\ArrId{} = f$.

We will prove that $\Glue$ forms a quasi-inverse to $\MorToFun$ and thereby conclude that
$\MorToFun$ is an equivalence. We must therefore prove (1) $\MorToFun \circ \Glue = \ArrId{}$ and
(2) $\Glue \circ \MorToFun = \ArrId{}$. (1) follows from direct calculation and
<ref>, so we will detail only (2).

Suppose we are given $F : \Int \to \Space$. We must show that $F = \Glue\prn{\MorToFun\prn{F}}$ or
equivalently, using the fact that $\Space$ is univalent, that there is an equivalence
$\alpha : \prn{i : \Int} \to F\prn{i} \Equiv \Glue\prn{\MorToFun\prn{F}}\,i$. To prove this, we
will begin by constructing $\alpha$ and then use <ref> to reduce to checking
that $\alpha$ is an equivalence at $0$ and $1$.  It is helpful to do this in stages and so we
begin by supposing $i : \Int$ and $f : F\prn{i}$ and define $\alpha$ as follows for some $X$ and
$Y$ to be determined:

\[
\alpha\,i\,f = \prn{X : F\prn{1}, Y : i = 0 \to F\prn{\ArrId{}}^{-1}\prn{X}}
\]

We will construct $X$ and $Y$ separately.

We can substantiate $X$ immediately: $F\prn{\lambda j.\,i \lor j} : F\prn{i} \to F\prn{1}$ and so
we choose $X \defeq F\prn{- \lor i}\,f$. This refines the type of $Y$ to
$i = 0 \to F\prn{\ArrId{}}^{-1}\prn{F\prn{- \lor i}\,f}$. Assume $\phi : i = 0$ so that it
suffices to define $Y.1 : F\prn{0}$ and $Y.2 : F\prn{\ArrId{}}\,Y.1 = F\prn{- \lor i}\,f$. Using
$\phi$, we may suppose that $f : F\prn{0}$ and that the type of $Y.2$ is
$F\prn{\ArrId{}}\,Y.1 = F\prn{\ArrId{}}\,f$ (since $0 \lor - = \ArrId{}$). After this,
$Y.1 \defeq f$ and $Y.2 \defeq \Refl$ suffices.

Finally, it is now straightforward to check that $\alpha\,0$ and $\alpha\,1$ are equivalences
using <ref>.

The proof that $\Space$ is Segal is very similar to the proof of directed univalence, though not
quite a consequence of it. Since the proof is similar to <ref>, we provide only a

$\Space$ is Segal.

We must show that $\prn{\Delta^2 \to \Space} \to \prn{\Lambda^2_1 \to \Space}$ is an
equivalence. We begin by noting that the codomain can be rewritten with <ref> as
$T = \Sum{A\,B\,C : \Space} A \to B \times B \to C$. We only need to show that the
forgetful map from $\prn{\Delta^2 \to \Space} \to T$ is an equivalence.

This argument proceeds along the same lines as <ref> where we replace
$\Int$ with $\Delta^2$: we introduce a variant of $\Glue$ which glues together three spaces along
two maps and show that this procedure induces a quasi-inverse to the forgetful map
$\prn{\Delta^2 \to \Space} \to T$. It is here that we require <ref> with
$\ell = 2$ rather than $\ell = 1$.

Composition of the morphisms in $\Space$ is realized by ordinary function composition.

In particular, an invertible morphism corresponds via <ref> to an
equivalence. Combining this with ordinary univalence, we obtain:

$\Space$ is Rezk.

Our final result is that $\Space$ lands in the subuniverse of simplicial types.

$\Space$ is simplicial.

By <cit.>, it suffices to show that $\eta : \Space \to \Simp \Space$ has a
retraction. By univalence, the composite of $\eta : \Uni[\Simp] \to \Simp \Uni[\Simp]$ followed by
$\DepSimp : \Simp \Uni[\Simp] \to \Uni[\Simp]$ is the identity and so it suffices to show that
both these maps restrict to $\Space$. That is, it suffices to show that
$\DepSimp \circ \Proj : \Simp \Space \to \Uni$ factors through $\Space$. This is an immediate
consequence of <ref>.

We conclude by noting a few of the categorical properties $\Space$ enjoys:

$\Space$ is finitely complete and finitely cocomplete and satisfies descent <cit.>.

Finite completeness and cocompleteness are an immediate consequence of
<ref> along with <ref> which implies that a ,
categorical limit in $\Space$ is an ordinary  limit of groupoids. To prove the descent
properties, we must show that various limits and colimits commute appropriately. However, by
<ref> once more, this is an immediate consequence of the fact that limits and
colimits in  enjoy descent <cit.>.

§ CONSEQUENCES OF A DIRECTED UNIVALENT UNIVERSE

We now reap the rewards of our efforts in constructing $\Space$ and give a brief tour of the
consequences of this type. We show how directed univalence may be used to prove free theorems and
substantiate the directed structure identity principle. We also use it to construct various
foundational example categories and lay the groundwork for the development of higher algebra
within .

§.§ Free theorems from naturality

Directed univalence allows us to make a precise link between familiar parametricity
arguments <cit.> with the categorical naturality arguments that helped motivate
them. In particular, directed univalence implies that a function
$\alpha : \prn{A : \Space} \to F\prn{A} \to G\prn{A}$ is natural:

If $F_0,F_1 : \Space \to \Space$ and $\alpha : \prn{A : \Space} \to F_0\prn{A} \to F_1\prn{A}$ then
$\alpha\prn{B} \circ f = f \circ \alpha\prn{B}$ for any $f : A \to B$.

Fix $A,B : \Space$ along with $f : A \to B$ and denote the corresponding morphism
$G : \Int \to \Space$. Note that $\alpha \circ G$ is then a function
$\prn{i : \Int} \to F_0\prn{i} \to F_1\prn{i}$. Applying <ref> once more, we note
that $\alpha\prn{G\prn{i}} : F_0\prn{i} \to F_1\prn{i}$ is a morphism in $\Space$ for every
$i$. Accordingly, $\alpha \circ G$ is equivalent to some $s : \prn{i\,j : \Int} \to H\,i\,j$ for
some $H$ where $H\,i\,0 = F_0\,i$ and $H\,i\,1 = F\,i$. We visualize $H$ as:

\[
\DiagramSquare{
nw = F_0\,0,
sw = F_1\,0,
ne = F_0\,1,
se = F_1\,1,
north = F_0,
south = F_1,
west = \alpha\prn{G\,0},
east = \alpha\prn{G\,1},
height = 1cm,
\]

This commuting square is equivalently an equality between the composites $F_1$ and
$\alpha\prn{G\,0}$ and $\alpha\prn{G\,1}$ and $F_0$. The conclusion then follows from

Fix $A : \Space$ and suppose we are given $a : A$. Applying <ref> to $f$
and $\lambda \_.\,a$, we conclude that $f\,A\,\prn{a\,\star} = a\prn{f\,\ObjTerm{}\,\star}$. Since
$f\,\ObjTerm{}\,\star = \star$ by the $\eta$ principle of $\ObjTerm{}$, $f = \lambda A\,a.\,a$.

Nothing limits us to considering only operations $\Space \to \Space$. The same techniques scale to
multi-argument operations such as $\Space \times \Space \to \Space$ or even mixed-variance
operations such as $\Modify[\OM]{\Space} \times \Space \to \Space$:

If $\alpha : \prn{A\,B : \Space} \to A \times B \to A$ then $\alpha = \Proj[1]$.

If $\DeclVar{A,B}{\GM}{\Space}$ and
$\alpha : \prn{\DeclVar{C}{\OM}{\Space}} \to A^{\Modify[\OM]{C}} \to B^{\Modify[\OM]{C}}$ then
$\alpha = \lambda\_g.f \circ g$ for some $f : A \to B$.

This methodology highlights the limitations of naturality as a facsimile for parametricity:
for operations whose parameters are not used strictly co- or contravariantly, directed univalence
does not provide any free theorems. We leave it to future work to consider alternative universes of
correspondences <cit.> and what parametricity arguments they might provide.

§.§ Full subcategories of S

A large number of important categories can be described as a full subcategories of
$\Space$. To do this, we must first show how to obtain full subcategories inside of . Recall
that a full subcategory of $\CC_0$ of a category $\DeclVar{\CC}{\GM}{\Uni}$ is a category $\CC_0$ where
objects are a subset of those in $\CC$ but the morphisms and all the higher cells agree. In other
words, a full subcategory is described by a predicate $\MFn[\GM]{\CC}{\Prop_\Simp}$ which picks out
those objects which land in $\CC_0$.

Given $\DeclVar{\phi}{\SM}{\MFn[\GM]{\CC}{\Prop_\Simp}}$, the resulting full subcategory
$\CC_\phi$ is $\Sum{c : \CC} \Modify[\SM]{\phi\prn{c^\eta}}$.[In practice, $\phi$ will be

Here we for the first time have occasion to explicitly use the right adjoint $\SM$ to $\GM$. Let us
note that $\CC_\phi$ is a category because (1) categories are closed under dependent sums and (2)
$\Modify[\SM]{\phi\prn{c^\eta}}$ is a groupoid. Furthermore, we can prove that $\CC_\phi$ is
actually a full subcategory:

Given $\CC$ and $\phi$ as above, if $a,b : \CC_\phi$ then
$\Hom[\CC_\phi]{a}{b} \Equiv \Hom[\CC]{\Proj[1]\,a}{\Proj[1]\,b}$.

By choosing different predicates on $\Space$ we obtain a number of familiar
categories. For instance:

The category of $n$-truncated groupoids $\Space_{\le n}$ is given by
$\Space_{\Con{hasHLevel}\,(n+2)}$.[The correction $+2$ ensures that $\Space_{\le n}$
comports with the standard indexing in homotopy theory which begins at $-2$, not $0$.] In
particular, the category of propositions is given by $\Space_{\le -1}$, and the category of
sets is given by $\Space_{\le 0}$.

The category of finite sets $\FinSet$ is given by $\Space_\phi$ where
$\phi\prn{X} = \Sum{n : \Nat} \prn{X = \Nat_{\le n}}$.

Note that $\FinSet$ is quite different than $\Sum{A : \Space} \exists n.\,\Nat_{\le n} = A$, which
has only invertible morphisms. The definition of $\CC_\phi$ is necessary to ensure that $\phi$ is
applied only to the objects of $\CC$, not its higher cells.

<ref> implies that these examples inherit directed univalence from
$\Space$, the first instance of the directed structure identity principle
(DSIP) <cit.>: homomorphisms in structured types coincide with their standard
analytic formulations and, consequently, all terms and types are functorial for these analytic
morphisms. For instance, a morphism in $\FinSet$ corresponds to an ordinary function and,
consequently, a family $F : \FinSet \to \Space$ has an action $F\prn{A} \to F\prn{B}$ for any
ordinary function $A \to B$.

§.§ The directed structure identity principle

Not only full subcategories of $\Space$ enjoy DSIP, in this section we survey other
categories which satisfy it as well. As a prototypical example, we consider pointed spaces,
$\Space_* = \Sum{A : \Space} A$:

Homomorphisms $\Hom[\Space_*]{\prn{A,a}}{\prn{B,b}}$ are equal to pointed functions
$\Sum{f : A \to B} f\prn{a} = b$.

By construction, the projection map $\Space_* \to \Space$ is covariant, giving, for any pair of
pointed spaces $(A,a_0)$ and $(B,b_0)$, an equivalence between homomorphisms from $a_0$ to $b_0$
lying over a homomorphism $f : A \to B$ and identifications $f(a_0) = b_0$.

This same methodology can be applied to more general algebraic structures to yield categories of
, monoids, groups, rings,  which all enjoy DSIP. Rather than dealing with this
generality, we will focus on monoids to complete the example given in <ref>. We
recall the type of monoids:

\[
\Con{Monoid} =
\Sum{A : \Space_{\le 0}}
\Sum{\epsilon : A}
\Sum{\cdot : A \times A \to A}
\Con{isAssociative}\prn{\cdot}
\times \Con{isUnit}\prn{\cdot,\epsilon}
\]

By repeated application of the closure of categories under dependent sums, functions, and
equalities, we already conclude that $\Con{Monoid}$ is a category. More interesting, we can
characterize its homomorphisms. For space, we omit the proof; it is a rehashing of

A homomorphism
$\Hom{\prn{A,\epsilon_A,\cdot_A,\alpha_A,\mu_A}}{\prn{B,\epsilon_B,\cdot_B,\alpha_B,\mu_B}}$ is
precisely a standard monoid homomorphism  a function $A \to B$ commuting with multiplication
and the unit.

Substituting <ref> within <ref>, we obtain
the promised result:

To complete our goal of proving $\Con{sum}$ natural automatically, it remains only to define
$\Con{List}$ as an endomap of monoids where $\Con{List}\,A$ has pointwise
multiplication. Remarkably, this straightforward consequence of our results. One need only write
down the definition of this monoid in the ordinary way and conclude that it lifts to a functor
because the carrier ($\Con{List} = \Sum{n : \Nat} -^n$) is already known to be a functor
$\Space_{\le 0} \to \Space_{\le 0}$ using the closure under $\Sigma$ and $\Nat$; no
special argument is required.

We can also apply directed univalence to non-algebraic structures using our ability to define
$n$-presheaf categories $\PSH[n]{C} = \Modify[\OM]{C} \to \Space_{\le n}$. We consider the
representative example of partial orders, which we isolate as a full subcategory of a presheaf
category. In particular, we begin with the category of reflexive graphs:
$\RGraph = \PSH[0]{\Delta_{\le 1}}$ where $\Delta_{\le 1}$ is the “walking fork” given by the
pushout $\Delta_2 \Pushout{\Int} \Delta_2$ adjoining a pair of retractions $\partial_0,\partial_1$
to a single arrow $r : 1 \to 0$. While we have not ensured $\Delta_{\le 1}$ is a category, this does
not matter as $\RGraph$ is a category regardless.

We use directed univalence to characterize this categories objects as well as its higher

The category $\RGraph$ is equivalent to
$\Sum{G_0 : \Space_{\leq 0}} \Sum{G_1 : G_0 \times G_0 \to \Space_{\leq 0}} \Prod{x:G_0} G_1(x,x).$

Using the universal property of a pushout,
$\RGraph = \Space_{\le 0}^{\Delta^2} \times_{\Space^\Int} \Space_{\le 0}^{\Delta^2}$ and so
repeated application of <ref> proves
$\RGraph = \Sum{G_0\, G_1 : \Space_{\leq 0}} \Sum{s\,t : G_1 \to G_0}\Sum{r : G_0 \to G_1} sr = st$
and the conclusion now follows from a standard argument.

We isolate $\Pos \subseteq \RGraph$ as a full subcategory spanned by objects where $G_1$ is a
partial order:

$\Pos = \RGraph_\phi$ where
$\phi\prn{G} \defeq
\Con{isASym}\prn{G_1}
\times
\Con{isTrans}\prn{G_1}
\times
\Prod{x,y : G_0} \IsProp\prn{G_1\prn{x,y}}$

<ref> now proves that homomorphisms in $\Pos$ are precisely monotone maps:

If $P,Q : \Pos$ then
$\Hom[\Pos]{P}{Q} \Equiv \Sum{f : P_0 \to Q_0}{\prod_{x,y:P_0}P_1(x,y) \to Q_1(fx,fy)}$.

Finally, for the next subsection we isolate a category which is foundational to $\infty$-category
theory: the simplex category $\SIMP$ is the full subcategory $\Pos_\phi$ where
$\phi\prn{P} = \Sum{n : \Nat} P = \Delta^n$.

§.§ First steps in synthetic higher algebra

As homotopy (type) theorists like to quip: homotopy types are modern sets. Higher algebra seeks to
take this slogan a step further by studying groups, rings, modules,  in a world where homotopy
types have replaced sets. While higher algebra has numerous applications to algebraic topology,
algebraic K-theory, and algebraic geometry, it is also a notoriously technical: even the simplest
higher algebraic structure must account for an infinite tower of coherences for each imposed
equation. For our final application of $\Space$, we initiate the study of higher
algebra <cit.> in  by defining some of the central objects of
study.  We begin by upgrading defining the category of (homotopy-coherent and untruncated) monoids following

The category of coherent monoids $\Con{Monoid}_\infty$ as the full subcategory of $\PSH{\Delta}$
carved out by the following predicate (the Segal condition):

\[
\phi\prn{\DeclVar{X}{\GM}{\Modify[\OM]{\Delta}} \to \Space} =
\prn{n : \Nat}
\to
\IsEquiv\prn{\gl{X\prn{\iota_k}_{k < n}} : X\prn{\Delta^{n}} \to X\prn{\Delta^{1}}^n}
\]

In the above, $\iota_k : \Delta^{1} \to \Delta^{n}$ is $\lambda i.\,\prn{1, \dots, 1, i, 0, \dots}$
picking out $k$ copies of $1$.

In other words, a coherent monoid is a functor $X : \Modify[\OM]{\Delta} \to \Space$ such that
$X\prn{\Delta^{n}}$ is the $n$-fold product of $X\prn{\Delta^{1}}$. While somewhat indirect, these
conditions encode all the necessary structure , multiplication is
given by the composite map $\mu_X : X(\Delta^1)^2 \Equiv X(\Delta^2) \to X(\Delta^1)$.

As a small example of manipulating this definition, we prove the following:

The functor $\Con{Monoid}_\infty \to \Space$ induced by evaluation at $\Delta^{1}$ is conservative.

Given $f : X \to Y$, by <cit.> and <ref>, it
suffices to show that if $f\prn{\Delta^{1}}$ is an isomorphism so is $f\prn{\Delta^{n}}$ for any $n$. By
the Segal condition and naturality, $f\prn{\Delta^{n}}$ is equivalent to
$\prn{f\prn{\Delta^{1}}}_{i \le n}$ which is invertible if $f\prn{\Delta^{1}}$ is an

We can also define the category of coherent groups:

The category of coherent groups $\Con{Grp}_\infty$ is the full subcategory of
$\Con{Monoid}_\infty$ carved out by the predicate
$\phi{\prn{\DeclVar{X}{\GM}{\Con{Monoid}_\infty}}} = \IsEquiv\prn{\lambda x\,y.\prn{x,\mu\prn{x,y}} : X\prn{\Delta^{1}}^2 \to X\prn{\Delta^{1}}^2}$.

These concepts and many others can be unified through the formalism of ($\infty$-)operads but we
leave it to future work to develop this apparatus in . An application of such a
formalism would be the ability to develop higher algebra not just in $\Space$, but in
spectra, another fundamental category in modern homotopy theory. We conclude this section by
constructing this category.

Suppose $C$ is a pointed category with pullbacks, , $C$ has pullbacks and comes with an element
$0 : C$ which is simultaneously initial terminal and initial. Within $C$, we define the loop
functor $\Omega : C \to C$ by $\Omega \defeq \lambda x. 0 \times_x 0$. We have already
encountered such a pointed category: $\Space_*$.

The category of spectra $\Sp$ is defined as
$\Lim_{n : \Nat}
\prn{\dots \stackrel{\Omega}{\to} \Space_* \stackrel{\Omega}{\to} \Space_* \stackrel{\Omega}{\to} \Space_*}$.

Here $\lim$ refers to the ordinary definition of a limit from  and we note that as the limit
of categories, $\Sp$ is itself automatically a category. Using directed univalence, we can easily
show that objects of $\Sp$ are infinite deloopings of a groupoid as
expected <cit.>.

§ CONCLUSIONS AND RELATED WORK

We have introduced , an enhancement of simplicial type theory featuring modalities and a
relaxed interval type. We have used  as a framework to construct a directed univalent universe
of groupoids $\Space$ which we have further proven to be a well-behaved category. Finally, we have
used $\Space$ as a jumping off point to construct numerous examples of categories and categorical
reasoning in  relevant both to $\infty$-category theory and mechanized verification. In order
to do so, we have shown how our same modal operators can be used to , construct full

§.§ Related work

While directed type theory generally and simplicial type theory specifically are relatively new
areas, there is already substantial work exploring the impact of a “type theory where types are
categories.” Much of this work focuses on either constructing such type theories

or studying “formal” category theory within them

, statements which do not use particular closed non-trivial categories but instead quantify
over arbitrary categories. This is distinct from our focus, which has been to combine essentially
off-the-shelf type theories <cit.> and to use this combination
to prove facts about the concrete type $\Space$ and types derived thereof. Closely related to this
is the work by Cavallo, Riehl, and Sattler <cit.> and <cit.>, who both
study directed univalence, in respectively simplicial and bicubical type theory ().

Cavallo, Riehl, and Sattler give an alternative construction of $\Space$ in the intended model of
, similar to the classical proof due to <cit.>. They have argued externally
that this subuniverse satisfies directed univalence and a version of
<ref>. However, their work is strictly external and does not
consider how one might integrate $\Space$ within . Since they do not consider a modal
extension of , they cannot even formulate , <ref>
within their target type theory nor capitalize on internal arguments to simplify their
proofs. However, given that both our universe and theirs satisfy
<ref>, they are weakly equivalent and so our results further show
that their universe is , a finitely (co)complete category and closed under various connectives.

On the other hand, <cit.> consider a variant of  based on two layers of cubical
type theory: one to account for homotopy type theory and a further layer for the directed
interval. Bicubical type theory is to  as cubical type theory is to : it is conjectured
that  can be formally presented[<cit.> do not give a definition of
but instead describe the intended model for any such situation. Their model is, however,
constructive and so it is conjectured that such a definition would satisfy canonicity.] so as to
enjoy canonicity and normalization, but bicubical categories and groupoids are not expected to be
adequate for ordinary $\infty$-categories or $\infty$-groupoids. Accordingly,
make a different trade-off than us with a system with better expected
computation, but which cannot be used to properly reason about $\infty$-category theory. We believe
both approaches to directed type theory warrant further consideration to (1) study our results on
top of base cubical type theory rather than  and (2) to translate our new results to their
setting. In particular,  proves only that $\Space$ is directed univalent and does not prove
<ref> but we believe our proof, along with those results in
<ref>, can be translated.

More fundamentally, while they also work within an internal language and we draw on their overal
strategy in <ref>, theirs is the internal extensional type theory of
$\PSH{\CUBE_{\mathsf{undirected}} \times \CUBE_{\mathsf{directed}}}$ and so they must not only
constructing $\Space$ but also the base  around it. This substantially complicates some of
their constructions; their versions of , covariance, $\Glue$ and so on include details that are
automatically handled when working pervasively with .  This model falsifies
<ref> and so they must introduce an additional set of axioms (the cobar modality)
work around this. Finally,  observes the utility of $\Space$ for formalization and we are
able to provide complete examples of this having proven that $\Space$ is a directed univalent

While not about directed type theory, <cit.> also consider a  for simplicial
spaces. We drew inspiration for some of our axioms ( <ref>) from them and
expect their other principles will prove useful to . Furthermore, <cit.>
formulated a version of <ref> to study synthetic algebraic geometry which led us to its
inclusion in . Finally, <cit.> presents a type theory with a single amazing right
adjoint whose syntax is well-adapted for this situation. We hope that  can be generalized
for  to yield more usable syntax.

§.§ Future work

We isolate three key directions for future work. First, we wish to extend the experimental proof
assistant  <cit.> with the minimum level of modal reasoning (, at least
$\Modify[\GM]{-}$, $\Modify[\SM]{-}$ and $\Modify[\OM]{-}$) to properly axiomatize and work with
$\Space$ as constructed in this paper. We hope to then use this to mechanize
<ref>. Related to this, we hope to give a constructive model of  to give a
computational justification of our axioms. We expect this to contribute to a version of  with
canonicity and normalization <cit.>.

Second, we intend to generalize our construction of $\Space$ to construct the category of (small)
categories $\Cat$ and prove that it is suitably directed univalent <cit.>. While
modalities were required to construct $\Space$, they will be required to state the properties
of $\Cat$; directed univalence will become
$\Modify[\GM]{\Int \to \Cat} \Equiv \Modify[\GM]{\Sum{A : \Cat} \Sum{B : \Cat} A \to B}$ because
homomorphisms from $A$ to $B$ must be the groupoid of the category of functors $A \to B$, not
the category. Aside from this, we believe our results will scale to this more general setting.

Finally, while we discussed presheaf categories in <ref>, we avoided describing
the Yoneda embedding $C \times \Modify[\OM]{C} \to \Space$. While it is possible to construct this
operation, it requires one additional modality (the twisted arrow construction) and, for reasons of
space, we have regretfully chosen to omit it in the present work. In forthcoming work, we will
detail this additional modality along with the resulting definition of the Yoneda embedding. Using
this in conjunction with our work on full subcategories, we are able to prove various important
results  that $\Space$ is cocomplete.