Reedy fibrations

The first part of this explainer mostly follows (Shulman, 2014).

A brief word on Notation.

todo

Inverse categories

definition1Inverse category A binary relation $\prec$ may be placed on the collection of objects of any category $\mathcal C$ by defining $y \prec x$ if and only if there is an arrow $x \rightarrow y$ in $\mathcal C$. An inverse category $\mathcal I$ is one for which $\prec$ is well-founded.

definition2Degree/rank Given an inverse category $\mathcal I$, we can define the degree aka rank $\rho(x)$ of an object $x$ of $\mathcal I$ by well-founded recursion in the usual way: \[ \rho(x) \coloneqq \sup_{y \, \prec \, x} \big( \rho(y) + 1 \big). \] The rank $\rho(\mathcal I)$ of $\mathcal I$ itself is then \[ \rho(\mathcal I) \coloneqq \sup_{x \, \in \, \mathcal I} \big( \rho(x) + 1 \big). \]

Equivalently, an inverse category $\mathcal I$ is one for which there is an ordinal $\lambda$ together with a rank function $\rho \colon \mathrm{ob}(\mathcal I) \rightarrow \lambda$, such that any nonidentity arrow $f \colon x \rightarrow y$ strictly lowers degree—i.e. $\rho(y) < \rho(x)$. We may always assume that $\rho$ is of the form given in definition (2).

definition3Truncated inverse category For an inverse category $\mathcal I$ and $x \in \mathcal I$, the $x$-truncated category $\Ix$ is the full subcategory of $\mathcal I$ on objects $y \prec x$. We also use $\Iex$ to denote the full subcategory on $\Ix \cup \{x\}$, but do not bother to give it a name.

Diagrams on inverse categories

notation4 For a category $\mathcal C$ and $x \in \mathcal C$, let denote the full subcategory of without the object $\mathrm{1}_x \colon x \rightarrow x$. Note that for an inverse category $\mathcal I$ and $x \in \mathcal I$ there is the canonical “codomain” forgetful functor .

Suppose we have a category $\mathcal C$, an inverse category $\mathcal I$ and a diagram $A_{\prec x} \colon \mathcal{I}_{\prec x} \rightarrow \mathcal C$ on the truncated inverse category. By unfolding definitions, we can see that (the data of) extensions of $A_{\prec x}$ to a diagram \[ A_{\preceq x} \colon \Iex \rightarrow \mathcal C \] are equivalently cones over which are equivalently maps into provided this limit exists.

definition5Matching object Suppose we have a category $\mathcal C$, inverse category $\mathcal I$ and diagram $A \colon \mathcal J \rightarrow \mathcal C$ where $\mathcal J \subseteq \mathcal I$ is a subcategory containing $\Ix$. The matching object $M_xA$ (of $A$, on “level” $x$) is the limit if it exists.

The preceding discussion then says that if the $x$-matching object for $A_{\prec x}$ exists, we can extend $A_{\prec x}$ to $x$ by simply giving an object $A_x$ and a map $A_x \rightarrow M_xA$ in $\mathcal I$.

Now let us consider extensions of maps between inverse diagrams. Suppose that $A_{\preceq x},\ B_{\preceq x} \colon \Iex \rightarrow \mathcal C$ have $x$-matching objects $M_xA,\ M_xB$, and that $f_{\prec x} \colon A_{\prec x} \rightarrow B_{\prec x}$ is a natural transformation restricted to the respective $x$-truncations. Then we can again check that extensions of $f_{\prec x}$ to maps \[ f_{\preceq x} \colon A_{\preceq x} \rightarrow B_{\preceq x} \] are equivalently lids of the square (where the walls and base are the evident arrows), which are equivalently arrows

labeled6 \[ A_x \xrightarrow{f_x} M_xA \times_{M_xB} B_x \]

such that commutes, provided that the pullback exists.

To summarize: if an inverse diagram $A \colon \mathcal{C}^{\mathcal I}$ has all matching objects, then it has a simple and uniform recursive description in terms of maps into $M_xA$ for all $x \in \mathcal I$ (note that $M_xA$ is always terminal for $\prec$-minimal $x$). Similarly, maps between inverse diagrams $A$, $B$ with all matching objects also have a uniform description in terms of maps in the sense of (6), assuming the pullback exists in $\mathcal C$.

Part of the appeal of these properties is that they suggest the possibility of encoding, for fixed $\mathcal I$, the type of such $\mathcal I$-diagrams and maps between them (possibly subject to additional conditions). We’ll come back to discuss this idea shortly.

Recall the definition of a type-theoretic fibration category (Shulman, 2014, 2.1). In particular, these are equipped with a terminal object and a class $\mathfrak F \subseteq \mathrm{mor}(\mathcal C)$ of fibrations (containing all terminal arrows and isomorphisms, closed under pullbacks, etc.) interpreting types-in-context.

definition7Reedy fibration Let $\mathcal C$ be a type theoretic fibration category and $\mathcal I$ an inverse category. A Reedy fibration $f \colon A \rightarrow B$ between diagrams $A,\ B \colon \mathcal{C}^{\mathcal I}$ is one where:

definition8Reedy fibrant diagram A Reedy fibrant diagram $A \colon \mathcal{C}^{\mathcal I}$ is one for which the terminal arrow is a Reedy fibration. Equivalently, it’s one with all matching objects and such that $A_x \rightarrow M_xA$ is a fibration for all $x$. Note that the terminal diagram is itself Reedy fibrant.

remark9 The extra fibrancy requirement on the map into the pullback in definition (7) ensures that we can place a type theoretic fibration structure on the category of Reedy fibrant diagrams and Reedy fibrations, and thus construct new models of type theory in such diagrams.

Type-valued Reedy fibrant diagrams

Now fix an inverse category $\mathcal I$ and ask for $\mathcal I$-diagrams in $\Type$, i.e. presheaves $A \colon \Type^\mathcal{I}$ valued in the category of types and functions of a type theory with $\Pi$, strong $\Sigma$, and unit types.

At such a level of generality, it’s not yet known how to perform such constructions type-theoretically, or indeed, if it’s even possible. Certainly there’s no hope if we’re asking for strict diagrams, so we should look instead for the correct notion “up to homotopy”.

todo

References

  1. Shulman, M. (2014). Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5), 1203–1277. https://doi.org/10.1017/s0960129514000565