One of the observations that launched homotopy type theory is that the rule of identity-elimination in Martin-Löf’s identity types automatically generates the structure of an $<semantics>\mathrm{\infty}<annotation\; encoding="application/x-tex">\backslash infty</annotation></semantics>$-groupoid. In this way, homotopy type theory can be viewed as a “synthetic theory of $<semantics>\mathrm{\infty}<annotation\; encoding="application/x-tex">\backslash infty</annotation></semantics>$-groupoids.”

It is natural to ask whether there is a similar *directed* type theory that describes a “synthetic theory of $<semantics>(\mathrm{\infty},1)<annotation\; encoding="application/x-tex">(\backslash infty,1)</annotation></semantics>$-categories”
(or even higher categories). Interpreting types directly as (higher) categories runs into various problems, such as the fact that not all maps between categories are exponentiable (so that not all $<semantics>\prod <annotation\; encoding="application/x-tex">\backslash prod</annotation></semantics>$-types exist), and that there are numerous different kinds of “fibrations” given the various possible functorialities and dimensions of categories appearing as fibers. The 2-dimensional directed type theory of Licata and Harper has semantics in 1-categories, with a syntax that distinguishes between co- and contra-variant dependencies; but since the 1-categorical structure is “put in by hand”, it’s not especially synthetic and doesn’t generalize well to higher categories.

An alternative approach was independently suggested by Mike and by Joyal, motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the $<semantics>\mathrm{\infty}<annotation\; encoding="application/x-tex">\backslash infty</annotation></semantics>$-cosmos of complete Segal spaces, which we call *Rezk spaces*. It is not possible to model ordinary homotopy type theory directly in the Rezk model structure, which is not right proper, but we can model it in the Reedy model structure and then identify internally some “types with composition,” which correspond to Segal spaces, and “types with composition and univalence,” which correspond to the Rezk spaces.

Almost five years later, we are finally developing this approach in more detail. In a new paper now available on the arXiv, Mike and I give definitions of *Segal* and *Rezk types* motivated by these semantics, and demonstrate that these simple definitions suffice to develop the synthetic theory of $<semantics>(\mathrm{\infty},1)<annotation\; encoding="application/x-tex">(\backslash infty,1)</annotation></semantics>$-categories. So far this includes functors, natural transformations, co- and contravariant type families with discrete fibers ($<semantics>\mathrm{\infty}<annotation\; encoding="application/x-tex">\backslash infty</annotation></semantics>$-groupoids), the Yoneda lemma (including a “dependent” Yoneda lemma that looks like “directed identity-elimination”), and the theory of coherent adjunctions.

## Cofibrations and extension types

One of the reasons this took so long to happen is that it required a technical innovation to become feasible. To develop the synthetic theory of Segal and Rezk types, we need to detect the semantic structure of the simplicial spaces model internally, and it seems that the best way to do this is to axiomatize the presence of a *strict interval* $<semantics>2<annotation\; encoding="application/x-tex">2</annotation></semantics>$ (a totally ordered set with distinct top and bottom elements). This is the geometric theory of which simplicial sets are the classifying topos (and of which simplicial spaces are the classifying $<semantics>(\mathrm{\infty},1)<annotation\; encoding="application/x-tex">(\backslash infty,1)</annotation></semantics>$-topos). We can then define an *arrow* in a type $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ to be a function $<semantics>2\to A<annotation\; encoding="application/x-tex">2\backslash to\; A</annotation></semantics>$.

