This year, Thomas Streicher (born 1958) passed away from cancer. Thomas was one of the Greats of dependent type theory and he also wrote an excellent textbook on domain theory for denotational semantics, but much more importantly he was kind and curious and patient and always made time for young people. While I was still finding my place in the community, Thomas was very generous to me with his time and advice, and he sent me many papers to referee.
Although Thomas made many contributions to dependent type theory, domain theory, realisability theory, and category theory, he is most known to type theorists for two things—both in collaboration with the late Martin Hofmann: the groupoid interpretation of type theory and the eponymous Hofmann–Streicher universe lifting construction. Andrew and my paper pertains to the latter.
The idea of Hofmann–Streicher lifting has to do with universes, which are “types of types” (typically defined in such a way as to avoid paradoxes). Martin-Löf type theory usually includes universes in order to be able to quantify over (small enough) types; in the simplest models of Martin-Löf type theory, types are interpreted as sets and so Martin-Löf’s universes are interpreted as certain sets of sets, such as Grothendieck universes. But it is important to be able to interpret the language of type theory in more sophisticated worlds than set theory: for example, in presheaves (which are functors from a fixed category into ). What Hofmann and Streicher did is show how to transform any universe of sets into a universe of presheaves!
Although Hofmann and Streicher’s construction worked well and had good properties, they did not find a universal property for it—which is an abstract description of the object that determines it uniquely up to isomorphism, usually in terms of how it relates to other objects. Recently Awodey found a 1-dimensional universal property, which was the starting point of our work. What Andrew and I wanted to do is generalise Awodey’s analysis in two directions:
- We wanted a 2-dimensional version, which is useful because it captures more about the universe than can be said in just one dimension: for example, with a 2-dimensional version, you can see immediately (by “abstract nonsense”) that Hofmann–Streicher lifting preserves structures like monads, adjunctions, etc. that might be used for modelling computational effects, etc.
- We wanted a relative version, which would make it easier to iterate the Hofmann–Streicher lifting construction: the purpose of this is to be able to define presheaf models of type theory internal to other presheaf models. These kind of situations actually happen in practice! For example, the model of guarded cubical type theory that combines step-indexing with univalence ought to be an example of this.
To develop this two-fold generalisation of Hofmann–Streicher lifting, we resituated the theory in terms of another of Thomas’s favourite topics: the theory of fibrations, on which Thomas had written the most wonderful lecture notes.
We dedicated our paper to Thomas’s memory. May he rest in peace.