Reedy fibrations
The first part of this explainer mostly follows (missing reference).
A brief word on Notation.
- We denote “$x$ (is) an object of $\mathcal C$” variously by $x \in \mathcal C$ or $x \in \mathrm{ob}(\mathcal C)$. Similarly, “$f$ (is) an arrow of $\mathcal C$” may be denoted $f \in \mathcal C$ or $f \in \mathrm{mor}(\mathcal C)$, but we shall be careful to always disambiguate with the latter notation if there is a danger of confusion.
- We also occasionally mix the use of $\in$ and $\colon$, especially when speaking of anything that may be interpreted as an arrow of some category. When this occurs outside of an explicitly type theoretic context, one should feel free to mentally substitute the more comfortable notation for the other.
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 (missing reference).
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:
- $A$ and $B$ have all matching objects,
- for all $x \in \mathcal I$, $M_xA \times_{M_xB} B_x$ exists and the map $A_x \xrightarrow{f_x} M_xA \times_{M_xB} B_x$ discussed in (6) is a fibration.
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