However, often we want to talk about arrows with specified source and target. We can of course define the type $<semantics>{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">\backslash hom\_A(x,y)</annotation></semantics>$ of such arrows to be $<semantics>{\sum}_{f:2\to A}(f(0)=x)\times (f(1)=y)<annotation\; encoding="application/x-tex">\backslash sum\_\{f:2\backslash to\; A\}\; (f(0)=x)\backslash times\; (f(1)=y)</annotation></semantics>$, but since we are in homotopy type theory, the equalities $<semantics>f0=x<annotation\; encoding="application/x-tex">f0=x</annotation></semantics>$ and $<semantics>f1=y<annotation\; encoding="application/x-tex">f1=y</annotation></semantics>$ are *data*, i.e. homotopical paths, that have to be carried around everywhere. When we start talking about 2-simplices and 3-simplices with specified boundaries as well, the complexity becomes unmanageable.

The innovation that solves this problem is to introduce a notion of *cofibration* in type theory, with a corresponding type of *extensions*. If $<semantics>i:A\to B<annotation\; encoding="application/x-tex">i:A\backslash to\; B</annotation></semantics>$ is a cofibration and $<semantics>X:B\to \mathcal{U}<annotation\; encoding="application/x-tex">X:B\backslash to\; \backslash mathcal\{U\}</annotation></semantics>$ is a type family dependent on $<semantics>B<annotation\; encoding="application/x-tex">B</annotation></semantics>$, while $<semantics>f:{\prod}_{a:A}X(i(a))<annotation\; encoding="application/x-tex">f:\backslash prod\_\{a:A\}\; X(i(a))</annotation></semantics>$ is a section of $<semantics>X<annotation\; encoding="application/x-tex">X</annotation></semantics>$ over $<semantics>i<annotation\; encoding="application/x-tex">i</annotation></semantics>$, then we introduce an **extension type** $<semantics>\u27e8{\prod}_{b:B}X(b){\mid}_{f}^{i}\u27e9<annotation\; encoding="application/x-tex">\backslash langle\; \backslash prod\_\{b:B\}\; X(b)\; \backslash mid^i\_f\backslash rangle</annotation></semantics>$ consisting of “those dependent functions $<semantics>g:{\prod}_{b:B}X(b)<annotation\; encoding="application/x-tex">g:\backslash prod\_\{b:B\}\; X(b)</annotation></semantics>$ such that $<semantics>g(i(a))\equiv f(a)<annotation\; encoding="application/x-tex">g(i(a))\; \backslash equiv\; f(a)</annotation></semantics>$ — note the strict judgmental equality! — for any $<semantics>a:A<annotation\; encoding="application/x-tex">a:A</annotation></semantics>$”. This is modeled semantically by a “Leibniz” or “pullback-corner” map. In particular, we can define $<semantics>{\mathrm{hom}}_{A}(x,y)=\u27e8{\prod}_{t:2}A{\mid}_{[x,y]}^{0,1}\u27e9<annotation\; encoding="application/x-tex">\backslash hom\_A(x,y)\; =\; \backslash langle\; \backslash prod\_\{t:2\}\; A\; \backslash mid^\{0,1\}\_\{[x,y]\}\; \backslash rangle</annotation></semantics>$, the type of functions $<semantics>f:2\to A<annotation\; encoding="application/x-tex">f:2\backslash to\; A</annotation></semantics>$ such that $<semantics>f(0)\equiv x<annotation\; encoding="application/x-tex">f(0)\backslash equiv\; x</annotation></semantics>$ and $<semantics>f(1)\equiv y<annotation\; encoding="application/x-tex">f(1)\; \backslash equiv\; y</annotation></semantics>$ strictly, and so on for higher simplices.

General extension types along cofibrations were first considered by Mike and Peter Lumsdaine for a different purpose. In addition to the pullback-corner semantics, they are inspired by the path-types of cubical type theory, which replace the inductively specified identity types of ordinary homotopy type theory with a similar sort of restricted function-type out of the cubical interval. Our paper introduces a general notion of “type theory with shapes” and extension types that includes the basic setup of cubical type theory as well as our simplicial type theory, along with potential generalizations to Joyal’s “disks” for a synthetic theory of $<semantics>(\mathrm{\infty},n)<annotation\; encoding="application/x-tex">(\backslash infty,n)</annotation></semantics>$-categories.

## Simplices in the theory of a strict interval

In simplicial type theory, the cofibrations are the “inclusions of shapes” generated by the coherent theory of a strict interval, which is axiomatized by the interval $<semantics>2<annotation\; encoding="application/x-tex">2</annotation></semantics>$, top and bottom elements $<semantics>0,1:2<annotation\; encoding="application/x-tex">0,1\; :\; 2</annotation></semantics>$, and an inequality relation $<semantics>\le <annotation\; encoding="application/x-tex">\backslash le</annotation></semantics>$ satisfying the strict interval axioms.

Simplices can then be defined as

$$<semantics>{\Delta}^{n}:=\{\u27e8{t}_{1},\dots ,{t}_{n}\u27e9\mid {t}_{n}\le {t}_{n-1}\cdots {t}_{2}\le {t}_{1}\}<annotation\; encoding="application/x-tex">\; \backslash Delta^n\; :=\; \backslash \{\; \backslash langle\; t\_1,\backslash ldots,\; t\_n\backslash rangle\; \backslash mid\; t\_n\; \backslash leq\; t\_\{n-1\}\; \backslash cdots\; t\_2\; \backslash leq\; t\_1\; \backslash \}\; </annotation></semantics>$$

Note that the 1-simplex $<semantics>{\Delta}^{1}<annotation\; encoding="application/x-tex">\backslash Delta^1</annotation></semantics>$ agrees with the interval $<semantics>2<annotation\; encoding="application/x-tex">2</annotation></semantics>$.

Boundaries, e.g. of the 2-simplex, can be defined similarly
$$<semantics>\partial {\Delta}^{2}:=\{\u27e8{t}_{1},{t}_{2}\u27e9:2\times 2\mid (0\equiv {t}_{2}\le {t}_{1})\vee ({t}_{2}\equiv {t}_{1})\vee ({t}_{2}\le {t}_{1}\equiv 1)\}<annotation\; encoding="application/x-tex">\; \backslash partial\backslash Delta^2\; :=\backslash \{\&\#10216;t\_1,t\_2\&\#10217;:\; 2\; \backslash times\; 2\; \backslash mid\; (0\; \backslash equiv\; t\_2\; \backslash leq\; t\_1)\; \backslash vee\; (t\_2\; \backslash equiv\; t\_1)\; \backslash vee\; (t\_2\; \backslash leq\; t\_1\; \backslash equiv\; 1)\backslash \}\; </annotation></semantics>$$
making the inclusion of the boundary of a 2-simplex into a cofibration.

## Segal types

For any type $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ with terms $<semantics>x,y:A<annotation\; encoding="application/x-tex">x,y\; :\; A</annotation></semantics>$ define

$$<semantics>{\mathrm{hom}}_{A}(x,y):=\u27e82\to A{\mid}_{[x,y]}^{\partial {\Delta}^{1}}\u27e9<annotation\; encoding="application/x-tex">\; hom\_A(x,y)\; :=\; \backslash langle\; 2\; \backslash to\; A\; \backslash mid^\{\backslash partial\backslash Delta^1\}\_\{\; [x,y]\}\; \backslash rangle\; </annotation></semantics>$$

That is, a term $<semantics>f:{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">f\; :\; hom\_A(x,y)</annotation></semantics>$, which we call an **arrow** from $<semantics>x<annotation\; encoding="application/x-tex">x</annotation></semantics>$ to $<semantics>y<annotation\; encoding="application/x-tex">y</annotation></semantics>$ in $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$, is a function $<semantics>f:2\to A<annotation\; encoding="application/x-tex">f:\; 2\; \backslash to\; A</annotation></semantics>$ so that $<semantics>f(0)\equiv x<annotation\; encoding="application/x-tex">f(0)\; \backslash equiv\; x</annotation></semantics>$ and $<semantics>f(1)\equiv y<annotation\; encoding="application/x-tex">f(1)\; \backslash equiv\; y</annotation></semantics>$. For $<semantics>f:{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">f\; :\; hom\_A(x,y)</annotation></semantics>$, $<semantics>g:{\mathrm{hom}}_{A}(y,z)<annotation\; encoding="application/x-tex">g\; :\; hom\_A(y,z)</annotation></semantics>$, and $<semantics>h:{\mathrm{hom}}_{A}(x,z)<annotation\; encoding="application/x-tex">h\; :\; hom\_A(x,z)</annotation></semantics>$, a similar extension type

$$<semantics>{\mathrm{hom}}_{A}(x,y,z,f,g,h):=\u27e8{\Delta}^{2}\to A{\mid}_{[x,y,z,f,g,h]}^{\partial {\Delta}^{2}}\u27e9<annotation\; encoding="application/x-tex">\; hom\_A(x,y,z,f,g,h)\; :=\; \backslash langle\; \backslash Delta^2\; \backslash to\; A\; \backslash mid^\{\backslash partial\backslash Delta^2\}\_\{[x,y,z,f,g,h]\}\backslash rangle\; </annotation></semantics>$$

has terms that we interpret as witnesses that $<semantics>h<annotation\; encoding="application/x-tex">h</annotation></semantics>$ is the composite of $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ and $<semantics>g<annotation\; encoding="application/x-tex">g</annotation></semantics>$. We define a **Segal type** to be a type in which any composable pair of arrows admits a unique (composite, witness) pair. In homotopy type theory, this may be expressed by saying that $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is **Segal** if and only if for all $<semantics>f:{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">f\; :\; hom\_A(x,y)</annotation></semantics>$ and $<semantics>g:{\mathrm{hom}}_{A}(y,z)<annotation\; encoding="application/x-tex">g\; :\; hom\_A(y,z)</annotation></semantics>$ the type

$$<semantics>\sum _{h:{\mathrm{hom}}_{A}(x,z)}{\mathrm{hom}}_{A}(x,y,z,f,g,h)<annotation\; encoding="application/x-tex">\; \backslash sum\_\{h\; :\; hom\_A(x,z)\}\; hom\_A(x,y,z,f,g,h)\; </annotation></semantics>$$

is contractible. A contractible type is in particular inhabited, and an inhabitant in this case defines a term $<semantics>g\circ f:{\mathrm{hom}}_{A}(x,z)<annotation\; encoding="application/x-tex">g\; \backslash circ\; f\; :\; hom\_A(x,z)</annotation></semantics>$ that we refer to as **the composite** of $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ and $<semantics>g<annotation\; encoding="application/x-tex">g</annotation></semantics>$, together with a 2-simplex witness $<semantics>\mathrm{comp}(g,f):{\mathrm{hom}}_{A}(x,y,z,f,g,g\circ f)<annotation\; encoding="application/x-tex">comp(g,f)\; :\; hom\_A(x,y,z,f,g,g\; \backslash circ\; f)</annotation></semantics>$.

Somewhat surprisingly, this single contractibility condition characterizing Segal types in fact ensures coherent categorical structure at all dimensions. The reason is that if $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is Segal, then the type $<semantics>X\to A<annotation\; encoding="application/x-tex">X\; \backslash to\; A</annotation></semantics>$ is also Segal for any type or shape $<semantics>X<annotation\; encoding="application/x-tex">X</annotation></semantics>$. For instance, applying this result in the case $<semantics>X=2<annotation\; encoding="application/x-tex">X=2</annotation></semantics>$ allows us to prove that the composition operation in any Segal type is associative. In an appendix we prove a conjecture of Joyal that in the simplical spaces model this condition really does characterize exactly the Segal spaces, as usually defined.

## Discrete types

An example of a Segal type is a **discrete type**, which is one for which the map

$$<semantics>\mathrm{idtoarr}:\prod _{x,y:A}(x{=}_{A}y)\to {\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">\; idtoarr\; :\; \backslash prod\_\{x,y:\; A\}\; (x=\_A\; y)\; \backslash to\; hom\_A(x,y)\; </annotation></semantics>$$

defined by identity elimination by sending the reflexivity term to the identity arrow, is an equivalence. In a discrete type, the $<semantics>\mathrm{\infty}<annotation\; encoding="application/x-tex">\backslash infty</annotation></semantics>$-groupoid structure encoded by the identity types and equivalent to the $<semantics>(\mathrm{\infty},1)<annotation\; encoding="application/x-tex">(\backslash infty,1)</annotation></semantics>$-category structure encoded by the hom types. More precisely, a type $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is discrete if and only if it is Segal, as well as *Rezk-complete* (in the sense to be defined later on), and moreover “every arrow is an isomorphism”.

## The dependent Yoneda lemma

If $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ and $<semantics>B<annotation\; encoding="application/x-tex">B</annotation></semantics>$ are Segal types, then any function $<semantics>f:A\to B<annotation\; encoding="application/x-tex">f:A\backslash to\; B</annotation></semantics>$ is automatically a “functor”, since by composition it preserves 2-simplices and hence witnesses of composition. However, not every type family $<semantics>C:A\to \mathcal{U}<annotation\; encoding="application/x-tex">C:A\backslash to\; \backslash mathcal\{U\}</annotation></semantics>$ is necessarily functorial; in particular, the universe $<semantics>\mathcal{U}<annotation\; encoding="application/x-tex">\backslash mathcal\{U\}</annotation></semantics>$ is not Segal — its hom-types $<semantics>{\mathrm{hom}}_{\mathcal{U}}(X,Y)<annotation\; encoding="application/x-tex">\backslash hom\_\{\backslash mathcal\{U\}\}(X,Y)</annotation></semantics>$ consist intuitively of “spans and higher spans”. We say that $<semantics>C:A\to \mathcal{U}<annotation\; encoding="application/x-tex">C:A\backslash to\; \backslash mathcal\{U\}</annotation></semantics>$ is **covariant** if for any $<semantics>f:{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">f:\backslash hom\_A(x,y)</annotation></semantics>$ and $<semantics>u:C(x)<annotation\; encoding="application/x-tex">u:C(x)</annotation></semantics>$, the type

$$<semantics>\sum _{v:C(y)}\u27e8\prod _{t:2}C(f(t)){\mid}_{[u,v]}^{\partial {\Delta}^{1}}\u27e9<annotation\; encoding="application/x-tex">\; \backslash sum\_\{v:C(y)\}\; \backslash langle\; \backslash prod\_\{t:2\}\; C(f(t))\; \backslash mid^\{\backslash partial\backslash Delta^1\}\_\{[u,v]\}\backslash rangle\; </annotation></semantics>$$

of “liftings of $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ starting at $<semantics>u<annotation\; encoding="application/x-tex">u</annotation></semantics>$” is contractible. An inhabitant of this type consists of a point $<semantics>{f}_{*}(u):C(y)<annotation\; encoding="application/x-tex">f\_\backslash ast(u):C(y)</annotation></semantics>$, which we call the *(covariant) transport of $<semantics>u<annotation\; encoding="application/x-tex">u</annotation></semantics>$ along $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$*, along with a witness $<semantics>\mathrm{trans}(f,u)<annotation\; encoding="application/x-tex">trans(f,u)</annotation></semantics>$. As with Segal types, this single contractibility condition suffices to ensure that this action is coherently functorial. It also ensures that the fibers $<semantics>C(x)<annotation\; encoding="application/x-tex">C(x)</annotation></semantics>$ are discrete, and that the total space $<semantics>{\sum}_{x:A}C(x)<annotation\; encoding="application/x-tex">\backslash sum\_\{x:A\}\; C(x)</annotation></semantics>$ is Segal.

In particular, for any Segal type $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ and any $<semantics>a:A<annotation\; encoding="application/x-tex">a:A</annotation></semantics>$, the hom-functor $<semantics>{\mathrm{hom}}_{A}(a,-):A\to \mathcal{U}<annotation\; encoding="application/x-tex">\backslash hom\_A(a,-)\; :A\; \backslash to\; \backslash mathcal\{U\}</annotation></semantics>$ is covariant. The Yoneda lemma says that for any covariant $<semantics>C:A\to \mathcal{U}<annotation\; encoding="application/x-tex">C:A\backslash to\; \backslash mathcal\{U\}</annotation></semantics>$, evaluation at $<semantics>(a,{\mathrm{id}}_{a})<annotation\; encoding="application/x-tex">(a,id\_a)</annotation></semantics>$ defines an equivalence

$$<semantics>(\prod _{x:A}{\mathrm{hom}}_{A}(a,x)\to C(x))\simeq C(a)<annotation\; encoding="application/x-tex">\; \backslash Big(\backslash prod\_\{x:A\}\; \backslash hom\_A(a,x)\; \backslash to\; C(x)\backslash Big)\; \backslash simeq\; C(a)\; </annotation></semantics>$$

The usual proof of the Yoneda lemma applies, except that it’s simpler since we don’t need to check naturality or functoriality; in the “synthetic” world all of that comes for free.

More generally, we have a *dependent Yoneda lemma*, which says that for any covariant $<semantics>C:({\sum}_{x:A}{\mathrm{hom}}_{A}(a,x))\to \mathcal{U}<annotation\; encoding="application/x-tex">C\; :\; \backslash Big(\backslash sum\_\{x:A\}\; \backslash hom\_A(a,x)\backslash Big)\; \backslash to\; \backslash mathcal\{U\}</annotation></semantics>$, we have a similar equivalence

$$<semantics>(\prod _{x:A}\prod _{f:{\mathrm{hom}}_{A}(a,x)}C(x,f))\simeq C(a,{\mathrm{id}}_{a}).<annotation\; encoding="application/x-tex">\; \backslash Big(\backslash prod\_\{x:A\}\; \backslash prod\_\{f:\backslash hom\_A(a,x)\}\; C(x,f)\backslash Big)\; \backslash simeq\; C(a,id\_a).\; </annotation></semantics>$$

This should be compared with the universal property of identity-elimination (path induction) in ordinary homotopy type theory, which says that for *any* type family $<semantics>C:({\sum}_{x:A}(a=x))\to \mathcal{U}<annotation\; encoding="application/x-tex">C\; :\; \backslash Big(\backslash sum\_\{x:A\}\; (a=x)\backslash Big)\; \backslash to\; \backslash mathcal\{U\}</annotation></semantics>$, evaluation at $<semantics>(a,{\mathrm{refl}}_{a})<annotation\; encoding="application/x-tex">(a,refl\_a)</annotation></semantics>$ defines an equivalence

$$<semantics>(\prod _{x:A}\prod _{f:a=x}C(x,f))\simeq C(a,{\mathrm{refl}}_{a}).<annotation\; encoding="application/x-tex">\; \backslash Big(\backslash prod\_\{x:A\}\; \backslash prod\_\{f:a=x\}\; C(x,f)\backslash Big)\; \backslash simeq\; C(a,refl\_a).\; </annotation></semantics>$$

In other words, the dependent Yoneda lemma really is a “directed” generalization of path induction.

## Rezk types

When is an arrow $<semantics>f:{\mathrm{hom}}_{A}(x,y)<annotation\; encoding="application/x-tex">f\; :\; hom\_A(x,y)</annotation></semantics>$ in a Segal type an isomorphism? Classically, $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ is an isomorphism just when it has a two-sided inverse, but in homotopy type theory more care is needed, for the same reason that we have to be careful when defining what it means for a function to be an equivalence: we want the notion of “being an isomorphism” to be a mere proposition. We could use analogues of any of the equivalent notions of equivalence in Chapter 4 of the HoTT Book, but the simplest is the following:

$$<semantics>\mathrm{isiso}(f):=(\sum _{g:{\mathrm{hom}}_{A}(y,x)}g\circ f={\mathrm{id}}_{x})\times (\sum _{h:{\mathrm{hom}}_{A}(y,x)}f\circ h={\mathrm{id}}_{y})<annotation\; encoding="application/x-tex">\; isiso(f)\; :=\; \backslash left(\backslash sum\_\{g\; :\; hom\_A(y,x)\}\; g\; \backslash circ\; f\; =\; id\_x\backslash right)\; \backslash times\; \backslash left(\backslash sum\_\{h\; :\; hom\_A(y,x)\}\; f\; \backslash circ\; h\; =\; id\_y\; \backslash right)\; </annotation></semantics>$$

An element of this type consists of a left inverse and a right inverse together with witnesses that the respective composites with $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ define identities. It is easy to prove that $<semantics>g=h<annotation\; encoding="application/x-tex">g\; =\; h</annotation></semantics>$, so that $<semantics>f<annotation\; encoding="application/x-tex">f</annotation></semantics>$ is an isomorphism if and only if it admits a two-sided inverse, but the point is that any pair of terms in the type $<semantics>\mathrm{isiso}(f)<annotation\; encoding="application/x-tex">isiso(f)</annotation></semantics>$ are equal (i.e., $<semantics>\mathrm{isiso}(f)<annotation\; encoding="application/x-tex">isiso(f)</annotation></semantics>$ is a mere proposition), which would not be the case for the more naive definition.

The type of isomorphisms from $<semantics>x<annotation\; encoding="application/x-tex">x</annotation></semantics>$ to $<semantics>y<annotation\; encoding="application/x-tex">y</annotation></semantics>$ in $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is then defined to be

$$<semantics>(x{\cong}_{A}y):=\sum _{f:{\mathrm{hom}}_{A}(x,y)}\mathrm{isiso}(f).<annotation\; encoding="application/x-tex">\; (x\; \backslash cong\_A\; y)\; :=\; \backslash sum\_\{f\; :\; \backslash hom\_A(x,y)\}\; isiso(f).\; </annotation></semantics>$$

Identity arrows are in particular isomorphisms, so by identity-elimination there is a map

$$<semantics>\prod _{x,y:A}(x{=}_{A}y)\to (x{\cong}_{A}y)<annotation\; encoding="application/x-tex">\; \backslash prod\_\{x,y:\; A\}\; (x\; =\_A\; y)\; \backslash to\; (x\; \backslash cong\_A\; y)\; </annotation></semantics>$$

and we say that a Segal type $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is **Rezk complete** if this map is an equivalence, in which case $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ is a **Rezk type**.

## Coherent adjunctions

Similarly, it is somewhat delicate to define homotopy correct types of adjunction data that are contractible when they are inhabited. In the final section to our paper, we compare *transposing adjunctions*, by which we mean functors $<semantics>f:A\to B<annotation\; encoding="application/x-tex">f\; :\; A\; \backslash to\; B</annotation></semantics>$ and $<semantics>u:B\to A<annotation\; encoding="application/x-tex">u\; :\; B\; \backslash to\; A</annotation></semantics>$ (i.e. functions between Segal types) together with a fiberwise equivalence

$$<semantics>\prod _{a:A,b:B}{\mathrm{hom}}_{A}(a,ub)\simeq {\mathrm{hom}}_{B}(fa,b)<annotation\; encoding="application/x-tex">\; \backslash prod\_\{a\; :A,\; b:\; B\}\; \backslash hom\_A(a,u\; b)\; \backslash simeq\; \backslash hom\_B(f\; a,b)\; </annotation></semantics>$$

with various notions of *diagrammatic adjunctions*, specified in terms of units and counits and higher coherence data.

The simplest of these, which we refer to as a **quasi-diagrammatic adjunction** is specified by a pair of functors as above, natural transformations $<semantics>\eta :{\mathrm{Id}}_{A}\to uf<annotation\; encoding="application/x-tex">\backslash eta:\; Id\_A\; \backslash to\; u\; f</annotation></semantics>$ and $<semantics>\u03f5:fu\to {\mathrm{Id}}_{B}<annotation\; encoding="application/x-tex">\backslash epsilon\; :\; f\; u\; \backslash to\; Id\_B</annotation></semantics>$ (a “natural transformation” is just an arrow in a function-type between Segal types), and witnesses $<semantics>\alpha <annotation\; encoding="application/x-tex">\backslash alpha</annotation></semantics>$ and $<semantics>\beta <annotation\; encoding="application/x-tex">\backslash beta</annotation></semantics>$ to both of the triangle identities. The incoherence of this type of data has been observed in bicategory theory (it is not cofibrant as a 2-category) and in $<semantics>(\mathrm{\infty},1)<annotation\; encoding="application/x-tex">(\backslash infty,1)</annotation></semantics>$-catgory theory (as a subcomputad of the free homotopy coherent adjunction it is not *parental*). One
homotopically correct type of adjunction data is a **half-adjoint diagrammatic adjunction**, which has additionally a witness that $<semantics>f\alpha :\u03f5\circ fu\u03f5\circ f\eta u\to \u03f5<annotation\; encoding="application/x-tex">f\; \backslash alpha\; :\; \backslash epsilon\; \backslash circ\; f\; u\backslash epsilon\; \backslash circ\; f\backslash eta\; u\; \backslash to\; \backslash epsilon</annotation></semantics>$ and $<semantics>\beta u:\u03f5\circ \u03f5fu\circ f\eta u<annotation\; encoding="application/x-tex">\backslash beta\; u:\; \backslash epsilon\; \backslash circ\; \backslash epsilon\; f\; u\; \backslash circ\; f\; \backslash eta\; u</annotation></semantics>$ commute with the naturality isomorphism for $<semantics>\u03f5<annotation\; encoding="application/x-tex">\backslash epsilon</annotation></semantics>$.

We prove that given Segal types $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ and $<semantics>B<annotation\; encoding="application/x-tex">B</annotation></semantics>$ and functors $<semantics>f:A\to B<annotation\; encoding="application/x-tex">f\; :\; A\; \backslash to\; B</annotation></semantics>$ and $<semantics>u:B\to A<annotation\; encoding="application/x-tex">u\; :\; B\; \backslash to\; A</annotation></semantics>$, the type of half-adjoint diagrammatic adjunctions between them is equivalent to the type of transposing adjunctions. More precisely, if in the notion of transposing adjunction we interpret “equivalence” as a “half-adjoint equivalence”, i.e. a pair of maps $<semantics>\varphi <annotation\; encoding="application/x-tex">\backslash phi</annotation></semantics>$ and $<semantics>\psi <annotation\; encoding="application/x-tex">\backslash psi</annotation></semantics>$ with homotopies $<semantics>\varphi \psi =1<annotation\; encoding="application/x-tex">\backslash phi\; \backslash psi\; =\; 1</annotation></semantics>$ and $<semantics>\psi \varphi =1<annotation\; encoding="application/x-tex">\backslash psi\; \backslash phi\; =\; 1</annotation></semantics>$ and a witness to *one* of the triangle identities for an adjoint equivalence (this is another of the coherent notions of equivalence from the HoTT Book), then these data correspond exactly under the Yoneda lemma to those of a half-adjoint diagrammatic adjunction.

This suggests that similar correspondences for other kinds of coherent equivalences. For instance, if we interpret transposing adjunctions using the “bi-invertibility” notion of coherent equivalence (specification of a separate left and right inverse, as we used above to define isomorphisms in a Segal type), we obtain upon Yoneda-fication a new notion of coherent diagrammatic adjunction, consisting of a unit $<semantics>\eta <annotation\; encoding="application/x-tex">\backslash eta</annotation></semantics>$ and *two* counits $<semantics>\u03f5,\u03f5\prime <annotation\; encoding="application/x-tex">\backslash epsilon,\backslash epsilon\text{\'}</annotation></semantics>$, together with witnesses that $<semantics>\eta ,\u03f5<annotation\; encoding="application/x-tex">\backslash eta,\backslash epsilon</annotation></semantics>$ satisfy one triangle identity and $<semantics>\eta ,\u03f5\prime <annotation\; encoding="application/x-tex">\backslash eta,\backslash epsilon\text{\'}</annotation></semantics>$ satisfy the other triangle identity.

Finally, if the types $<semantics>A<annotation\; encoding="application/x-tex">A</annotation></semantics>$ and $<semantics>B<annotation\; encoding="application/x-tex">B</annotation></semantics>$ are not just Segal but Rezk, we can show that adjoints are literally unique, not just “unique up to isomorphism”. That is, given a functor $<semantics>u:B\to A<annotation\; encoding="application/x-tex">u:B\backslash to\; A</annotation></semantics>$ between Rezk types, the “type of left adjoints to $<semantics>u<annotation\; encoding="application/x-tex">u</annotation></semantics>$” is a mere proposition.