# Formalizing the $\infty$-categorical Yoneda lemma

Nikolai Kudasov<EMAIL_ADDRESS>0000-0001-6572-7292 Lab of Programming
Languages and Compilers
Innopolis UniversityUniversitetskaya 1InnopolisTatarstan RepublicRussia420500
,  Emily Riehl  0000-0002-8465-8859<EMAIL_ADDRESS>and  Jonathan Weinberger
0000-0003-4701-3207<EMAIL_ADDRESS>Department of Mathematics
Johns Hopkins University3400 N Charles StreetBaltimoreMDUSA21218

###### Abstract.

The field of category theory seeks to unify and generalize concepts and
constructions across different areas of mathematics, from algebra to geometry
to topology and also to logic and theoretical computer science. Formalized
$1$-category theory forms a core component of various libraries of
mathematical proofs. However, more sophisticated results in fields from
algebraic topology to theoretical physics, where objects have “higher
structure,” rely on infinite-dimensional categories in place of
$1$-dimensional categories, and $\infty$-category theory has thusfar proved
unamenable to computer formalization.

Using a new proof assistant called Rzk, which is designed to support
Riehl–Shulman’s simplicial extension of homotopy type theory for synthetic
$\infty$-category theory, we provide the first formalizations of results from
$\infty$-category theory. This includes in particular a formalization of the
Yoneda lemma, often regarded as the fundamental theorem of category theory, a
theorem which roughly states that an object of a given category is determined
by its relationship to all of the other objects of the category. A key feature
of our framework is that, thanks to the synthetic theory, many constructions
are automatically natural or functorial. We plan to use Rzk to formalize
further results from $\infty$-category theory, such as the theory of limits
and colimits and adjunctions.

category theory, homotopy type theory, formalization, directed type theory,
$\infty$-category theory, Yoneda lemma, fibrations

††ccs: Theory of computation Logic and verification

##  1\. Introduction

_Computer proof assistants_ are computer programs that formally verify the
logical reasoning of mathematical proofs. There are a wide variety of such
programs — including Agda (Bove et al., 2009; Norell and Chapman, 2009), Coq
(Bertot and Castéran, 2013), HOL Light (Harrison, 2009), Isabelle (Nipkow et
al., 2002), and Lean (de Moura et al., 2015; de Moura and Ullrich, 2021),
among many others — which have enjoyed striking success in recent decades.
Notable accomplishments include:

  * •

A project (Hales et al., 2017) in Isabelle from 2003–2014, to formally verify
the Ferguson–Hales proof of the Kepler conjecture, after the referees for the
2005 _Annals_ publication issued a disclaimer stating that they were only 99%
certain of its correctness.

  * •

A project (Gonthier et al., 2013) in Coq, from 2006–2012, to formally verify
the Feit–Thompson Odd Order Theorem, a foundational result in the
classification of finite simple groups.

  * •

A project in Lean (de Moura and Ullrich, 2021), from 2020–2022, dubbed the
“liquid tensor experiment” (Scholze, 2022), to formally verify a result from
condensed mathematics after Peter Scholze expressed concern about the
correctness of his own proof.

Part of the task in formalizing a cutting-edge mathematical result is to
develop an accompanying _library_ of background mathematics on which it
depends. For instance, the liquid tensor experiment required a formalized
library of standard results from graduate-level homological algebra as well as
many other background topics.

In addition to homological algebra, Lean’s mathematics library mathlib
(mathlib Community, 2020) contains standard results from number theory,
representation theory, general topology, linear algebra including Banach and
Hilbert spaces, measures and integral calculus, random variables, basic
algebraic geometry, model theory, and category theory, among other topics.
Despite all these achievements, as of the writing of this article, Lean’s
mathlib doesn’t contain any $\infty$-category theory, and thus myriad recent
results from algebraic K-theory (Blumberg et al., 2013), derived and spectral
algebraic geometry (Lurie, 2004, 2018), the Langlands program (Fargues and
Scholze, 2021), and symplectic geometry (Nadler and Tanaka, 2020) are
inaccessible to formalization.

Building such a library would arguably be no more difficult than the successes
mentioned above, but the endeavor would be frustrated by the ways in which the
traditional set-based foundations for mathematics are not optimal for
reasoning about $\infty$-categories. To give a precise definition of an
$\infty$-_category_ — which, roughly speaking, is an infinite-dimensional
category with a weak composition law in which all morphisms above dimension 1
are weakly invertible — one must pick a “model,” a Bourbaki-style mathematical
structure presenting the $\infty$-categorical data (Camarena, 2013; Bergner,
2018). A variety of models — such as _quasi-categories_ (Boardman and Vogt,
1973; Joyal, 2002), _complete Segal spaces_ (Rezk, 2001), and _Segal
categories_ (Hirschowitz and Simpson, 2001; Pellissier, 2002) — are used at
various places in the literature, and theorems are often proven
“analytically,” in reference to the “coordinates” of a particular model. A
computer formalizer is thus faced with an unattractive choice of either

  * •

picking one model, which must then be used for the entire library of
subsequent results, or

  * •

formalizing multiple models and the comparisons between them (Joyal and
Tierney, 2007), which significantly increases the workload.111Experts in the
field often prefer to work “model-independently” (Ayala et al., 2022; Lurie,
2003) which can be done either by using $\infty$-category theory itself as the
ambient metatheory, or deploying the formalism of _$\infty$ -cosmoi_ (_i.e._ ,
categories of $\infty$-categories) (Riehl and Verity, 2022), but either
approach would require some initial formalization in a specific model of
$\infty$-categories.

###  1.1. Reimagining the foundations of $\infty$-category theory

A radical-sounding alternative, which we argue is worth taking seriously, is
to change the foundation system. The article “Could $\infty$-category theory
be taught to undergraduates?” (Riehl, 2023a) argues that it is possible to
narrow the gap between $\infty$-category theory and ordinary 1-category theory
by replacing the traditional foundations with a directed extension of
_homotopy type theory_ (Rijke, 2022; Univalent Foundations Program, 2013). The
basis for this claim is the paper (Riehl and Shulman, 2017) (and the follow-up
work of (Bardomiano Martínez, 2022; Buchholtz and Weinberger, 2023;
Weinberger, 2022a)), which develops the basic theory of $\infty$-categories in
an alternative foundational framework established there. The _simplicial type
theory_ is a formal framework that permits one to make the following intuitive
definitions rigorous:

  * •

A type is a _pre- $\infty$-category_ (aka a _Segal type_) if every composable
pair of arrows has a unique composite.

  * •

A pre-$\infty$-category is an _$\infty$ -category_ (aka a _Rezk type_) if
equalities are equivalent to isomorphisms.

  * •

A type is an _$\infty$ -groupoid_ (aka a _discrete type_) if equalities are
equivalent to arrows.

  * •

A type family is a _left fibration_ (aka a _covariant type family_) if every
arrow in the base type has a unique lift with specified domain.

The intended model of this formal system is Rezk’s complete Segal spaces
(Rezk, 2001), in which pre-$\infty$-categories correspond to Segal spaces
(Segal, 1968; Rezk, 2001), $\infty$-categories correspond to complete Segal
spaces (Rezk, 2001), and left fibrations correspond to left fibrations (de
Brito, 2016; Kazhdan and Varshavsky, 2014). This extends Shulman’s model of
homotopy theory, in which types are interpreted as Reedy fibrant simplicial
spaces (Shulman, 2015). The phrases “for all …there exists …unique” are meant
in the standard sense of homotopy type theory (Rijke, 2022; Univalent
Foundations Program, 2013). In particular, following the homotopical extension
of the Curry-Howard correspondence (Hofmann and Streicher, 1998; Awodey and
Warren, 2009; Voevodsky, 2009), _uniqueness_ means _contractibility_ — which
is precisely what is true semantically for the composition operation in an
$\infty$-category.222Those familiar with the Segal space model of
$\infty$-categories may be surprised that the definition of a
pre-$\infty$-category refers to binary sequences of composable arrows and not
also composable triples and quadruples and so on. Here the binary statement
subsumes the $n$-ary ones for $n\geq 0$ because it is interpreted _internally_
in the model as the assertion that the internal mapping types mapping out of
the $2$-simplex and out of its inner horn are equivalent (Riehl and Shulman,
2017, Section 5).

More generally, Shulman has proven that homotopy type theory has semantics in
any $\infty$-topos (Shulman, 2019; Riehl, 2023c) and Weinberger (Weinberger,
2022c) has shown that the simplicial type theory of (Riehl and Shulman, 2017)
can be interpreted in simplicial objects in any $\infty$-topos (Rasekh, 2022;
Stenzel, 2023; Martini, 2021).

###  1.2. Formalizing $\infty$-category theory

It is relatively standard practice in homotopy type theory to formalize
results while writing the corresponding paper proofs.333While homotopy type
theory cannot be formalized in Lean or Idris (Brady, 2013) because their
kernels assume that all types are sets, contradicting Voevodsky’s _univalence
axiom_ , it can be done in Agda, Coq, and a growing variety of experimental
proof assistants. At the time of the writing of (Riehl and Shulman, 2017) it
was not possible to formalize any of its results because the work is done in
an _extension_ of traditional homotopy type theory, with multilevel contexts
and a new type-forming operation providing _extension types_. But this is
possible now thanks to the proof assistant Rzk developed by Kudasov (Kudasov,
[n. d.]). Thus, finally one can formally test the claims made in the article
(Riehl, 2023a). This is the content of our project.

In §2, we describe the simplicial type theory, and in §3 we introduce
synthetic $\infty$-category theory. In §4, we describe the Rzk proof
assistant. In §5, we describe our formalization of the $\infty$-categorical
Yoneda lemma in Rzk. In §6, we compare this formalization with parallel
formalizations of the $1$-categorical Yoneda lemma in the agda-unimath (Rijke
et al., 2021) and mathlib libraries. In §7, we offer a few takeaways from this
formalization project and describe related future work.

###  1.3. Related work

A roughly parallel synthetic framework for $\infty$-category theory has been
proposed by Weaver and Licata using bicubical sets as an intended model
(Weaver and Licata, 2020). An alternate approach to formalizing higher
category is within the framework of _two-level type theory_ , using
extensional type theory as a meta-theory, see e.g. (Voevodsky, 2013; Annenkov
et al., 2023; Kraus, 2021).

A conceptual discussion of the approach behind simplicial type theory with
comparisons is done by Buchholtz in (Buchholtz, 2019). A self-contained
overview of both syntactic and semantic aspects of simplicial type theory is
given in the master’s thesis of Bakke (Bakke, 2021).

Furthermore, there has been extensive work on directed type theories (Licata
and Harper, 2011; Warren, 2013; Nuyts, 2015; North, 2019), though most of this
was not created to describe $\infty$-category theory. Other work includes
domain-specific languages for two-dimensional categories (Garner, 2009; Ahrens
et al., 2022) and virtual equipments (New and Licata, 2023). There also exist
other type theories capturing infinite-dimensional categorical structures.
Notable developments include (Finster et al., 2021, 2022; Dean, 2020; Finster
and Mimram, 2017; Benjamin et al., 2021; Allioux et al., 2021; Bordg and Doña
Mateo, 2023). However, these systems differ from the one that we are using in
two major aspects: their setup and their purposes. Our framework features a
synthetic and homotopical theory of $\infty$-categories with the aim of
developing a range of classical $\infty$-categorical results. The other
frameworks tend to involve a specific model of either strict or weak infinite-
dimensional categories.

