Discussing "Some Properties of Fib as a Fibred 2-category"

(Link)

Author: Claudio Hermida (McGill University)

Reference: Claudio Hermida, Some properties of Fib as a fibred 2-category, Journal of Pure and Applied Algebra, Volume 134, Issue 1, 1999, Pages 83-109

Why this paper? Cited by Semantics for two-dimensional type theory and Linear Dependent Type Theory for Quantum Programming Languages

I generally try to keep the technical content of this blog relatively low; this is a bit of a challenge for a paper like this which focuses on technical development, with most applications and examples left as pointers to the literature. I will at minimum have to assume some familiarity with the mathematical field of category theory to get anywhere with this post.

This paper combines two ideas in category theory, namely fibrations and 2-categories. To get to fibrations, one can (following Chapter 1 of this PhD thesis) start with the notion of an indexed set, which can be defined as a function from a set of elements to an index set. The ‘fibres’ of a certain index are then all the elements that are mapped to that index. A fibration is the categorification of this concept – categorification is not a precise term, but is broadly the process of replacing sets with categories in one’s definitions, usually motivated by a desire for more general results. One here replaces the function between sets with a functor between categories. This move turns out to be fruitful for type theory and (typed first- and higher- order) logic because we can take our index category to be contexts and category ‘above’ to be, for example, where propositions live; the ‘fibres’ then pick out those propositions which make sense in a certain context.

What of 2-categories? One slightly amusing motivation is that sets can be considered 0-categories, ordinary categories as 1-categories, and so 2-categories are merely the categorification of the notion of a category! This makes some sense if one has spent time with categories, as one often talks not just of the categories themselves, and functors between them, but of morphisms between functors, which are called natural transformations (in fact, the historical motivation for the development of category theory was exactly to formalise the notion of natural transformation; some of the other useful terminology was invented as a by-product). The concept of 2-category then gives the general definition for a mathematical structure with that sort of three-level structure of objects, maps between objects, and maps between maps (or if not ‘the’ definition, at least a framework for such definitions, because one in fact gets a few different definitions based on how ‘lax’ or ‘strict’ one wants to be about certain equalities).

This paper’s contribution is to introduce a 2-categorical counterpart of fibrations. The paradigmatic example of such a 2-fibration turns out to be the category Fib of ordinary 1-fibrations, which is fibred over (has an appropriate functor to) the 2-category of categories. At this point one might with some justification feel one’s head start to spin, but Hermida goes on to exploit this viewpoint to prove a variety of theorems about Fib. The value of Fib, to type theory in particular, means that this paper has been steadily cited since its publication, with a modest recent uptick thanks to type theoretic interest in higher categories being driven by research in homotopy type theory.