FALL 2023 Program
Fridays 1-3pm in BH 150
September 1, Welcome to new students
September 8, Steve Awodey — Homotopy Type Theory
A new branch of logic called Homotopy Type Theory was founded in the Philosophy Department at CMU and has flourished there in the intervening 15 years. This talk will survey the historical, philosophical, and logical background leading up to the invention of HoTT, and trace some of the challenges and advances that have marked its subsequent development. This is a non-technical talk, intended for a general audience.
September 15, Mathieu Anel — ∞-Loop spaces and Spectra
I will recall a few things about chain complexes, homology and cohomology to introduce spectra. I will then take a more abstract point of view and define spectra by means of ∞-loop spaces.
September 22, Jacob Neumann — Paranatural Category Theory
What is the appropriate notion of transformation between "difunctors", that is, between functors of the form C^op × C → Set? In this talk, we'll examine several applications in the semantics/metatheory of functional programming and type theory where we find ourselves in a "Goldilocks"-type situation: the usual notion of natural transformation is too narrow (excluding the examples we're interested in) and standard notions of 'diagonal natural transformation' are too broad (so broad, indeed, that they fail to be closed under composition). I'll talk about the notion which I think is 'just right': strong dinatural transformations. Strong dinatural transformations (which I advocate for rechristening as 'paranatural transformations') are a concept neglected in the present literature, I claim, and one which can serve as the centerpiece of a striking and widely useful mathematical theory (which I dub 'paranatural category theory'). I hope to bring attention to some of the basic results in this fascinating branch of category theory, and instigate further research into it.
A preprint covering this material is available at arxiv.org/abs/2307.09289.
October 6, Jonas Frey — The shape of contexts in type theory
Contrary to simple type theory, the variables in a context in dependent type theory cannot be arbitrarily permuted, since the types of variables further right may depend on variables further left. However, considering dependent contexts to be always linearly ordered is a simplification, since later variables do not have to depend on all earlier variables, in particular simply typed contexts are a special case of dependently typed contexts. While a first attempt at a framework containing both unordered and linearly ordered shapes would be to use finite posets, in this talk I explain why it is better to use finite direct categories (FDCs), and outline some important properties of the category of FDCs and discrete fibrations.
October 13, David Forsman — Algebraic structures on categories and their coherence
We define a signature and associated algebraic theories, which will be modeled in the setting of categories. Freely completing some initial data into a model of an algebraic theory will build a type theory. Type theories of this form allow formulations of coherence theorems in the style of Mac Lane. We will revisit the coherence of monoidal categories, proven by Mac Lane, and comment on the coherence properties of the cartesian monoidal categories.
If time allows, we comment on how to upgrade the defined language into a predicate logic and formulate questions of completeness, in the sense of Gödel, of different categorical settings. A question of interest is the completeness of the universe categories itself.
October 20 — No seminar (fall break)
October 27, Kian Cho — The Algebraic Small Object Argument
An algebraic weak factorization system uses a comonad and a monad to encode a uniform choice of lifts of left maps against right maps. We are interested in "cofibrantly generating" an algebraic wfs, but from a category of maps instead of a set of maps. The free (a badly behaved generalization of "cofibrantly generated") algebraic wfs is obtained through reflecting the category of maps along a sequence of forgetful functors. At the end, we are going to see a transfinite construction similar to the usual small object argument. All of this is based on Garner's 2008 paper "Understanding the small object argument".
November 3, Egbert Rijke — Decisions and descent
In this talk I would like to present several examples of cases where univalence was used in order to bypass applications of the law of excluded middle or the axiom of choice. Some of these examples are well known, such as the fact that functors between univalent categories are equivalences if and only if they are essentially surjective and fully faithful. Another example on this theme comes from a recent theorem of David Wärn, which solved the open problem of whether the suspension of a set is a 1-type. In a third example, we present an example of a nontrivial acyclic type that classifies Higman's group. The traditional proof that Higman's group is nontrivial passes through combinatorial group theory, with lots of decision making along the way. Our proof that Higman's type is noncontractible makes use of the descent property and bypasses combinatorial group theory entirely.
November 10, Reid Barton — Normed Homological Algebra
Normed homological algebra is a variant of ordinary homological algebra in which equations are systematically replaced by approximations with error bounds of a specific form. It is a useful organizational framework for certain computations with condensed abelian groups, and a more complicated version is used in the proof of the "main theorem of liquid vector spaces" of Clausen and Scholze. I will explain how normed homological algebra can be seen as ordinary homological algebra internal to the "Lipschitz topos", a variant of the topos for continuous logic of Figueroa and van den Berg. This talk is based on joint work with Johan Commelin.
November 17, Jure Taslak — Type theory of Enumerion
Disclaimer: This is a WIP. Enumerion is a system for systematically enumerating finite discrete mathematical structure. In the talk I'm going to try to motivate why such a system could be useful, describe the type theory underlying it, give a few examples of defining finite structures in such a system and define a groupoid model of the type theory. Time permitting I'm going to show a short demo of the current state of the system.
November 24 — No seminar (Thanksgiving)
December 1, Raffael Stenzel — General and diagrammatic comprehension schemes over ∞-categories
We define a general comprehension scheme over an oo-category B to be but a representable natural transformation of presheaves over B. One can motivate this definition in terms of the ordinary categorical semantics of type theory. We hence will take a look at the structural theory of such general comprehension schemes in this light, and then define and study a class of comprehension schemes that we call the ``(standard) diagrammatic'' ones. This latter class of comprehension schemes captures all examples of ``generalized'' comprehension schemes that Johnstone considers in the Elephant (over a 1-category). It also captures all specific instances of comprehension schemes that are introduced by Benabou in his paper on ``Fibered categories and the foundations of naive category theory''. In fact, we will make the point that his ``categories'' can be interpreted to be fibered ∞-categories. In doing so however some of his concerns regarding the definability of identity become vacuous. The theory of standard diagrammatic ∞-categorical comprehension schemes is generally in fact much better behaved than its ordinary categorical counterpart, and subsumes a plethora of examples some of which we will discuss during the talk.
Earlier seminars are listed here.