Aside from direct applications to category theory, new kinds of type theories
have been devised for the purpose of doing differential topology and stable
homotopy theory synthetically, making heavy use of type-theoretic _modalities_
(Shulman, 2018; Schreiber and Shulman, 2014; Cherubini, 2022; Rijke et al.,
2020; Myers, 2022a, 2021, b; Riley et al., 2021; Myers and Riley, 2023).

##  2\. The simplicial type theory

In (Riehl and Shulman, 2017), Riehl–Shulman develop a type theory to reason
synthetically about $\infty$-categories. The key features of their theory is
that $\infty$-categories can be described in relatively simple terms, and all
the results are invariant under _homotopy equivalence_ —the right notion of
equivalence of $\infty$-categories. This is in stark contrast to the more
traditional and familiar developments of $\infty$-category theory in set
theory, cf. e.g. (Lurie, 2009; Joyal, 2008). We will give an overview of the
structure and features of the simplicial type theory, with an emphasis on its
use for synthetic $\infty$-category theory.

The theory builds on Martin-Löf intensional type theory (MLTT) (Martin-Löf,
1975) whose _intensional identity types_ have homotopically well-behaved _path
objects_ as models (Awodey and Warren, 2009; Kapulkin and Lumsdaine, 2021;
Streicher, 2014; Riehl, 2023b). This homotopical interpretation, paired with
Voevodksy’s _univalence axiom_ , which allows one to treat homotopy equivalent
types as (intensionally) equal, goes by the name _homotopy type theory_ (HoTT)
or _univalent foundations_ cf. (Voevodsky, 2009; Awodey and Warren, 2009;
Univalent Foundations Program, 2013). Homotopy type theory may be thought of
as a synthetic theory for $\infty$-groupoids (aka homotopy types) and thus
provides a fertile basis for the simplicial type theory.

###  2.1. Base theory: Martin-Löf intensional type theory

#### Overview

The base theory is intensional Martin-Löf type theory (Martin-Löf, 1975) with
$\Sigma$-, $\Pi$-, and identity types. Though Rzk works with a universe types
to implement dependent types, this assumption is not necessary (Riehl and
Shulman, 2017, Remark 2.5).444In particular, though convenient for certain
applications, univalence is not necessary for our development. To stay in line
with the notation of (Riehl and Shulman, 2017), we also notate a dependent
type $x:A\vdash C(x)$ as a _type family_ $C:A\to\mathcal{U}$, pretending
$\mathcal{U}$ is a universe type (without being explicit about universe
hierarchy or different levels of size).

####  $\Sigma$-types (05-sigma)

The type formers $\Sigma$ and $\Pi$, resp., generalize existential and
universal quantification, resp., as follows. For $C:A\to\mathcal{U}$, the
_dependent sum_ $\sum_{x:A}C(x)$ is the type consisting of dependent pairs
$(a,c)$ with $a:A$ and $c:C(a)$. This is also referred to as the _total type_
of the family $C$. The $\Sigma$-type comes with the usual set of rules for
formation, introduction (by forming dependent pairs), and elimination (by
projecting to the factors). We also assume the $\beta$\- and
$\eta$-computation rules to be satisfied, meaning that introduction and
elimination are inverse to each other in the strictest possible way, _i.e._ ,
_up to judgmental equality_.

The family $C:A\to\mathcal{U}$ can alternatively be encoded as a map
$p_{C}:\widetilde{C}\to A$, with the total type
$\widetilde{C}:\equiv\sum_{x:A}C(x)$, and the projection $p_{C}(a,c):\equiv
a$. The total type is then the “sum” of all the fibers of $C$, canonically
indexed by $A$. If $C$ is a constant family, _i.e._ , $C(a)\equiv B$ for all
$a:A$ and some type $B$, the $\Sigma$-type becomes the _cartesian product_
$A\times B$.

####  $\Pi$-types

Of particular interest is the notion of _dependent function_ or _section_ of a
family $C:A\to\mathcal{U}$, which is an assignment $\sigma$ to each element
$x:A$ of some element $\sigma(x):C(x)$ in the corresponding fiber. This is
reified as the _dependent product_ type $\prod_{x:A}C(x)$, with introduction
rule given by $\lambda$-abstraction and elimination rule by function
application. Likewise, we require the $\beta$\- and $\eta$-rules to hold
judgmentally. When the type family $C$ is constant with value some type $B$,
the dependent function type reduces to an ordinary function type, denoted by
$A\to B$ or $B^{A}$.

#### Identity types (01-paths)

The _Martin-Löf identity types_ $(a=_{A}b)$ for a type $A$ and elements
$a,b:A$ capture the idea that equality between terms of a type is witnessed
proof-relevantly by a term $p:a=_{A}b$. In the homotopical models, identity
types get interpreted as _path objects_ in the sense of homotopical algebra
(Awodey and Warren, 2009), so elements $p:(a=_{A}b)$ can be seen as paths from
$a$ to $b$ in $A$. The introduction rule is given by the canonical
_reflexivity terms_ $\textup{refl}_{a}:(a=_{A}a)$ witnessing self-identity.
Elimination is given by the _path induction principle_. Intuitively, this says
the following. First, for a type $A$, fix $a:A$. Then, for a family
$C:\left(\sum_{x:A}(a=_{A}x)\right)\to\mathcal{U}$ the type of sections
$\prod_{(y,p):\sum_{x:A}(a=_{A}x)}C(y,p)$ is equivalent to
$C(a,\textup{refl}_{a})$ via the map

$\mathsf{evrefl}_{C,a}:\left(\prod_{(y,p):\sum_{x:A}(a=_{A}x)}C(y,p)\right)\to
C(a,\textup{refl}_{a}).$

In particular, given $d:C(a,\textup{refl}_{a})$ we obtain a section

$\mathsf{ind}_{=}(d):\prod_{(y,p):\sum_{x:A}(a=_{A}x)}C(y,p)$

such that $\mathsf{ind}_{=}(d)(a,\textup{refl}_{a})\equiv d$. Thus, for type
families over (based) path types, to produce a section of the whole family it
suffices to produce a section only at the reflexivity loop.

#### The homotopy theory of types

The following notions are due to Voevodsky (Voevodsky, 2009), cf. also (Awodey
and Warren, 2009; Kapulkin and Lumsdaine, 2021; Streicher, 2014; Riehl,
2023b). According to the idea that terms $p:(a=_{A}b)$ encode paths in a type
we want to express when a type is homotopically trivial _aka_  _contractible_.
This is witnessed by the type

$ \mathsf{isContr}(A)\mathrel{\vcentcolon\equiv}\sum_{x:A}
\prod_{y:A}(x=_{A}y).$

A contractible type $A$ comes equipped with a canonical inhabitant, the
_center of contraction_ $c_{A}:A$ (contraction-center) and a homotopy
$H_{A}:\prod_{y:A}(c_{A}=_{A}y)$ (contracting-htpy). Contractible types are
equivalent to the point or _terminal type_ $\mathbf{1}$, see (contr-iff-
terminal-map-is-equiv).

Traditional homotopy theory involves constructions on topological spaces that
are invariant under _homotopy equivalence_ , which is a pair of maps between
two spaces in opposite directions whose composites are homotopic to the
identity. Translating this into type theory, a map $f:A\to B$ between types is
a (homotopy) equivalence when there is a term inhabiting the type

$\mathsf{isEquiv}(f)\mathrel{\vcentcolon\equiv}\sum_{g:B\to A}(g\circ f=_{A\to
A}\mathsf{id}_{A})\times\sum_{h:B\to A}(f\circ h=_{B\to B}\mathsf{id}_{B}).$

This type is a _proposition_ in the sense that it is contractible whenever if
it is inhabited. By (Rijke, 2022, 12.1.3), this can equivalently be captured
by the type

$ \mathsf{isProp}(A)\mathrel{\vcentcolon\equiv}\prod_{x,y:A} (x=_{A}y).$

When a type $A$ is a proposition (_i.e._ , $\mathsf{isProp}(A)$ is inhabited),
then it can be treated as a _mere property_ (up to homotopy, _i.e._ , a
contractible and thus trivial choice of data) rather than additional
_structure_. The fact that $\mathsf{isEquiv}(f)$ is always a proposition hence
means that being an equivalence is, in fact, a _property_ of a map, much in
line with the expected intuition. It turns out there is a further equivalent
characterization of when a map is an equivalence in that sense, namely if and
only if all its _fibers_
$\mathsf{fib}(f,b)\mathrel{\vcentcolon\equiv}\sum_{x:A}(f(x)=_{A}b)$ are
contractible, _i.e._ ,

$\mathsf{isEquiv}(f)\simeq\prod_{b:B} \mathsf{isContr}(\mathsf{fib}(f,b)).$

If type families are understood as _fibrations_ $p:\sum_{x:A}C(x)\to A$, then
equivalences in this sense behave like _trivial fibrations_ (10-trivial-
fibrations) whose fibers are all contractible. These homotopical
interpretations of Martin Löf’s dependent type theory open up a whole area of
research doing homotopy theory synthetically, cf. (Univalent Foundations
Program, 2013; Rijke, 2022).

#### Function extensionality (FunExt)

While we do not require the univalence axiom in our formalization, we do make
use of _function extensionality_ , which is one of its consequences (Rijke,
2022, Theorem 17.3.2): we will postulate the map

$
\mathsf{htpy}\text{-}\mathsf{eq}:\prod_{X:\mathcal{U}}\prod_{A:X\to\mathcal{U}}\prod_{f,g:\prod_{X}A}(f=g)\to\prod_{x:X}(fx=gx)$

defined via path induction by

$\mathsf{htpy}\text{-}\mathsf{eq}(X,A,f,f,\textup{refl}_{f},x)\mathrel{\vcentcolon\equiv}\textup{refl}_{fx}$

is an equivalence, _i.e._ , there exists a term

$\mathsf{funext}:\prod_{X:\mathcal{U}}\prod_{A:X\to\mathcal{U}}\prod_{f,g:\prod_{X}A}\mathsf{isEquiv}(\mathsf{htpy}\text{-}\mathsf{eq}_{X,A,f,g}).$

#### The $\infty$-groupoid structure on a type

By (iterated) path induction one can prove the existence of functions

(rev) $\displaystyle\prod_{x,y:A} (x=_{A}y)\to(y=_{A}x),$ (concat)
$\displaystyle\prod_{x,y,z:A} (x=_{A}y)\to(y=_{A}z)\to(x=_{A}z)$

serving to reverse paths as well as concatenating them. One can show that
these satisfy the expected groupoid laws, but only up to propositional
equality, endowing every type canonically with the structure of a (weak)
$\infty$-groupoid, cf. (Hofmann and Streicher, 1998; van den Berg and Garner,
2011).

While $\infty$-groupoids are special cases of $\infty$-categories, in a
general $\infty$-category we require directed “arrows” that are not
necessarily reversible. This suggests the following extensions of the
underlying type theory.

###  2.2. Extension 1: Cube and tope layers

Intuitively, a synthetic $\infty$-category is a type where directed arrows can
be composed up to homotopy. To reason about directed arrows, their composites,
and other shapes arising from this the idea is to introduce an appropriate
shape theory to the type theory. The shapes will be part of the contexts so
that type families and sections can depend on them.

Each shape is viewed as a _subshape_ embedded inside a _higher dimensional
(directed) cube_. This is reminiscent of the basic setup of _cubical type
theory_ (Bezem et al., 2014; Cohen et al., 2018; Orton and Pitts, 2018;
Cavallo et al., 2020; Angiuli et al., 2021).

