FALL 2023 Program
Fridays 1-3pm in BH 150
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.
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.
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.
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.
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.
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".
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.
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.
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.
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.