The n-Category Café

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 $2$ (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 $(\infty,1)$-topos). We can then define an arrow in a type $A$ to be a function $2\to A$.

However, often we want to talk about arrows with specified source and target. We can of course define the type $\hom_A(x,y)$ of such arrows to be $\sum_{f:2\to A} (f(0)=x)\times (f(1)=y)$, but since we are in homotopy type theory, the equalities $f0=x$ and $f1=y$ 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 $i:A\to B$ is a cofibration and $X:B\to \mathcal{U}$ is a type family dependent on $B$, while $f:\prod_{a:A} X(i(a))$ is a section of $X$ over $i$, then we introduce an extension type $\langle \prod_{b:B} X(b) \mid^i_f\rangle$ consisting of “those dependent functions $g:\prod_{b:B} X(b)$ such that $g(i(a)) \equiv f(a)$ — note the strict judgmental equality! — for any $a:A$”. This is modeled semantically by a “Leibniz” or “pullback-corner” map. In particular, we can define $\hom_A(x,y) = \langle \prod_{t:2} A \mid^{0,1}_{[x,y]} \rangle$, the type of functions $f:2\to A$ such that $f(0)\equiv x$ and $f(1) \equiv y$ 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 $(\infty,n)$-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 $2$, top and bottom elements $0,1 : 2$, and an inequality relation $\le$ satisfying the strict interval axioms.

Simplices can then be defined as

$$\Delta^n := \{ \langle t_1,\ldots, t_n\rangle \mid t_n \leq t_{n-1} \cdots t_2 \leq t_1 \}$$

Note that the 1-simplex $\Delta^1$ agrees with the interval $2$.

Boundaries, e.g. of the 2-simplex, can be defined similarly $$\partial\Delta^2 :=\{⟨t_1,t_2⟩: 2 \times 2 \mid (0 \equiv t_2 \leq t_1) \vee (t_2 \equiv t_1) \vee (t_2 \leq t_1 \equiv 1)\}$$ making the inclusion of the boundary of a 2-simplex into a cofibration.

Segal types

For any type $A$ with terms $x,y : A$ define

$$hom_A(x,y) := \langle 2 \to A \mid^{\partial\Delta^1}_{ [x,y]} \rangle$$

That is, a term $f : hom_A(x,y)$, which we call an arrow from $x$ to $y$ in $A$, is a function $f: 2 \to A$ so that $f(0) \equiv x$ and $f(1) \equiv y$. For $f : hom_A(x,y)$, $g : hom_A(y,z)$, and $h : hom_A(x,z)$, a similar extension type

$$hom_A(x,y,z,f,g,h) := \langle \Delta^2 \to A \mid^{\partial\Delta^2}_{[x,y,z,f,g,h]}\rangle$$

has terms that we interpret as witnesses that $h$ is the composite of $f$ and $g$. 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 $A$ is Segal if and only if for all $f : hom_A(x,y)$ and $g : hom_A(y,z)$ the type

$$\sum_{h : hom_A(x,z)} hom_A(x,y,z,f,g,h)$$

is contractible. A contractible type is in particular inhabited, and an inhabitant in this case defines a term $g \circ f : hom_A(x,z)$ that we refer to as the composite of $f$ and $g$, together with a 2-simplex witness $comp(g,f) : hom_A(x,y,z,f,g,g \circ f)$.

Somewhat surprisingly, this single contractibility condition characterizing Segal types in fact ensures coherent categorical structure at all dimensions. The reason is that if $A$ is Segal, then the type $X \to A$ is also Segal for any type or shape $X$. For instance, applying this result in the case $X=2$ 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

$$idtoarr : \prod_{x,y: A} (x=_A y) \to hom_A(x,y)$$

defined by identity elimination by sending the reflexivity term to the identity arrow, is an equivalence. In a discrete type, the $\infty$-groupoid structure encoded by the identity types and equivalent to the $(\infty,1)$-category structure encoded by the hom types. More precisely, a type $A$ 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 $A$ and $B$ are Segal types, then any function $f:A\to B$ is automatically a “functor”, since by composition it preserves 2-simplices and hence witnesses of composition. However, not every type family $C:A\to \mathcal{U}$ is necessarily functorial; in particular, the universe $\mathcal{U}$ is not Segal — its hom-types $\hom_{\mathcal{U}}(X,Y)$ consist intuitively of “spans and higher spans”. We say that $C:A\to \mathcal{U}$ is covariant if for any $f:\hom_A(x,y)$ and $u:C(x)$, the type