For the _cube layer_ , consider a new pretype $\mathbbn{2}$, equipped with two
distinct elements $0,1:\mathbbn{2}$, and a binary relation $\leq$ making
$\mathbbn{2}$ into a strict partial order with bottom element $0$ and top
element $1$. The Lawvere theory generated by $\mathbbn{2}$ constitutes the
cube layer, _i.e._ , the cubes are exactly the finite powers
$\mathbbn{2}^{n}$, with $\mathbbn{2}^{0}\equiv\mathbf{1}$. The partial order
is captured by a new judgment form, called a tope:

$x,y:\mathbbn{2}\vdash x\leq y\,\mathsf{tope}$

The _tope layer_ is a finitary intuitionistic logic over the cube layer. The
intention is to carve out _subshapes_ $\Phi\subseteq I$ of a cube $I$ by
describing it via a formula on the cube variables. In general: if $I$ is a
cube and $\varphi$ is a tope in context $t:I$, written as a judgment
$t:I\vdash\varphi\,\mathsf{tope}$, then
$\Phi\mathrel{\vcentcolon\equiv}\\{t:I\;| \;\varphi\\}$ is the _shape_
corresponding to $\varphi$. This way, one can define important shapes such as
the $n$-simplex $\Delta^{n}$, for $n\in\mathbb{N}$, its boundaries
$\partial\Delta^{n}$, the _$(n,k)$ -horns_ $\Lambda_{k}^{n}$ for $k\leq n$,
and more. E.g., we have the following formulas, cf. also Figure 1:

$\displaystyle\Delta^{1}$
$\displaystyle\mathrel{\vcentcolon\equiv}\\{t:\mathbbn{2}\mid\top\\}\subseteq\mathbbn{2}$
$\displaystyle\partial\Delta^{1}$
$\displaystyle\mathrel{\vcentcolon\equiv}\\{t:\mathbbn{2}\mid(t\equiv
0)\lor(t\equiv 1)\\}\subseteq\mathbbn{2}$ $\displaystyle\Delta^{2}$
$\displaystyle\mathrel{\vcentcolon\equiv}\\{(t,s):\mathbbn{2}^{2}\mid\top\\}\subseteq\mathbbn{2}^{2}$
$\displaystyle\partial\Delta^{2}$
$\displaystyle\mathrel{\vcentcolon\equiv}\\{(t,s):\mathbbn{2}^{2}\mid(s\equiv
0)\lor(s\equiv t)\lor(t\equiv 1)\\}\subseteq\mathbbn{2}^{2}$ (03-simplicial-
type-theory) $\displaystyle\Lambda_{1}^{2}$
$\displaystyle\mathrel{\vcentcolon\equiv}\\{(t,s):\mathbbn{2}^{2}\mid(s\equiv
0)\lor(t\equiv 1)\\}\subseteq\mathbbn{2}^{2}$

Like in cubical type theory, we connect the standard type layer with the cube
and tope layer through a three-part context, which allows type families $A$ to
depend on a cube context $\Xi$, a tope context $\Phi$, and a type context
$\Gamma$, written as $\Xi\mid\Phi\mid\Gamma\vdash A$.

The directed arrows in a type are now defined using our interval shape
$\Delta^{1}$ and another feature to be introduced, the _extension types_.

${11}$${11}$${0}$${1}$${00}$${10}$${00}$${10}$${{\Delta^{1}\subseteq\mathbbn{2}}}$${{\Lambda_{1}^{2}\subseteq\mathbbn{2}^{2}}}$${{\Delta^{2}\subseteq\mathbbn{2}^{2}}}$
Figure 1. Some important shapes

###  2.3. Extension 2: Extension types (04-extension-types)

Let $\Phi\subseteq\Psi$ be an inclusion of subshapes, in cube context $I$. An
_extension type_ as introduced in (Riehl and Shulman, 2017), originally due to
unpublished work by Lumsdaine and Shulman, captures the strict extension of a
section defined on the smaller shape $\Phi$ to the larger shape $\Psi$.
Concretely, assume given a type family $I\;|\;\Psi\;|\;\Gamma\vdash A$
together with a partial section $t:I\;|\;\Phi\;|\;\Gamma\vdash a(t):A(t)$ over
the subshape $\Phi\subseteq\Psi$. Then, the corresponding _extension type_ has
as elements the strict extensions $t:I\;|\;\Psi\;|\;\Gamma\vdash b(t):A(t)$
such that $a|_{\Phi}\equiv b$. We denote the extension type by
$\left\langle\mathchoice{\textstyle\prod_{t:\Psi}}{\textstyle\prod_{t:\Psi}}{\scriptstyle\prod_{t:\Psi}}{\scriptscriptstyle\prod_{t:\Psi}}A(t)\middle|^{\Phi}_{a}\right\rangle$.
In case $A$ is a constant type, the ensuing extension type will be written as
$\left\langle\Psi\to A\middle|^{\Phi}_{a}\right\rangle$.

In analogy to ordinary type-to-type function types, we can emulate shape-to-
type function types by instantiating extension types by the “empty tope”
$\varphi\mathrel{\vcentcolon\equiv}\bot$ and the canonical term
$\mathsf{rec}_{\bot}$, allowing us to define the functions of shape $\Psi$
into type $A$ as $\Psi\to A\mathrel{\vcentcolon\equiv}\left\langle\Psi\to
A\middle|^{\bot}_{\mathsf{rec}_{\bot}}\right\rangle$, and similarly for the
dependent case.

#### Extension extensionality (ExtExt)

Just as in (Riehl and Shulman, 2017, Section 4), to make the extension types
homotopically well-behaved, we also assume a version of function
extensionality for extension types. In Rzk, we postulate an axiom that allows
us to extend relative homotopies between extensions of a given partial
section.

Namely, let $I$ be a cube and $\Phi\subseteq\Psi\subseteq I$ be a shape
inclusion. Consider a type family $A:\Psi\to\mathcal{U}$ with a partial
section $a:\prod_{t:\Phi} A(t)$. As in the case of dependent functions, we may
use path induction to define a map for any
$f,g:\left\langle\mathchoice{\textstyle\prod_{t:\Psi}}{\textstyle\prod_{t:\Psi}}{\scriptstyle\prod_{t:\Psi}}{\scriptscriptstyle\prod_{t:\Psi}}A(t)\middle|^{\Phi}_{a}\right\rangle$
of the form

(ext-htpy-eq)
$\mathsf{exthtpyeq}_{A,a,f,g}:(f=g)\to\left\langle\mathchoice{\textstyle\prod_{t:\Psi}}{\textstyle\prod_{t:\Psi}}{\scriptstyle\prod_{t:\Psi}}{\scriptscriptstyle\prod_{t:\Psi}}f(t)=g(t)\middle|^{\Phi}_{\textup{refl}}\right\rangle.$

As we did for function extensionality, we assert an extension extensionality
axiom of the following form.

###### Axiom 2.1 (ExtExt).

For any $A$, $a$, $f$, and $g$ as above, the map (ext-htpy-eq) is an
equivalence, _i.e._ , there exists a term

$\mathsf{extext}:\prod_{A,a,f,g}\mathsf{isEquiv}(\mathsf{exthtpyeq}_{A,a,f,g})$

In the original paper, 2.1 is derived from another version of the extension
extensionality axiom (Riehl and Shulman, 2017, Axiom 4.6). This version is
analogous to the version of function extensionality that states that, given a
family $B:A\to\mathcal{U}$, then if every fiber $Bx$ is contractible, then so
is the type $\prod_{x:A}Bx$.

In the case of function extensionality, this is known to be equivalent to the
version of function extensionality (FunExt). However, it is not known whether
this equivalence also holds for extension types. Therefore, Riehl–Shulman
assume the version appearing as (Riehl and Shulman, 2017, Axiom 4.6) since
they show that the other desired versions, such as (ExtExt), can be derived
from it.

The axiom (Riehl and Shulman, 2017, Axiom 4.6) is called _relative function
extensionality_ (or _extension extensionality_), and it reads as follows. Let
$\Phi\subseteq\Psi\subseteq I$ be a shape inclusion and let
$A:\Psi\to\mathcal{U}$ be a family such that each $A(t)$ is contractible.
Then, given $a:\prod_{t:\Phi}A(t)$, the type
$\left\langle\mathchoice{\textstyle\prod_{t:\Psi}}{\textstyle\prod_{t:\Psi}}{\scriptstyle\prod_{t:\Psi}}{\scriptscriptstyle\prod_{t:\Psi}}A(t)\middle|^{\Phi}_{a}\right\rangle$
is contractible. Our version (ExtExt) then follow as one of the consequences
established in (Riehl and Shulman, 2017, Proposition 4.8).

##  3\. Synthetic $\infty$-categories

Simplicial type theory is a combination of the homotopical interpretation of
Martin-Löf type theory with strict shape and extension types. As demonstrated
in (Riehl and Shulman, 2017; Buchholtz and Weinberger, 2023; Weinberger,
2022c; Bardomiano Martínez, 2022), this framework is powerful enough to
develop $\infty$-category theory synthetically, within a genuinely homotopical
framework.

###  3.1. Pre-$\infty$-categories and $\infty$-categories

#### Hom types (hom)

${{\Bigg{\\{}{\small x}}}$${{{\small y}}}$${{{\small
z}\Bigg{\\}}}}$${{\Bigg{\\{}{\small x}}}$${{{\small y}}}$${{{\small
z}\Bigg{\\}}}}$$\scriptstyle{\simeq}$$\scriptstyle{{\small
g}}$$\scriptstyle{{\small f}}$$\scriptstyle{{\small g}}$$\scriptstyle{{\small
g\circ f}}$$\scriptstyle{{\small
f}}$$\scriptstyle{{\tiny\mathrm{comp}_{f,g}}}$ Figure 2. The Segal condition

Let $A$ be a type with elements $a,b:A$. The $1$-simplex serves as the shape
for our directed arrows.

Thus, the type of _(directed) arrows_ or _homomorphisms_ from $a$ to $b$ is
the extension type

$\hom_{A}(a,b)\mathrel{\vcentcolon\equiv}\left\langle\Delta^{1}\to
A\middle|^{\partial\Delta^{1}}_{[a,b]}\right\rangle,$

where $t:\partial\Delta^{1}\vdash[a,b](t):A$ is the term with $[a,b](0)\equiv
a$ and $[a,b](1)\equiv b$.

#### Identity arrows (id-arr)

By the introduction rule for extension types, any element $x:A$ induces an
arrow $\mathsf{id}_{x}:\hom_{A}(x,x)$,
$\mathsf{id}_{x}\mathrel{\vcentcolon\equiv}\lambda s.x$.

#### Segal types (05-segal-types)

We can now impose a synthetic version of the Segal condition (Grothendieck,
1961; Segal, 1968), witnessing that a type admits unique composition of arrows
up to contractibility.

###### Definition 3.1 (Segal types; is-segal).

A type is a _Segal type_ or a _pre- $\infty$-category_ if any composable pair
of arrows has a unique composite, _i.e._ , given a pair of arrows
$f:\hom_{A}(x,y)$ and $g:\hom_{A}(y,z)$ the type of fillers

$\sum_{h:\hom_{A}(x,z)}\hom_{A}^{2}(f,g;h)$

is contractible, where

$\hom_{A}^{2}(f,g;h)\mathrel{\vcentcolon\equiv}\left\langle\Delta^{2}\to
A\middle|^{\partial\Delta^{2}}_{[f,g;h]}\right\rangle$

is the type of $2$-simplices bounded by a fixed choice of $1$-simplices:

$
\mathsf{isSegal}(A)\mathrel{\vcentcolon\equiv}\prod_{\begin{subarray}{c}x,y,z:A\\\
f:\hom_{A}(x,y)\\\ g:\hom_{A}(y,z)\end{subarray}}\\\
\mathsf{isContr}\left(\sum_{h:\hom_{A}(x,z)}\hom_{A}^{2}(f,g;h)\right)$

