19
$\begingroup$

I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/programs. So I guess it is some implementation/semantic specific stuff and "fibration" seems related to Pi types, and "cofibration" to intervals?

I'm also curious about their intuitions/origins. It's always cool but kinda confusing to see these categorical constructs in the implementation for some naive code readers like me.

$\endgroup$
1
  • $\begingroup$ I think the 'fibration' part comes from the fibration-based model of dependent type theories, for example comprehension categories. $\endgroup$
    – ice1000
    Commented Mar 17, 2022 at 20:51

2 Answers 2

14
$\begingroup$

So, first, the origin of this term in the context of cubical type theory comes from its intended semantics, which are in turn inspired by the model-categorical semantics of homotopy type theory. Let's start with the model-categorical semantics of HoTT.*

These models work by interpreting types as a fibration (in the sense of model categories) $p_A : \Gamma.A \to \Gamma$.** Now, the rather than recapitulating the definition of a model category here, let me just say that fibrations are a class of morphisms satisfy a lifting property against another class of morphisms (trivial cofibrations).

For instance, in the original semantics of HoTT in simplicial sets, fibrations are Kan fibrations: maps which lift against inclusions $\Lambda^n_i \to \Delta^n$ (the generating trivial cofibrations). One important observation here is that trivial cofibrations are monomorphisms. Accordingly, the fact that $p_A : \Gamma.A \to \Gamma$ is a fibration can be rephrased to say that there is a particular class of propositions $\Gamma \vdash \phi : \Omega$ and any element $\Gamma.[\phi] \vdash M_\phi : A$ can be somehow extended to an element $\Gamma \vdash M : A$.

OK, that's HoTT, let's go back to cubical type theory (the theoretical underpinnings of cooltt). Taking inspirations from these models of HoTT, cubical type theory asks that types be equipped with an explicit algorithm showing types are fibration. This is a break from HoTT, where all this fibrancy and model categorical stuff was hidden away beneath identity types and univalence. With cubical type theory, this structure is made explicit. The fact that types are intended to be modeled by "fibrations" is manifested through the "composition structure" each type is equipped with. These essential equip each type with a lifting operation against "trivial cofibrations". The class of special propositions in cubical type theory is precisely meant to internalize the special propositions (monomorphisms) which we wish to think of as cofibrations.

A natural question is why these are cofibrations when types (fibrations) should only lift against trivial cofibrations. Well, remember that the composition operation in cubical type theory requires you to provide more than just a partial element $\phi \mapsto M_\phi$, you must also provide a "base" for your box, so in total you're providing a partial element for more than just $\phi$. If we look back to the case of simplicial sets, we are essentially using the fact that for any cofibration $A \hookrightarrow B$, the monomorphism $(\{0\} \times B \coprod_{\{0\} \times A} \Delta^1 \times A) \hookrightarrow \Delta^1 \times B$ is a trivial cofibration. The composition operation in cubical type theory morally lets you indicate $A \hookrightarrow B$ and then forces you to provide a partial element for the trivial cofibration akin to $(\{0\} \times B \coprod_{\{0\} \times A} \Delta^1 \times A) \hookrightarrow \Delta^1 \times B$.

That "morally" in the previous sentence is doing a bit of work. How much work is actually an interesting research question: is there a model structure on the intended models of cubical type theory for which types are fibrations and cofibrations/trivial cofibrations are the expected maps? The answer is slightly complicated (some references) but yes, you can formally substantiate the intuitions I sketched above into a genuine model structure on cubical sets so the intended semantics of cubical type theory realizes types as fibrations and cofibrations as.. cofibrations.

The next interesting question we can ask with such a model structure is what the homotopy theory of cubical type theory looks like. (This is actually the primary motivation for model structures in the first place!) I believe the very frontier of research on this topic indicates that many varieties of cubical type theory have a model in a model category which is Quillen equivalent to spaces, a crucial fact for arguing that the synthetic homotopy theory carried out in cubical type theory "means the right thing".


*In other corners of type theory, "fibration" is meant to draw a connection to structures different from what I describe here. Unfortunately fibration is a word mathematicians love to use, so it has innumerable related but subtly different definitions.

** In fact, these ideas pre-date modern HoTT/univalence with Awodey and Warren recognizing the importance of this idea for intensional identity types.

$\endgroup$
10
$\begingroup$

Let me provide a slightly watered up supplement of Gratzer's answer.

In the beginning, mathematicians need to study spaces by considering how other spaces cover(*) them. For example, if you have a line and a circle, you can wind up that line around the circle completely. In mathematical terms, you are given $\mathbb R$ and $\mathbb S = \{z\in\mathbb C: |z|=1\}$. You can wind it up with $x\mapsto e^{ix}$. This is good because locally, i.e. in a small area $U$ around each point, this map looks like the projection function $\mathbb Z \times U \xrightarrow{\pi_2}U$.

I'll steal a picture here:

Covering space

Note that if you restrict your attention on a small region around one of the black arrows (the space "above" a point in $\mathbb S$), it just looks like $\mathbb Z$ copies of the same thing overlaid on that region.

Now, what's good about it? Generally, we want to study the geometry of the base space $\mathbb S$ by "projecting" down from the total space $\mathbb R$. So we need the covering to be relatively well-behaved. For instance, when we are studying paths, we may want to require the property that, no matter how I walk along the base space, you can follow along in the total space, while keeping yourself strictly above me. As an example (lots of examples!), if I start at $\color{blue}1$, and you start at $\color{red}{-1}$; when I go counterclockwise along $\color{blue}{1 \to i \to -1 \to 1}$, you must follow along. And you can: $\color{red}{-1\to-\frac34\to-\frac12\to0}$.