$$\sum_{v:C(y)} \langle \prod_{t:2} C(f(t)) \mid^{\partial\Delta^1}_{[u,v]}\rangle$$

of “liftings of $f$ starting at $u$” is contractible. An inhabitant of this type consists of a point $f_\ast(u):C(y)$, which we call the (covariant) transport of $u$ along $f$, along with a witness $trans(f,u)$. As with Segal types, this single contractibility condition suffices to ensure that this action is coherently functorial. It also ensures that the fibers $C(x)$ are discrete, and that the total space $\sum_{x:A} C(x)$ is Segal.

In particular, for any Segal type $A$ and any $a:A$, the hom-functor $\hom_A(a,-) :A \to \mathcal{U}$ is covariant. The Yoneda lemma says that for any covariant $C:A\to \mathcal{U}$, evaluation at $(a,id_a)$ defines an equivalence

$$\Big(\prod_{x:A} \hom_A(a,x) \to C(x)\Big) \simeq C(a)$$

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 $C : \Big(\sum_{x:A} \hom_A(a,x)\Big) \to \mathcal{U}$, we have a similar equivalence

$$\Big(\prod_{x:A} \prod_{f:\hom_A(a,x)} C(x,f)\Big) \simeq C(a,id_a).$$

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 $C : \Big(\sum_{x:A} (a=x)\Big) \to \mathcal{U}$, evaluation at $(a,refl_a)$ defines an equivalence

$$\Big(\prod_{x:A} \prod_{f:a=x} C(x,f)\Big) \simeq C(a,refl_a).$$

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

Rezk types

When is an arrow $f : hom_A(x,y)$ in a Segal type an isomorphism? Classically, $f$ 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:

$$isiso(f) := \left(\sum_{g : hom_A(y,x)} g \circ f = id_x\right) \times \left(\sum_{h : hom_A(y,x)} f \circ h = id_y \right)$$

An element of this type consists of a left inverse and a right inverse together with witnesses that the respective composites with $f$ define identities. It is easy to prove that $g = h$, so that $f$ 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 $isiso(f)$ are equal (i.e., $isiso(f)$ is a mere proposition), which would not be the case for the more naive definition.

The type of isomorphisms from $x$ to $y$ in $A$ is then defined to be

$$(x \cong_A y) := \sum_{f : \hom_A(x,y)} isiso(f).$$

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

$$\prod_{x,y: A} (x =_A y) \to (x \cong_A y)$$

and we say that a Segal type $A$ is Rezk complete if this map is an equivalence, in which case $A$ 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 $f : A \to B$ and $u : B \to A$ (i.e. functions between Segal types) together with a fiberwise equivalence

$$\prod_{a :A, b: B} \hom_A(a,u b) \simeq \hom_B(f a,b)$$

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 $\eta: Id_A \to u f$ and $\epsilon : f u \to Id_B$ (a “natural transformation” is just an arrow in a function-type between Segal types), and witnesses $\alpha$ and $\beta$ 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 $(\infty,1)$-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 $f \alpha : \epsilon \circ f u\epsilon \circ f\eta u \to \epsilon$ and $\beta u: \epsilon \circ \epsilon f u \circ f \eta u$ commute with the naturality isomorphism for $\epsilon$.

We prove that given Segal types $A$ and $B$ and functors $f : A \to B$ and $u : B \to A$, 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 $\phi$ and $\psi$ with homotopies $\phi \psi = 1$ and $\psi \phi = 1$ 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 $\eta$ and two counits $\epsilon,\epsilon'$, together with witnesses that $\eta,\epsilon$ satisfy one triangle identity and $\eta,\epsilon'$ satisfy the other triangle identity.

Finally, if the types $A$ and $B$ 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 $u:B\to A$ between Rezk types, the “type of left adjoints to $u$” is a mere proposition.