This means, up to homotopy there exists a unique arrow $g\circ
f:\hom_{A}(x,z)$ acting as a composite of $g$ and $f$, together with a
$2$-cell $\mathsf{comp}_{A,f,g}:\hom_{A}^{2}(f,g;g\circ f)$ that witnesses
that the $2$-simplex bounded by $f$, $g$, and $g\circ f$, is filled, cf.
Figure 2.

One can show that that the Segal condition of 3.1 can be reexpressed by saying
that the type $A$ is local with respect to an inner horn inclusion.

###### Theorem 3.2 (is-segal-iff-is-local-horn-inclusion).

A type $A$ is Segal if and only if restriction along the shape inclusion
$\Lambda_{1}^{2}\subseteq\Delta^{2}$ is an equivalence

$\mathsf{isEquiv}\Big{(}\mathsf{res}_{A}:A^{\Delta^{2}}\to
A^{\Lambda_{1}^{2}}\Big{)}.$

#### Isomorphisms in Segal types

In a Segal type $A$ we may define the type of _isomorphisms_ by

$
\mathrm{iso}_{A}(x,y)\mathrel{\vcentcolon\equiv}\sum_{f:\hom_{A}(x,y)}\mathsf{isIso}(f),$

where

$ \mathsf{isIso}(f)\mathrel{\vcentcolon\equiv}\sum_{g:\hom_{A}(y,x)}g\circ
f=\mathsf{id}_{x}\times\sum_{h:\hom_{A}(y,x)}f\circ h=\mathsf{id}_{y}.$

This is in analogy with the definition of equivalences in §2.1, and
$\mathsf{isIso}(f)$ is a proposition whenever the ambient type $A$ is Segal
(is-prop-is-iso-arrow).

#### Rezk types (10-rezk-types)

Segal types, cf. 3.1, have two competing notions of sameness between terms,
defined by the identity types and by the types of isomorphisms. A
pre-$\infty$-category is an $\infty$-category if the notion of isomorphism
just defined coincides with the notion of path in a type. This requirement
captures the established notions of _Rezk completeness_ or _local univalence_
(Rezk, 2001; Ahrens et al., 2015).

By path induction, we can define a family of comparison maps

$ \mathsf{isoeq}_{A}:\prod_{x,y:A}(x=_{A}y)\to\mathrm{iso}_{A}(x,y)$

via path induction by

$\mathsf{isoeq}_{A}(x,x,\textup{refl}_{x})\mathrel{\vcentcolon\equiv}(\mathsf{id}_{x},\mathsf{id}_{x},\textup{refl}_{\mathsf{id}_{x}},\mathsf{id}_{x},\textup{refl}_{\mathsf{id}_{x}}).$

###### Definition 3.3 (Rezk types; is-rezk).

A type $A$ is _Rezk_ or an _$\infty$ -category_ if it is Segal and Rezk-
complete:

$\mathsf{isRezk}(A)\mathrel{\vcentcolon\equiv}\mathsf{isSegal}(A)\times\prod_{x,y:A}\mathsf{isEquiv}\left(\mathsf{isoeq}_{A,x,y}\right).$

This synthetic definition semantically translates to the well-understood
notion of _complete Segal_ or _Rezk space_ , a model of $\infty$-category
(Rezk, 2001; Joyal and Tierney, 2007; Bergner, 2018; Rasekh, 2021).555More
generally, this yields Rezk _objects_ internal to a given $\infty$-topos by
(Riehl and Shulman, 2017; Shulman, 2019; Weinberger, 2022c), hence _internal_
$\infty$-categories (de Brito, 2016; Rasekh, 2022; Stenzel, 2023; Martini and
Wolf, 2023).

And also from an internal standpoint, the ensuing theory is quite rich. One
obtains notions of functors, natural transformations, functor categories,
adjunctions (Riehl and Shulman, 2017), (co-)limits (Bardomiano Martínez,
2022), and fibrations (Riehl and Shulman, 2017; Buchholtz and Weinberger,
2023; Weinberger, 2022b, d), with many parallels to Riehl–Verity’s _$\infty$
-cosmos theory_, a model-independent approach to $\infty$-category theory
(Riehl and Verity, 2022).

#### Naturality for free

A useful feature of the synthetic theory is that various functoriality and
naturality properties are automatically satisfied. This saves a lot of work
compared to set-theoretic foundations. For instance, given Segal types $A$ and
$B$ any type-theoretic function $f:A\to B$ turns out to be a functor, _i.e._ ,
preserves compositions and identity, up to propositional equality, see
(functors-pres-id) and (functors-pres-comp).666Semantically, this can be seen
as the fact that any morphism between simplicial objects automatically
preserves composition if they happen to be Segal. In particular, we do not
have to specify object and morphism part separately. Similarly, given functors
$f,g:A\to B$, natural transformations may be defined, using the formalism of
extension types, to be arrows $\varphi:\underset{A\to B}{\hom}(f,g)$ (nat-
trans). This definition automatically yields the expected naturality squares
without having to specify them, (Riehl and Shulman, 2017, Proposition 6.6).

Further instances of automatic naturality appear in §3.2 and 5.

###  3.2. Covariant families of discrete types

#### Discrete types (07-discrete)

We are also interested in synthetic $\infty$-groupoids, meaning
$\infty$-categories where every arrow is invertible.777As shown in (Riehl and
Shulman, 2017, Section 7), one can drop the Rezkness assumption. E.g., one can
show that for any Segal type $A$, the hom types $\hom_{A}(x,y)$ are
necessarily discrete. This matches up with the traditional theory and the
intuition that $\infty$-categories are (weakly enriched) in _spaces_ as
modeled by $\infty$-groupoids (Quillen, 2006).

The groupoidal condition can be understood as a kind of _discreteness
condition_. To make it precise, we need a comparison of paths with arrows,
similarly to our treatment of Rezk completeness, cf. Section 3.1. Namely, for
a type $A$ we define

$ \mathsf{arreq}_{A}:\prod_{x,y:A}(x=_{A}y)\to\hom_{A}(x,y)$

via path induction by

$\mathsf{arreq}_{A}(x,x,\textup{refl}_{x})\mathrel{\vcentcolon\equiv}\mathsf{id}_{x}.$

###### Definition 3.4 (Discrete types; is-discrete).

A type $A$ is _discrete_ or an _$\infty$ -groupoid_ if

$
\mathsf{isDiscrete}(A)\mathrel{\vcentcolon\equiv}\prod_{x,y:A}\mathsf{isEquiv}(\mathsf{arreq}_{A,x,y}).$

This definition also yields the desired notion in the Segal object models
(Bousfield, 1992; Stenzel, 2022).

${{\sum_{a:A}C(a)}}$${u}$${{f_{*}(u)}}$${A}$${x}$${y}$$\scriptstyle{f}$$\scriptstyle{\mathrm{lift}_{C,f}(u)}$
Figure 3. A covariant family $C:A\to\mathcal{U}$

#### Covariant families (08-covariant)

The $\infty$-categorical Yoneda lemma deals with families or _fibrations_ of
discrete types indexed by a Segal type. These families $C:A\to\mathcal{U}$ are
supposed to be _functorial_ in the sense that an arrow $f:\hom_{A}(x,y)$ in
the base $A$ should give a functor
$f_{*}\mathrel{\vcentcolon\equiv}\mathsf{trans}_{C,f}:C(x)\to C(y)$ between
the fibers.

This is achieved by the notion of _covariant family_ , corresponding to what
semantically is often called _left fibration_ , after (Joyal, 2008, §8) and
(Lurie, 2009, Section 2.1), see also (Kazhdan and Varshavsky, 2014; Heuts and
Moerdijk, 2015; Ayala and Francis, 2020; Barwick and Shah, 2018; Rasekh,
2023b; Riehl and Verity, 2017; Cisinski, 2019).

To define it, we have to introduce a _dependent_ version of the hom type,
capturing arrows in the total type $\sum_{x:A}C(x)$ that get mapped to a
prescribed arrow in the base. This can, once again, conveniently be formulated
using extension types.

###### Definition 3.5 (Dependent hom; dhom).

Let $C:A\to\mathcal{U}$ be a type family. For elements $x,y:A$, let
$f:\hom_{A}(x,y)$ be an arrow. For elements in the fibers $u:C(x)$ and
$v:C(y)$, the corresponding _dependent hom type_ from $u$ to $v$ is given by
the extension type

$\textup{dhom}_{C(f)}(u,v)\mathrel{\vcentcolon\equiv}\left\langle\mathchoice{\textstyle\prod_{t:\Delta^{1}}}{\textstyle\prod_{t:\Delta^{1}}}{\scriptstyle\prod_{t:\Delta^{1}}}{\scriptscriptstyle\prod_{t:\Delta^{1}}}C(f(t))\middle|^{\partial\Delta^{1}}_{[u,v]}\right\rangle.$

The defining property for a covariant family $C:A\to\mathcal{U}$ says that we
can lift an arrow $f:\hom_{A}(x,y)$ in the base, given a point $u:C(x)$ in the
fiber over its source, to a dependent arrow

(covariant-transport) $\mathsf{lift}_{C,f,u}:\textup{dhom}_{C(f)}(u,f_{*}u)$

lying over $f$, and more so, uniquely up to homotopy, cf. Figure 3.

###### Definition 3.6 (Covariant family; is-covariant).

Let $C:A\to\mathcal{U}$ be a type family. We say $C$ is _covariant_ if the
following proposition is inhabited:

$\prod_{x,y:A}\prod_{f:\hom_{A}(x,y)}\prod_{u:C(x)}\mathsf{isContr}\left(\sum_{v:C(y)}\textup{dhom}_{C(f)}(u,v)\right)$

As shown in (Riehl and Shulman, 2017, Section 8), it turns out that, over a
Segal type $A$, covariant families $C:A\to\mathcal{U}$ behave in the expected
ways. Namely, the fibers are all discrete (Riehl and Shulman, 2017,
Proposition 8.18), and they are _functorial_ in the following sense: for
elements $x,y,z:A$, morphisms $f:\hom_{A}(x,y)$, $g:\hom_{A}(y,z)$, and an
element in the fiber $u:C(x)$, we get identifications

$g_{*}(f_{*}u)=(g\circ f)_{*}u\;\text{and}\;(\mathsf{id}_{x})_{*}u=u,$

see (Riehl and Shulman, 2017, Proposition 8.16).

A fundamental example are the _representable_ covariant families of the form
$\hom_{A}(x,-):A\to\mathcal{U}$, for $x:A$, when $A$ is Segal (is-segal-
representable-is-covariant).

Furthermore, between covariant families $C,D:A\to\mathcal{U}$, a fiberwise map
$\varphi:\prod_{x:A}C(x)\to D(x)$ is automatically _natural_ : for any arrow
$f:\hom_{A}(x,y)$ and element $u:C(x)$ we have an identification

(naturality-covariant-fiberwise-transformation)
$f_{*}(\varphi_{x}(u))=\varphi_{y}(f_{*}u).$

##  4\. The Rzk proof assistant

Kudasov has implemented Rzk, the first proof assistant to support simplicial
type theory. In our work since the spring of 2023, we have been developing a
library for Rzk, formalizing a range of result from Riehl–Shulman’s work
(Riehl and Shulman, 2017), and in addition to that also the required results
from standard homotopy type theory (Univalent Foundations Program, 2013;
Rijke, 2022). The formalizations in this paper have been written for and
checked with Rzk version 0.5.4.

Syntax of the formalized code in Rzk is very close to the underlying theory,
allowing for easy correspondence between statements in the code and on paper.
However, proofs in Rzk may appear too detailed sometimes, since, being
experimental, Rzk has not yet evolved enough syntactic sugar or tools like
implicit parameters, tactics, or type classes to simplify proof construction.