Actually, a notion that came earlier is fiber bundles, which puts a stricter requirement: If you look at a small enough region, then the whole thing just looks like $F \times B \to B$. This is slightly easier to work with, but it is too restrictive in our use cases.

To formalize the notion of fibration, we can use a continuous function $[0,1]\to B$ to represent a path in $B$. Also, we have a point $*\xrightarrow0 [0, 1]$. (Using an arrow from a singleton space to another space is a common category speak to "pinpoint" a point in space; Here we want to get the point $0$. Also, I use $*$ instead of the categorical $1$, because it clashes with the real number $1$ here.) We start with a path $q:[0, 1]\to B$, and a "covering" $p:E\to B$ (our picture above is a covering $\mathbb R \to \mathbb S$). We also specify our starting point in $E$ with an arrow $*\to E$. This starting point must lie above our starting point of the path $q$ in the base space. So it can be written in a commutative diagram:

$$ \begin{matrix} *&\to&E\\ \downarrow & & \downarrow\\ [0, 1]&\color{blue}{\xrightarrow q} & B \end{matrix} $$

By saying that "you can follow along the path $q$ in $E$", we really mean that you can lift the path into $\hat q : [0, 1]\to E$, and the commutativity of the diagram ensures that this lifted path lies "above" the original one. So:

$$ \begin{matrix} *&\to&E\\ \downarrow &\color{red}{\nearrow} & \downarrow\\ [0, 1]& \color{blue}{\to}& B \end{matrix} $$

In this case, we say that the arrow $p$ lifts against the arrow $*\xrightarrow 0 [0,1]$. But of course, we may wish to use other arrows than $0$. So in general, if $p$ lifts against a certain set of arrows, we call $p$ a fibration.

On the other hand, we can consider the dual notion. Since fibrations are really good coverings, by reversing the arrows, we get that cofibrations are really good inclusions.

We invert our diagram:

$$ \begin{matrix} Y&\leftarrow&B\\ \uparrow &\color{red}{\swarrow} & \uparrow\\ X& \color{blue}{\leftarrow}& A \end{matrix} $$

Here $X \to Y$ is some other given arrow which we want to "colift" against. This is called an extension property. The archetypical example is when $X \to Y$ is $S^{[0,1]} \xrightarrow {p_0} S$, which maps each path in the space of paths in $S$ to its starting point. Suppose $A = *$, and $* \to B$ is a point of $B$, then the commutative square gives

$$ \begin{matrix} S&\leftarrow&B\\ \uparrow &\color{red}{\swarrow} & \uparrow\\ S^{[0,1]}& \color{blue}{\leftarrow}& * \end{matrix} $$

  • A map $\color{blue}{H : * \to S^{[0,1]}}$, which is equivalent to a path $\color{blue}{[0,1] \to S}$.
  • A map $B \to S$, mapping $B$ inside $S$.

The extension property gives the diagonal arrow $\color{red}{B \to S^{[0,1]}} \cong B \times [0,1] \to S$, which describes how $B$ "moves" continuously in $S$. $\color{blue}H$ gives the trajectory of a single point of $B$. So the extension property roughly says that, whenever you have the starting position of $B$, and describe how a single point moves inside $S$, then you can always "drag $B$ along that trajectory". Another way to put it is you can always extend the orbit of the point to the orbit of the whole of $B$.

Of course, extension of a point sounds trivial. But we can immediately create another example: If you replace $A = *$ with $A = 2$, the space with two points, then the extension property says that given the trajectory of two points, you can always extend the trajectory to the whole of $B$.

This is very useful in type theory. Suppose you have proved three equalities:

$$ \begin{matrix} a&&d\\ \|& & \|\\ b& =& c \end{matrix} $$

In cubical type theory, this is represented as three paths, similar to $[0,1] \to X$. To compose them, you invoke a version of the extension property: Let $B$ be the path $b=c$, and you have the trajectory of the two endpoints $b$ and $c$: they move to $a$ and $d$, respectively. Now "dragging $B$ along", you will end up with a path $a = d$. This is how path composition is proved (**).

(*): Covering spaces is a related term, but I don't want to talk too much about that. I'm using this word to represent intuition.

(**): In some flavors of CuTT, at least. There are type theories that try to achieve this with different methods.

$\endgroup$
5
  • $\begingroup$ I was slightly thrown by the explanations of cofibrations, where you've used $\Lambda \to \Delta$ as a stand-in for a trivial fibration? Other than that, a lovely explanation of the geometric motivation for fibrations! Perhaps it's worth mentioning to the curious reader that these properties are meant to be an abstraction of fiber bundles, which are ubiquitous in geometry. $\endgroup$ Commented Mar 18, 2022 at 10:12
  • $\begingroup$ @DanielGratzer Thanks for the correction! I was probably having a bad day. I expanded my answer a little bit now. $\endgroup$
    – Trebor
    Commented Mar 18, 2022 at 11:54
  • $\begingroup$ Ha, if this is the worst oversight you make on bad days then I envy you! I'll go back to making basic arithmetic errors and wondering how I've deduced $\bot$... And the updated version seems very nice! $\endgroup$ Commented Mar 18, 2022 at 12:44
  • $\begingroup$ Not a large enough change to submit an edit, but the paragraph after your image could probably use a line break before it. Otherwise, at least on my screen, "Note" gets wedged next to the image. $\endgroup$
    – Tyberius
    Commented Mar 18, 2022 at 15:06
  • $\begingroup$ @Tyberius Fixed. I was editing on my phone so I never noticed :P $\endgroup$
    – Trebor
    Commented Mar 18, 2022 at 15:25

Not the answer you're looking for? Browse other questions tagged or ask your own question.