###  4.1. Key features of Rzk

The kernel of Rzk provides the following primitive notions and capabilities.

#### The universes

There are three fixed universes: TOPE of topes, and , CUBE, which is also
present, for example, in the UniMath library (Voevodsky et al., [n. d.]) We
consider such simplification acceptable for the time being and hope that Rzk
will evolve proper universes in the future.

#### Tope logic

This includes both cubes and topes. Rzk has built-in unit cube 2 (with points
02 : 2 and RiehlShulman2017, and the inequality tope RiehlShulman2017; curry-
uncurry). Rzk offers full automation of the tope layer which helps keep the
Rzk syntax and proofs simpler and automatically locate coherence issues in
proof terms.

#### Dependent types

Rzk offers basic support for dependent functions $\Sigma$ (x : A), B x, and
identity types x = y and x =_A y and induces more explicit and verbose proof
terms.

#### Extension types

Rzk offers two separate concepts that result in support for extension types.
First, Rzk allows dependent functions to have a cube or a shape (a cube
restricted with a tope) argument. These correspond to extension types
restricted to $\mathsf{rec}_{\bot}$ at the empty tope $\bot$. Second, any type
is allowed to have a “refinement,” specifying values for arbitrary tope
constraints. For example, a type A such that values of this type are
_computationally_ equal to $\phi$ holds and to $\psi$ holds. Of course, y must
agree when A is considered equivalent to , removing the need for explicit type
coercions. Combining functions depending on shapes with such refinements
yields extension types. For instance,
$\hom_{A}(a,b)\mathrel{\vcentcolon\equiv}\left\langle\Delta^{1}\to
A\middle|^{\partial\Delta^{1}}_{[a,b]}\right\rangle$ (hom) is defined as
follows:

⬇

#def hom (A : U) (x y : A) : U

:= (t : Δ¹) → A [t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y]

#### Sections and variables

Rzk supports Coq-style sections,888https://rzk-
lang.github.io/rzk/v0.5.4/reference/sections.rzk/ allowing for locally defined
assumptions (variables) which are automatically added as parameters to
definitions that use them. Importantly, Rzk features a mechanism for detecting
implicitly used assumptions to avoid accidental circular reasoning in
definitions. To ensure that such an implicit assumption is not accidental, Rzk
has the simplicial-hott/09-yoneda.rzkyoneda-lemma) itself is specified in a
way that makes explicit the use of function extensionality (mintedrzk #def
yoneda-lemma uses (funext) ( A : U) ( is-segal-A : is-segal A) ( a : A) ( C :
A → U) ( is-covariant-C : is-covariant A C) : is-equiv ((z : A) → hom A a z →
C z) (C a) (evid A a C) := … We find this particularly useful for readability,
highlighting the use of axioms or other assumptions (e.g. that a certain type
is Segal).

##  5\. The $\infty$-categorical Yoneda lemma in Rzk

#### The statement

In $1$-category theory, the Yoneda lemma says the following. Given a category
$\mathbb{A}$ and a _copresheaf 999Our formalization considers the covariant
case as well as the dual contravariant case. on $\mathbb{A}$_, _i.e._ , a
functor $C:\mathbb{A}\to\mathcal{S}\textup{{et}}$, for any
$a\in\textup{ob}(\mathbb{A})$ there is a bijection

$ \hom_{[\mathbb{A},\mathcal{S}\textup{{et}}]}(\hom_{\mathbb{A}}(a,-),C)\cong
C(a)$

mapping a natural transformation $\alpha$ to $\alpha(a,\mathsf{id}_{a})\in
C(a)$, naturally in both $C$ and $a$. In the $\infty$-categorical setting,
sets get replaced by $\infty$-groupoids. Copresheaves are modeled by left
fibrations _aka_ covariant families. Accordingly, the synthetic
$\infty$-categorical Yoneda lemma reads as follows.

###### Theorem 5.1 (Yoneda-lemma).

Let $C:A\to\mathcal{U}$ be a covariant family over a Segal type $A$. Then, for
any $a:A$ the map

$\mathsf{evid}_{A,a,C}:\left(\prod_{z:A}\hom_{A}(a,z)\to C(z)\right)\to C(a)$

defined by

$
\mathsf{evid}_{A,a,C}(\varphi)\mathrel{\vcentcolon\equiv}\varphi(a,\mathsf{id}_{a})$

is an equivalence.

Note this result holds for pre-$\infty$-categories, not just
$\infty$-categories. For semantical accounts of the $\infty$-categorical
Yoneda lemma see e.g. (Kazhdan and Varshavsky, 2014; Rasekh, 2023b; Riehl and
Verity, 2017; Martini, 2021), and (Riehl and Verity, 2022, Chapter 5).

#### The proof

An inverse map is constructed using the covariant transport of $C$. Namely, we
define

$\mathsf{yon}_{A,a,C}:C(a)\to\left(\prod_{z:A}\hom_{A}(a,z)\to C(z)\right)$

by

(yon) $\mathsf{yon}_{A,a,C}(u)\mathrel{\vcentcolon\equiv}\lambda x.\lambda
f.f_{*}u.$

In the $1$-categorical Yoneda lemma, a crucial part of the work is to show
that the terms $\mathsf{yon}_{A,a,C}(u)$ defined by the inverse map are
actually morphisms of presheaves, _i.e._ , natural transformations. In our
setting, this is, in fact, an automatic consequence from both $C$ and
$\hom_{A}(a,-):A\to\mathcal{U}$ being covariant. In the formalization
considerable work goes into showing a type $A$ is Segal if and only if the
type families $\hom_{A}(a,-)$ are covariant; for the implication relevant
here, see (is-segal-representable-is-covariant). In more detail, if $A$ is a
Segal type, $a:A$, and $C:A\to\mathcal{U}$ is a covariant family, let
$\varphi:\prod_{z:A}\hom_{A}(a,z)\to C(z)$ be a family of maps. Then for any
$x,y:A$ and arrows $f:\hom_{A}(a,x)$ and $g:\hom_{A}(x,y)$, we have

(1) $g_{*}(\varphi(x,f))=\varphi(y,g\circ f)$

as a special case of

$ {\eqref{eq:fam-maps-cov-is-nat}}.$

For the Yoneda lemma, one has to show that the two composites of
$\mathsf{evid}_{A,a,C}$ and $\mathsf{yon}_{A,a,C}$ yield identities. The
direction $\mathsf{evid}_{A,a,C}\circ\mathsf{yon}_{A,a,C}=\mathsf{id}$ is
rather easy to see. Using function extensionality, we can check this
pointwise. For $u:C(a)$ we have to produce an identification

$(\lambda x.\lambda f.f_{*}u)(a,\mathsf{id}_{a})=u.$

But the left-hand side evaluates to $(\lambda x.\lambda
f.f_{*}u)(a,\mathsf{id}_{a})=(\mathsf{id}_{a})_{*}(u)$, and the claim follows
by concatenating with the path
$(\mathsf{id}_{a})_{*}(u)=\mathsf{id}_{C(a)}(u)$ given by the fact covariant
transport of identities gives the identity functor of the fiber. For the other
direction, the main work is giving homotopies

$\displaystyle\mathsf{yon}_{A,a,C}(\mathsf{evid}_{A,a,C}(\varphi))(x,f)=\varphi(x,f).$

for all $\varphi:\prod_{z:A}\hom_{A}(a,z)\to C(z)$, $x:A$, and
$f:\hom_{A}(a,x)$. We first get a path
$f_{*}(\varphi(a,\mathsf{id}_{a}))=\varphi(x,f\circ\mathsf{id}_{a})$, again by
naturality (1). Then, using action on paths on the canonical identification
$f\circ\mathsf{id}_{a}=f$ gives
$\varphi(x,f\circ\mathsf{id}_{a})=\varphi(x,f)$, and we are done. We now have
to abstract over evaluating at $x$ and $f$ using function extensionality
twice, which ultimately yields the desired identification
$(\mathsf{yon}_{A,a,C}\circ\mathsf{evid}_{A,a,C})(\varphi)=\varphi$, between
fibered maps of type $\prod_{z:A}\hom_{A}(a,z)\to C(z)$. This concludes the
proof of the Yoneda lemma.

#### The dependent Yoneda lemma

The Yoneda lemma of Theorem 5.1 is some sort of “arrow-induction” principle,
but is not expressed in fully dependent form. This inspired the authors of
(Riehl and Shulman, 2017) to search for a dependent generalization, proving a
theorem that had not been previously known for $\infty$-categories.111111There
is a version of the dependent Yoneda lemma appearing in (Riehl and Verity,
2022, Chapter 5), but this was proven subsequently. From the _dependent Yoneda
lemma_ , the “absolute” version (yoneda-lemma) can be derived.

###### Theorem 5.2 (dependent-yoneda-lemma).

Let $A$ be a Segal type, $a:A$, and
$C:\left(\sum_{x:A}\hom_{A}(a,x)\right)\to\mathcal{U}$ be a covariant family.
Then the map

$\mathsf{devid}_{A,a,C}:\left(\prod_{z:A}\prod_{f:\hom_{A}(a,z)}C(z,f)\right)\to
C(a)$

defined by

$
\mathsf{devid}_{A,a,C}(\varphi)\mathrel{\vcentcolon\equiv}\varphi(a,\mathsf{id}_{a})$

is an equivalence.

Note that 5.2 is reminiscent of the path induction principle, cf. Section 2.1,
and hence it can be seen as a _directed arrow induction principle_.

##  6\. Comparing the $\infty$\- vs 1-categorical Yoneda lemmas

A fundamental advantage of the synthetic framework for $\infty$-category is
that it narrows the gap between $\infty$-category theory and 1-category
theory, by moving much of the complexity inherent in homotopy coherent
mathematics into the background foundation system. We can see this by
comparing the formalization of the Yoneda lemma for $\infty$-categories in Rzk
with the formalization of the Yoneda lemma for 1-categories in other proof
assistants. As part of this project, we contributed a formalization of the
Yoneda lemma for precategories to the agda-unimath
library,121212https://unimath.github.io/agda-unimath/category-theory.yoneda-
lemma-precategories.html which describes itself as a “community-driven effort
aimed at formalizing mathematics from a univalent point of view.” This library
contains notions of _precategories_ and _categories_ , which parallel our
pre-$\infty$-categories and $\infty$-categories, except their hom-types are
sets, as is appropriate to 1-category theory. Both proofs follow the same
outline, proving that (evid) is an equivalence by constructing a two-sided
inverse. A point of difference in the agda-unimath proof is that the data of
the inverse involves both the function (yon) together with a proof of its
naturality. As with our proof in Rzk, one of the composites is directly
identifiable with the identity, while the other requires a calculation
together with two instances of function extensionality. Other differences
arise from the varying ways that categorical data is encoded in Rzk vs agda-
unimath. There, precategories are types with additional structure while here
pre-$\infty$-categories are types satisfying a property. There, representables
are encoded as functors valued in the precategory of sets, while here
representables are encoded as covariant type families. These differences have
more of an effect on the syntax of the proof than its structural content. At
our request, Sina Hazratpour wrote a Lean formalization of the 1-categorical
Yoneda lemma, first as a self-contained formalization in Lean
3,131313https://github.com/sinhp/CovariantYonedaLean3 with the proof of the
Yoneda lemma later updated to Lean
4.141414https://github.com/sinhp/CovariantYonedaLean4 Formal proofs in Lean
are quite different than formal proofs in Rzk or in Agda because of the use of
automation tactics in the interactive theorem proving mode, allowing the user
to rewrite along known identifications or “simplify” the goal using known
lemmas. In addition, Lean’s use of type classes and automatic instance
inference simplifies the syntax in the statement of the Yoneda lemma, as
compared with the agda-unimath proof. In the Lean 3 proof, the naturality of
(yon) must again be checked explicitly via a proof that involves unfolding the
definition of the representable functor and using the fact that functors
preserve composition. The remainder of the proof proceeds as before.
Interestingly, in the Lean 4 proof, Hazratpour proves a lemma — (1) in the
case where $f$ is $\mathsf{id}_{a}$ — and then feeds it to the tactic
aesop_cat,151515Aesop (Automated Extensible Search for Obvious Proofs) is a
proof search tactic for Lean 4; see https://github.com/JLimperg/aesop which
then automatically verifies the naturality of (yon) and checks that the Yoneda
maps are inverses. Other formalizations of the 1-categorical Yoneda lemma
appear in
UniMath161616https://github.com/UniMath/UniMath/blob/7d7fb997dbe84b0d0107adc963281c6efb97ff60/UniMath/CategoryTheory/yoneda.v#L325-L328
(Voevodsky et al., [n. d.]) and mathlib.171717https://leanprover-
community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Yoneda.html#CategoryTheory.yoneda

##  7\. Conclusions and future work

The formalization process led us to discover a mistake in the paper (Riehl and
Shulman, 2017): the published proof of the “only if” direction of Proposition
8.13 employed circular reasoning.181818While this mistake could have been
caught by the original authors, the process of formalization made it entirely
transparent: a proof of the conclusion was called as a hypothesis by one of
the lemmas cited in the original argument. Fortunately, the stated result
remains true. Our new formalized proof (is-segal-is-covariant-representable)
now appears in (Riehl and Shulman, 2023). We hope that the Rzk proof assistant
will provide a tool that may make $\infty$-category theory easier to learn. To
that end we invite new collaborators to help us formalize other results from
$\infty$-category theory, a few of which we now describe.

###  7.1. Adjunctions

One application of the dependent Yoneda lemma is to the theory of adjunctions
between $\infty$-categories. The standard logically equivalent definitions of
an adjunction are encoded by various types that define a _transposing
adjunction_ , _half-adjoint diagrammatic adjunction_ , or a _bidiagrammatic
adjunction_. We plan to formalize these notions and prove the equivalences
established in (Riehl and Shulman, 2017, §11).

###  7.2. The cocartesian $\infty$-categorical Yoneda lemma

As a future endeavor, it is desirable to extend the existing fibrational
theory from $\infty$-groupoid-valued functorial families to $\infty$-category-
valued functorial families. Building on the semantical theory of
(co-)cartesian fibrations (Joyal, 2008; Lurie, 2009; Ayala and Francis, 2020;
Barwick and Shah, 2018; Riehl and Verity, 2017, 2022; Rasekh, 2023a; Martini,
2022) these so-called _(co-)cartesian families_ have been studied in the
synthetic setting of simplicial type theory in (Buchholtz and Weinberger,
2023; Weinberger, 2022a). Cocartesian fibrations play a crucial role when
computing limits of $\infty$-categories (Lurie, 2009, Subsection 3.3.3),
studying moduli spaces in geometry (Lurie, 2018, Chapter 1), and higher
algebraic objects such as symmetric monoidal $\infty$-categories (Lurie, 2017,
Definition 2.1.2.13). A central theorem is the (co-)cartesian Yoneda lemma,
cf. (Riehl and Verity, 2022, Section 5.7). It reads similar to the version of
the discrete Yoneda Lemma discussed in 5: given a _cocartesian_ family
$C:A\to\mathcal{U}$ over a Rezk type $A$ (all of whose fibers are also Rezk),
we want to classify families of functions $\prod_{x:A}\hom_{A}(a,x)\to C(x)$,
for a fixed element $a:A$. However, we will have to restrict to the type
$\prod_{(x,f):\sum_{y:A}\hom_{A}(a,y)}^{\mathrm{cocart}}C(x)$ of sections
$\sigma$ such that for every $x^{\prime}:A$,
$f^{\prime}:\hom_{A}(a,x^{\prime})$, and $g:\hom_{A}(x,x^{\prime})$ with
$g\circ f=f^{\prime}$ the dependent morphism $\sigma(g)$ is what is called a
_cocartesian arrow_ , _i.e._ , satisfies a certain initiality property (is-
cocartesian-arrow). A family $C:A\to\mathcal{U}$ whose total type is Rezk (as
well as all its fibers) is cocartesian exactly if it admits enough lifts of
arrows in the base $A$ to a cocartesian dependent arrow (is-cocartesian-
family). The cocartesian Yoneda lemma then states that the evaluation map

$\mathsf{evid}^{C}_{a}:\left(\prod_{(x,f):\sum_{y:A}\hom_{A}(a,y)}^{\mathrm{cocart}}C(x)\right)\to
C(a)$

is an equivalence. The _dependent version_ of this theorem, semantically
established by Riehl–Verity in (Riehl and Verity, 2022, Theorem 5.7.2.), can,
again, be seen as a (one-sided) _directed arrow induction principle_ ,
analogous to the well-known path induction principle for the identity types in
standard Martin-Löf type theory. Efforts in the direction of formalizing
Buchholtz–Weinberger’s proof of the cocartesian Yoneda lemma from (Buchholtz
and Weinberger, 2023, Section 7) in Rzk are under way, but will require
formalizing if not all then at least some of the preliminary structural
properties and operations for cocartesian families from (Buchholtz and
Weinberger, 2023, Section 5).

###  7.3. Limits and colimits

In (Bardomiano Martínez, 2022), Bardomiano Martínez introduces limits and
colimits of diagrams valued in Segal types and proves that right adjoints
between Segal types preserve limits. We would like to formalize his results
and explore further developments of the theory of limits and colimits.

###  7.4. Improvements to Rzk

We note a few improvements for Rzk that would positively affect this and
future formalization projects. First, supporting term inference and implicit
arguments would help reduce the size of formalizations and, consequently,
assist with readability. Second, the current implementation lacks incremental
typechecking and proper module support, which makes the feedback on changes
less immediate. Finally, while a minimal integration with an IDE
exists,191919there is a VS Code extension for Rzk at https://github.com/rzk-
lang/vscode-rzk it still has to acquire proper language server support. We
note also that Rzk’s experimental diagram rendering feature202020https://rzk-
lang.github.io/rzk/v0.5.4/reference/render.rzk/ (which is useful on small
examples) could be extended further to assist with visualizations (or even
interactive capabilities) for statements and constructions in simplicial type
theory.

###  7.5. Extensions of simplicial type theory

The simplicial type theory is not sufficiently powerful to prove all results
of $\infty$-category theory contained for instance in (Lurie, 2009). A longer
range goal would be to further extend this synthetic framework by including
directed higher inductive types to freely generate $\infty$-categories,
universes to classify covariant fibrations and cocartesian fibrations, and
modalities for opposite $\infty$-categories and the $\infty$-groupoid core as
outlined in (Buchholtz and Weinberger, 2019); see also (Shulman, 2018; Myers
and Riley, 2023; North, 2019; Gratzer et al., 2020; Aagaard et al., 2022;
Licata et al., 2017, 2018). If such theoretical developments were paired with
experimental extensions to Rzk, that would greatly aid the process of
exploring the expanded formal system.

###### Acknowledgements.

The authors are very grateful to Benedikt Ahrens, who first suggested the
project of creating a proof assistant for the simplicial type theory. Fredrik
Bakke contributed formalizations concerning the 2-category of Segal types and
made invaluable improvements to the professionalization of the repository,
drafting a style guide, overseeing its implementation, and suggesting
improvements to our github workflow. Sina Hazratpour produced a formalized
proof of the 1-categorical Yoneda lemma in Lean to provide a useful direct
comparison. Abdelrahman Abounegm has contributed an Rzk
plugin212121https://github.com/rzk-lang/mkdocs-plugin-rzk for MkDocs allowing
for hyperlinks to the syntax-highlighted code used in this paper.

## References

  * (1)
  * Aagaard et al. (2022) Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, and Lars Birkedal. 2022\.  Unifying cubical and multimodal type theory.  (2022).  arXiv:2203.13000
  * Ahrens et al. (2015) Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. 2015\.  Univalent categories and the Rezk completion.  _Mathematical Structures in Computer Science_ 25, 5 (2015), 1010–1039.  https://doi.org/10.1017/S0960129514000486
  * Ahrens et al. (2022) Benedikt Ahrens, Paige Randall North, and Niels van der Weide. 2022.  Semantics for Two-Dimensional Type Theory. In _Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science_ (Haifa, Israel) _(LICS ’22)_. Association for Computing Machinery, New York, NY, USA, Article 12, 14 pages.  https://doi.org/10.1145/3531130.3533334
  * Allioux et al. (2021) Antoine Allioux, Eric Finster, and Matthieu Sozeau. 2021\.  Types are Internal $\infty$-Groupoids.  arXiv:2105.00024 [cs.LO]
  * Angiuli et al. (2021) Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou, and Daniel R Licata. 2021.  Syntax and models of Cartesian cubical type theory.  _Mathematical Structures in Computer Science_ 31, 4 (2021), 424–468.  https://doi.org/10.1017/S0960129521000347
  * Annenkov et al. (2023) Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. 2023.  Two-level type theory and applications.  _Mathematical Structures in Computer Science_ (may 2023), 1–56.  https://doi.org/10.1017/s0960129523000130
  * Awodey and Warren (2009) Steve Awodey and Michael A Warren. 2009.  Homotopy theoretic models of identity types. In _Mathematical proceedings of the cambridge philosophical society_ , Vol. 146. Cambridge University Press, 45–55.  https://doi.org/10.1017/S0305004108001783
  * Ayala and Francis (2020) David Ayala and John Francis. 2020.  Fibrations of $\infty$-categories.  _Higher Structures_ 4 (2020), 168–265.  Issue 1. https://higher-structures.math.cas.cz/api/files/issues/Vol4Iss1/AyalaFrancis
  * Ayala et al. (2022) David Ayala, Aaron Mazel-Gee, and Nick Rozenblyum. 2022\.  Stratified noncommutative geometry.  arXiv:1910.14602 [math.AG]
  * Bakke (2021) Fredrik Bakke. 2021\.  _Segal Spaces in Homotopy Type Theory_.  Master’s thesis. NTNU.  https://ntnuopen.ntnu.no/ntnu-xmlui/handle/11250/2995704
  * Bardomiano Martínez (2022) César Bardomiano Martínez. 2022\.  Limits and colimits of synthetic $\infty$-categories.  arXiv:2202.12386 [math.CT]
  * Barwick and Shah (2018) Clark Barwick and Jay Shah. 2018.  Fibrations in $\infty$-category theory.  _2016 MATRIX annals_ (2018), 17–42.  https://www.matrix-inst.org.au/wp_Matrix2016/wp-content/uploads/2017/08/BarwickShah.pdf
  * Benjamin et al. (2021) Thibaut Benjamin, Eric Finster, and Samuel Mimram. 2021\.  Globular weak $omega$-categories as models of a type theory.  _CoRR_ abs/2106.04475 (2021).  arXiv:2106.04475
  * Bergner (2018) Julia E Bergner. 2018\.  _The homotopy theory of $(\infty,1)$-categories_. Vol. 90.  Cambridge University Press.  https://doi.org/10.1017/9781316181874
  * Bertot and Castéran (2013) Yves Bertot and Pierre Castéran. 2013.  _Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions_.  Springer Science & Business Media.  https://doi.org/10.1093/comjnl/bxh141
  * Bezem et al. (2014) Marc Bezem, Thierry Coquand, and Simon Huber. 2014\.  A Model of Type Theory in Cubical Sets. In _19th International Conference on Types for Proofs and Programs (TYPES 2013)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 26)_ , Ralph Matthes and Aleksy Schubert (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 107–128.  https://doi.org/10.4230/LIPIcs.TYPES.2013.107
  * Blumberg et al. (2013) Andrew J Blumberg, David Gepner, and Gonçalo Tabuada. 2013\.  A universal characterization of higher algebraic $K$-theory.  _Geometry & Topology_ 17, 2 (2013), 733–838.  10.2140/gt.2013.17.733
  * Boardman and Vogt (1973) John Michael Boardman and Rainer M Vogt. 1973.  _Homotopy invariant algebraic structures on topological spaces_. Lecture Notes in Mathematics, Vol. 347.  Springer.  https://doi.org/10.1007/BFb0068547
  * Bordg and Doña Mateo (2023) Anthony Bordg and Adrián Doña Mateo. 2023\.  Encoding Dependently-Typed Constructions into Simple Type Theory. In _Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs_ (Boston, MA, USA) _(CPP 2023)_. Association for Computing Machinery, New York, NY, USA, 78–89.  https://doi.org/10.1145/3573105.3575679
  * Bousfield (1992) Aldridge K. Bousfield. 1992\.  The simplicial homotopy theory of iterated loop spaces.  Typed notes by Julie Bergner.
  * Bove et al. (2009) Ana Bove, Peter Dybjer, and Ulf Norell. 2009.  A brief overview of Agda–a functional language with dependent types. In _Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22_. Springer, 73–78.  https://doi.org/10.1007/978-3-642-03359-9_6
  * Brady (2013) Edwin Brady. 2013\.  Idris, a general-purpose dependently typed programming language: Design and implementation.  _Journal of functional programming_ 23, 5 (2013), 552–593.  https://doi.org/10.1017/S095679681300018X
  * Buchholtz (2019) Ulrik Buchholtz. 2019\.  _Higher Structures in Homotopy Type Theory_.  Springer International Publishing, Cham, 151–172.  https://doi.org/10.1007/978-3-030-15655-8_7
  * Buchholtz and Weinberger (2019) Ulrik Buchholtz and Jonathan Weinberger. 2019.  Type-theoretic Modalities for Synthetic $(\infty,1)$-Categories.  https://hott.github.io/HoTT-2019//conf-slides/Weinberger.pdf Talk at HoTT 2019 Conference at CMU, Pittsburgh, CA.
  * Buchholtz and Weinberger (2023) Ulrik Buchholtz and Jonathan Weinberger. 2023.  Synthetic fibered $(\infty,1)$-category theory.  _Higher Structures_ 7 (2023), 74–165.  Issue 1. https://doi.org/10.21136/HS.2023.04
  * Camarena (2013) Omar Antolın Camarena. 2013\.  A whirlwind tour of the world of $(\infty,1)$-categories.  _Mexican mathematicians abroad: recent contributions_ 657 (2013), 15–61.  https://www.matem.unam.mx/~omar/papers/infinity-survey.pdf
  * Cavallo et al. (2020) Evan Cavallo, Anders Mörtberg, and Andrew W Swan. 2020\.  Unifying Cubical Models of Univalent Type Theory. In _28th EACSL Annual Conference on Computer Science Logic (CSL 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 152)_ , Maribel Fernández and Anca Muscholl (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 14:1–14:17.  https://doi.org/10.4230/LIPIcs.CSL.2020.14
  * Cherubini (2022) Felix Cherubini. 2022\.  Cartan Geometry in Modal Homotopy Type Theory.  arXiv:1806.05966 [math.DG]
  * Cisinski (2019) Denis-Charles Cisinski. 2019\.  _Higher categories and homotopical algebra_. Vol. 180.  Cambridge University Press.
  * Cohen et al. (2018) Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018.  Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In _21st International Conference on Types for Proofs and Programs (TYPES 2015)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 69)_ , Tarmo Uustalu (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5:1–5:34.  https://doi.org/10.4230/LIPIcs.TYPES.2015.5
  * de Brito (2016) Pedro Boavida de Brito. 2016\.  Segal objects and the Grothendieck construction.  (2016).  arXiv:1605.00706 [math.AT]
  * de Moura et al. (2015) Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015.  The Lean theorem prover (system description). In _Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25_. Springer, 378–388.  https://doi.org/10.1007/978-3-319-21401-6_26
  * de Moura and Ullrich (2021) Leonardo de Moura and Sebastian Ullrich. 2021.  The Lean 4 theorem prover and programming language. In _Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28_. Springer, 625–635.  https://doi.org/10.1007/978-3-030-79876-5_37
  * Dean (2020) Christopher J. Dean. 2020\.  Globular Multicategories with Homomorphism Types.  arXiv:2005.14104 [math.CT]
  * Fargues and Scholze (2021) Laurent Fargues and Peter Scholze. 2021.  Geometrization of the local Langlands correspondence.  arXiv:2102.13459 [math.RT]
  * Finster and Mimram (2017) Eric Finster and Samuel Mimram. 2017.  A type-theoretical definition of weak $\omega$-categories. In _2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_. IEEE, 1–12.  https://doi.org/10.1109/LICS.2017.8005124
  * Finster et al. (2022) Eric Finster, David Reutter, Jamie Vicary, and Alex Rice. 2022\.  A Type Theory for Strictly Unital $\infty$-Categories. In _Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science_ (Haifa, Israel) _(LICS ’22)_. Association for Computing Machinery, New York, NY, USA, Article 48, 12 pages.  https://doi.org/10.1145/3531130.3533363
  * Finster et al. (2021) Eric Finster, Alex Rice, and Jamie Vicary. 2021.  A Type Theory for Strictly Associative Infinity Categories.  arXiv:2109.01513 [math.CT]
  * Garner (2009) Richard Garner. 2009\.  Two-dimensional models of type theory.  _Mathematical Structures in Computer Science_ 19, 4 (2009), 687–736.  https://doi.org/10.1017/S0960129509007646
  * Gonthier et al. (2013) Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al. 2013\.  A machine-checked proof of the odd order theorem. In _International conference on interactive theorem proving_. Springer, 163–179.  https://doi.org/10.1007/978-3-642-39634-2_14
  * Gratzer et al. (2020) Daniel Gratzer, GA Kavvos, Andreas Nuyts, and Lars Birkedal. 2020.  Multimodal dependent type theory. In _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_. 492–506.
  * Grothendieck (1961) Alexander Grothendieck. 1961\.  Techniques de construction et théorèmes d’existence en géométrie algébrique III : préschémas quotients.  In _Séminaire Bourbaki : années 1960/61, exposés 205-222_. Number 6 in Séminaire Bourbaki. Société mathématique de France.  http://www.numdam.org/item/SB_1960-1961__6__99_0/ talk:212.
  * Hales et al. (2017) Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. 2017\.  A formal proof of the Kepler conjecture. In _Forum of mathematics, Pi_ , Vol. 5. Cambridge University Press, e2.  https://doi.org/10.1017/fmp.2017.1
  * Harrison (2009) John Harrison. 2009\.  HOL light: An overview. In _International Conference on Theorem Proving in Higher Order Logics_. Springer, 60–66.  https://doi.org/10.1007/978-3-642-03359-9_4
  * Heuts and Moerdijk (2015) Gijs Heuts and Ieke Moerdijk. 2015.  Left fibrations and homotopy colimits.  _Mathematische Zeitschrift_ 279, 3-4 (2015), 723–744.  https://doi.org/10.1007/s00209-014-1390-7
  * Hirschowitz and Simpson (2001) André Hirschowitz and Carlos Simpson. 2001.  Descente pour les $n$-champs (Descent for $n$-stacks).  arXiv:math/9807049 [math.AG]
  * Hofmann and Streicher (1998) Martin Hofmann and Thomas Streicher. 1998.  The groupoid interpretation of type theory.  _Twenty-five years of constructive type theory (Venice, 1995)_ 36 (1998), 83–111.  https://doi.org/10.1093/oso/9780198501275.003.0008
  * Joyal (2002) André Joyal. 2002\.  Quasi-categories and Kan complexes.  _Journal of Pure and Applied Algebra_ 175, 1-3 (2002), 207–222.  https://doi.org/10.1016/S0022-4049(02)00135-4
  * Joyal (2008) André Joyal. 2008\.  Notes on quasi-categories.  _preprint_ (2008).  https://www.math.uchicago.edu/~may/IMA/Joyal.pdf
  * Joyal and Tierney (2007) André Joyal and Myles Tierney. 2007.  Quasi-categories vs Segal spaces.  _Contemp. Math._ 431, 277-326 (2007), 10.  https://doi.org/10.1090/conm/431/08278
  * Kapulkin and Lumsdaine (2021) Krzysztof Kapulkin and Peter LeFanu Lumsdaine. 2021.  The simplicial model of Univalent Foundations (after Voevodsky).  _Journal of the European Mathematical Society_ 23, 6 (2021), 2071–2126.  https://doi.org/10.4171/JEMS/1050
  * Kazhdan and Varshavsky (2014) David Kazhdan and Yakov Varshavsky. 2014.  Yoneda Lemma for complete Segal spaces.  _Functional Analysis and Its Applications_ 48, 2 (April 2014), 81–106.  https://doi.org/10.1007/s10688-014-0050-3
  * Kraus (2021) Nicolai Kraus. 2021\.  Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT. In _2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_. 1–14.  https://doi.org/10.1109/LICS52264.2021.9470667
  * Kudasov ([n. d.]) Nikolai Kudasov. [n. d.].  Rzk.  https://github.com/rzk-lang/rzk An experimental proof assistant based on a type theory for synthetic $\infty$-categories.
  * Licata and Harper (2011) Daniel R. Licata and Robert Harper. 2011.  2-Dimensional Directed Type Theory.  _Electronic Notes in Theoretical Computer Science_ 276 (2011), 263–289.  https://doi.org/10.1016/j.entcs.2011.09.026 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).
  * Licata et al. (2018) Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018.  Internal Universes in Models of Homotopy Type Theory. In _3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108)_ , Hélène Kirchner (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 22:1–22:17.  https://doi.org/10.4230/LIPIcs.FSCD.2018.22
  * Licata et al. (2017) Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017\.  A Fibrational Framework for Substructural and Modal Logics. In _2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84)_ , Dale Miller (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 25:1–25:22.  https://doi.org/10.4230/LIPIcs.FSCD.2017.25
  * Lurie (2003) Jacob Lurie. 2003\.  On Infinity Topoi.  arXiv:math/0306109 [math.CT]
  * Lurie (2004) Jacob Lurie. 2004\.  _Derived algebraic geometry_.  Ph. D. Dissertation. Massachusetts Institute of Technology.  http://hdl.handle.net/1721.1/30144
  * Lurie (2009) Jacob Lurie. 2009\.  _Higher topos theory_.  Princeton University Press.  https://www.math.ias.edu/~lurie/papers/HTT.pdf
  * Lurie (2017) Jacob Lurie. 2017\.  Higher Algebra.  https://www.math.ias.edu/~lurie/papers/HA.pdf
  * Lurie (2018) Jacob Lurie. 2018\.  Spectral algebraic geometry.  (2018).  https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf Under construction.
  * Martin-Löf (1975) Per Martin-Löf. 1975\.  An intuitionistic theory of types: Predicative part.  In _Studies in Logic and the Foundations of Mathematics_. Vol. 80. Elsevier, 73–118.  https://doi.org/10.1016/S0049-237X(08)71945-1
  * Martini (2021) Louis Martini. 2021\.  Yoneda’s lemma for internal higher categories.  (2021).  arXiv:2103.17141
  * Martini (2022) Louis Martini. 2022\.  Cocartesian fibrations and straightening internal to an $\infty$-topos.  (2022).  arXiv:2204.00295
  * Martini and Wolf (2023) Louis Martini and Sebastian Wolf. 2023.  Internal higher topos theory.  arXiv:2303.06437 [math.CT]
  * mathlib Community (2020) The mathlib Community. 2020\.  The Lean Mathematical Library. In _Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs_ (New Orleans, LA, USA) _(CPP 2020)_. Association for Computing Machinery, New York, NY, USA, 367–381.  https://doi.org/10.1145/3372885.3373824
  * Myers (2021) David Jaz Myers. 2021\.  Modal Fracture of Higher Groups.  arXiv:2106.15390 [math.CT]
  * Myers (2022a) David Jaz Myers. 2022a.  Good Fibrations through the Modal Prism.  _Higher Structures_ 6 (2022), 212–255.  Issue 1. https://higher-structures.math.cas.cz/api/files/issues/Vol6Iss1/Myers
  * Myers (2022b) David Jaz Myers. 2022b.  Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory.  arXiv:2205.15887 [math.AT]
  * Myers and Riley (2023) David Jaz Myers and Mitchell Riley. 2023.  Commuting Cohesions.  arXiv:2301.13780 [math.CT]
  * Nadler and Tanaka (2020) David Nadler and Hiro Lee Tanaka. 2020.  A stable $\infty$-category of Lagrangian cobordisms.  _Advances in Mathematics_ 366 (2020), 107026.  https://www.sciencedirect.com/science/article/pii/S0001870820300517
  * New and Licata (2023) Max S. New and Daniel R. Licata. 2023.  A Formal Logic for Formal Category Theory. In _Foundations of Software Science and Computation Structures_ , Orna Kupferman and Pawel Sobocinski (Eds.). Springer Nature Switzerland, Cham, 113–134.  https://doi.org/10.1007/978-3-031-30829-1_6
  * Nipkow et al. (2002) Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002\.  _Isabelle/HOL: a proof assistant for higher-order logic_.  Springer.  https://doi.org/10.1007/3-540-45949-9
  * Norell and Chapman (2009) Ulf Norell and James Chapman. 2009.  Dependently typed programming in Agda. In _Proceedings of the 4th international workshop on Types in language design and implementation_. 1–2.  https://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
  * North (2019) Paige Randall North. 2019\.  Towards a Directed Homotopy Type Theory.  _Electronic Notes in Theoretical Computer Science_ 347 (2019), 223–239.  https://doi.org/doi.org/10.1016/j.entcs.2019.09.012 Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics.
  * Nuyts (2015) Andreas Nuyts. 2015\.  _Towards a directed homotopy type theory based on 4 kinds of variance_.  Master’s thesis. KU Leuven.  https://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf
  * Orton and Pitts (2018) Ian Orton and Andrew M Pitts. 2018.  Axioms for modelling cubical type theory in a topos.  _Logical Methods in Computer Science_ 14 (2018).  https://doi.org/10.4230/LIPIcs.CSL.2016.24
  * Pellissier (2002) Régis Pellissier. 2002\.  _Catégories enrichies faibles_.  Ph. D. Dissertation. Université Nice Sophia Antipolis.  arXiv:math/0308246 [math.AT]
  * Quillen (2006) Daniel G Quillen. 2006\.  _Homotopical algebra_. Vol. 43.  Springer.  https://doi.org/10.1007/BFb0097438
  * Rasekh (2021) Nima Rasekh. 2021\.  Quasi-categories vs. Segal spaces: Cartesian edition.  _Journal of Homotopy and Related Structures_ 16, 4 (2021), 563–604.  10.1007/s40062-021-00288-2
  * Rasekh (2022) Nima Rasekh. 2022\.  Cartesian fibrations and representability.  _Homology, Homotopy and Applications_ 24, 2 (2022), 135–161.  https://doi.org/10.4310/HHA.2022.v24.n2.a7
  * Rasekh (2023a) Nima Rasekh. 2023a.  Cartesian Fibrations of Complete Segal Spaces.  _Higher Structures_ 7 (2023), 40–73.  Issue 1. https://doi.org/10.21136/HS.2023.03
  * Rasekh (2023b) Nima Rasekh. 2023b.  Yoneda lemma for simplicial spaces.  _Applied Categorical Structures_ 31, 4 (2023), 27\.  https://doi.org/10.1007/s10485-023-09734-z
  * Rezk (2001) Charles Rezk. 2001\.  A model for the homotopy theory of homotopy theory.  _Trans. Amer. Math. Soc._ 353, 3 (2001), 973–1007.  https://www.jstor.org/stable/221843
  * Riehl (2023a) Emily Riehl. 2023a.  Could $\infty$-category theory be taught to undergraduates?  _Notices of the AMS_ (May 2023).  https://www.ams.org/journals/notices/202305/noti2692/noti2692.html
  * Riehl (2023b) Emily Riehl. 2023b.  Homotopy types are homotopy types.  https://emilyriehl.github.io/files/hopkins65.pdf Lecture notes for an invited talk to “A panorama of homotopy theory: a conference in honour of Mike Hopkins”, Oxford, UK.
  * Riehl (2023c) Emily Riehl. 2023c.  On the $\infty$-topos semantics of homotopy type theory.  arXiv:2212.06937 [math.CT]  Lecture notes for a mini-course at CIRM, Luminy, Feb 2022.
  * Riehl and Shulman (2017) Emily Riehl and Michael Shulman. 2017.  A type theory for synthetic $\infty$-categories.  _Higher Structures_ 1 (2017), 147–224.  Issue 1. https://higher-structures.math.cas.cz/api/files/issues/Vol1Iss1/RiehlShulman
  * Riehl and Shulman (2023) Emily Riehl and Michael Shulman. 2023.  A type theory for synthetic $\infty$-categories.  (2023).  arXiv:1705.07442v5 [math.CT]
  * Riehl and Verity (2017) Emily Riehl and Dominic Verity. 2017.  Fibrations and Yoneda’s lemma in an $\infty$-cosmos.  _Journal of Pure and Applied Algebra_ 221, 3 (2017), 499–564.  https://doi.org/10.1016/j.jpaa.2016.07.003
  * Riehl and Verity (2022) Emily Riehl and Dominic Verity. 2022.  _Elements of $\infty$-Category Theory_.  Cambridge University Press.  https://doi.org/10.1017/9781108936880
  * Rijke (2022) Egbert Rijke. 2022\.  _Introduction to Homotopy Type Theory_.  Cambridge University Press.  https://arxiv.org/abs/2212.11082 forthcoming.
  * Rijke et al. (2021) Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, et al. 2021\.  Univalent mathematics in Agda.  https://github.com/UniMath/agda-unimath/
  * Rijke et al. (2020) Egbert Rijke, Michael Shulman, and Bas Spitters. 2020\.  Modalities in homotopy type theory.  _Logical Methods in Computer Science_ 16 (2020).  https://doi.org/10.23638/LMCS-16(1:2)2020
  * Riley et al. (2021) Mitchell Riley, Eric Finster, and Daniel R. Licata. 2021\.  Synthetic Spectra via a Monadic and Comonadic Modality.  arXiv:2102.04099 [math.CT]
  * Scholze (2022) Peter Scholze. 2022\.  Liquid Tensor Experiment.  _Experimental Mathematics_ 31, 2 (2022), 349–354.  https://doi.org/10.1080/10586458.2021.1926016
  * Schreiber and Shulman (2014) Urs Schreiber and Michael Shulman. 2014.  Quantum Gauge Field Theory in Cohesive Homotopy Type Theory.  _Electronic Proceedings in Theoretical Computer Science_ 158 (jul 2014), 109–126.  https://doi.org/10.4204/eptcs.158.8
  * Segal (1968) Graeme Segal. 1968\.  Classifying spaces and spectral sequences.  _Publications Mathématiques de l’IHÉS_ 34 (1968), 105–112.  http://www.numdam.org/item/PMIHES_1968__34__105_0/
  * Shulman (2015) Michael Shulman. 2015\.  The univalence axiom for elegant Reedy presheaves.  _Homology, Homotopy and Applications_ 17 (2015), 81–106.  Issue 2. https://doi.org/10.4310/HHA.2015.v17.n2.a6
  * Shulman (2018) Michael Shulman. 2018\.  Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.  _Mathematical Structures in Computer Science_ 28, 6 (2018), 856–941.  https://doi.org/10.1017/S0960129517000147
  * Shulman (2019) Michael Shulman. 2019\.  All $(\infty,1)$-toposes have strict univalent universes.  arXiv:1904.07004 [math.AT]
  * Stenzel (2022) Raffael Stenzel. 2022\.  Bousfield-Segal spaces.  _Homology Homotopy Appl._ 24, 1 (2022), 217–243.  https://doi.org/10.4310/HHA.2022.v24.n1.a12
  * Stenzel (2023) Raffael Stenzel. 2023\.  Univalence and completeness of Segal objects.  _Journal of Pure and Applied Algebra_ 227, 4 (2023), 107254\.  https://doi.org/10.1016/j.jpaa.2022.107254
  * Streicher (2014) Thomas Streicher. 2014\.  A model of type theory in simplicial sets: A brief introduction to Voevodsky’s homotopy type theory.  _Journal of Applied Logic_ 12, 1 (2014), 45–49.  https://doi.org/10.1016/j.jal.2013.04.001
  * Univalent Foundations Program (2013) The Univalent Foundations Program. 2013\.  _Homotopy Type Theory: Univalent Foundations of Mathematics_.  https://homotopytypetheory.org/book, Institute for Advanced Study.
  * van den Berg and Garner (2011) Benno van den Berg and Richard Garner. 2011.  Types are weak $\omega$-groupoids.  _Proceedings of the London Mathematical Society_ 102, 2 (2011), 370–394.  https://doi.org/10.1112/plms/pdq026
  * Voevodsky (2009) Vladimir Voevodsky. 2009\.  A very short note on homotopy $\lambda$-calculus.  https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf
  * Voevodsky (2013) Vladimir Voevodsky. 2013\.  A simple type system with two identity types.  _Unpublished note_ (2013).  https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf
  * Voevodsky et al. ([n. d.]) Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. [n. d.].  UniMath — a computer-checked library of univalent mathematics.  Available at http://unimath.org.  https://doi.org/10.5281/zenodo.7848572
  * Warren (2013) Michael Warren. 2013\.  Directed Type Theory.  https://www.ias.edu/video/univalent/1213/0410-MichaelWarren Lecture at IAS, Princeton, NJ.
  * Weaver and Licata (2020) Matthew Z. Weaver and Daniel R. Licata. 2020.  A Constructive Model of Directed Univalence in Bicubical Sets. In _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_ (Saarbrücken, Germany) _(LICS ’20)_. Association for Computing Machinery, New York, NY, USA, 915–928.  https://doi.org/10.1145/3373718.3394794
  * Weinberger (2022a) Jonathan Weinberger. 2022a.  _A Synthetic Perspective on $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects_.  Ph. D. Dissertation. TU Darmstadt.  https://doi.org/10.26083/tuprints-00020716
  * Weinberger (2022b) Jonathan Weinberger. 2022b.  Internal sums for synthetic fibered $(\infty,1)$-categories.  arXiv:2205.00386 [math.CT]
  * Weinberger (2022c) Jonathan Weinberger. 2022c.  Strict stability of extension types.  arXiv:2203.07194 [math.CT]
  * Weinberger (2022d) Jonathan Weinberger. 2022d.  Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories.  arXiv:2204.00938 [math.CT]