FALL 2023 Program
December 12, Simon Henry — Prodiscrete locales as a procompletion
It is well known that the procompletion of the category of finite sets is the category of profinite spaces (i.e. Stone spaces). But the similar result for the procompletion of arbitrary sets and pro-discrete spaces doesn't hold. In this talk, I will explain how using Locales one can get a result in this vein: The category of prodiscrete locales (i.e. Strongly zero-dimensional locales) is the "extensive procompletion" of the category of sets, i.e. the initial category which is both complete and (infinitary) extensive. I will also show how for every infinitary extensive category C we obtain a "pi_0" functor from C to the category of prodiscrete locales (the right adjoint to the universal functor from the claim above).
December 8, Reid Barton — Proper and etale maps of condensed sets
Many mathematical objects (such as the real numbers or p-adic numbers) have a nontrivial "natural" topology, traditionally thought of as additional structure on an underlying set, which in turn determines a notion of continuous maps between such objects. Condensed sets form a topos which is sufficiently similar to the category of topological spaces that constructions in condensed sets tend to already produce objects with the "correct" maps, without the need for additional structure. After a brief motivation and introduction to condensed sets, I will define two classes of morphisms that correspond to the proper maps and the local homeomorphisms in topology, and describe relationships between these two classes. There may also be some speculation on the nature of this structure. This is work in progress with Johan Commelin.
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.
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 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 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.
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".
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 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.
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.
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 8, Steve Awodey — Homotopy Type Theory (Philosophy Department Colloquium)
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.
SPRING 2023 Program
May 5, Steve Awodey Cartesian cubical model categories
The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.
April 28, Owen Milner Formalizing the Whitehead tower in cubical agda
This talk will present details of a formalization, in cubical agda, of the key properties of the Whitehead tower. The material formalized includes the definition of the Whitehead tower, a proof of that its objects satisfy a universal property, the computation of their homotopy groups, and the identification of the fibers of the structure maps of the tower as particular Eilenberg-MacLane spaces.
April 21, Greg Langmead Towards gauge theory in homotopy type theory
Gauge theory is the study of connections on smooth manifolds, and the solution set of functions defined on the space of connections. Sometimes these functions have terms coupling connections to sections of associated vector bundles, as in the standard model of particle physics. The starting point of gauge theory is the theory of principal bundles and their isomorphisms. I will remind us of the theory of higher groups in homotopy type theory and how we can think of deloopings as classifying spaces for principal bundles. I will show some related types that emerge from deloopings and which let us move around inside a space of symmetries, using identity types. Then I will show some work in progress to define connections and curvature using the modalities of real cohesion together with the delooping.
April 7, Astra Kolomatskaia Displayed Type Theory and Semi-simplical types
We introduce Displayed Type Theory (dTT), a multi-modal two-layered type theory whose outer layer consists of types with augmented semi-simplicial structure. The simplicial structure is exposed to the user via the fully computational parametric operation ᵈ (called display or dependency). The inner “discrete layer” represents the universe of homotopy type theory and conjecturally has semantics in any infinity-topos. It is possible to construct semi-simplicial types in the “simplicial layer” and subsequently to reflect them into the discrete layer via the fully computational modality ◇. Upon doing this, the definition of semi-simplicial types unfolds into infinitely many mutually recursive definition in the language of Book HoTT.
March 24, Claymont retreat — no seminar
March 13, 20, 27, Denis-Charles Cisinski, Hoang Kim Nguyen, Tashi Walde — Univalent Directed Type Theory
We will introduce a version of dependent type theory that is suitable to develop a synthetic theory of 1‑categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)‑category theory (under the form of quasi-categories or complete Segal spaces) gives a semantic interpretation, in a way which extends Voevodsky's interpretation of univalent dependent type theory in the homotopy theory of Kan complexes. More generally, using a slight generalization of Shulman's methods, we should be able to see that the theory of (∞,1)‑categories internally in any ∞‑topos (as developed by Martini and Wolf) is a semantic interpretation as well (hence so is parametrized higher category theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links with ∞‑cosmoi of Riehl and Verity as well as with cubical Hott (as strongly suggested by the work of Licata and Weaver), or simplicial Hott (as in the work of Buchholtz and Weinberger). We will explain the axioms in detail and have a glimpse at basic theorems and constructions in this context (Yoneda Lemma, Kan extensions, Localizations). We will also discuss the perspective of reflexivity: since the theory speaks of itself (through directed univalence), we can use it to justify new deduction rules that express the idea of working up to equivalence natively (e.g. we can produce a logic by rectifying the idea of having a locally cartesian type). In particular, this logic can be used to produce and study semantic interpretations of Hott.
Talk 1: video, slides intro, slides talk
Talk 2: video, slides
Talk 3: video, slides
March 3, Andrew Swan — Oracle modalities
I give a new definition of function computable relative to an oracle, based on the classic result by Hyland that Turing degrees embed into the lattice of subtoposes of the effective topos. Higher modalities in homotopy type theory play a key role at every step. Justified by realizability semantics, we can assume that all functions N -> N are computable. In order to talk about functions that are not necessarily computable we use the modality of double negation sheafification. We think of functions in double negation sheaves, which we refer to as *oracles*, as external functions in sets that we can construct and reason about using classical logic. We say the *oracle modality* for an oracle is the smallest modality forcing the oracle to be total, and think of functions in the corresponding reflective subuniverse as computable relative to the oracle. By augmenting HoTT with certain axioms we can do some basic synthetic computability theory, including some reasoning about programs that use unbounded search using the new axiom of *Markov induction*. I also give a simple definition of homotopy group for a Turing degree and prove that two Turing degrees are equal as soon as they have isomorphic homotopy groups.
February 24, Jonas Frey — « Seminar Surprise »
February 17 (10am on Zoom), Eric Finster — The (∞,1)‑category of Types
A major outstanding difficulty in Homotopy Type Theory is the description of coherent higher algebraic structures. That is, well-behaved algebraic structures on types which are not assumed to be truncated. A classic example which motivates the desire to define such structures is the universe of type theory itself. Indeed, it is well known that the natural structure possessed by types and functions between them is not an 1-category, but rather an (∞,1)‑category. Expressing this fact appears to required principles which go beyond the standard presentation of MLTT.
In this talk, I will describe how the addition of a finite collection additional definitional equalities designed to render the notion of "opetopic type" definable in fact allows one to construct the (∞,1)‑category structure on the universe of types.
slides
February 10, Pietro Sabelli — Revisiting the equivalence between theories and models of dependent type theory using Curien’s explicit syntax
A good notion of semantics for a type theory calculus should give rise to an equivalence between theories and models through the syntactic category/internal language constructions. In the case of dependent type theory, Pierre Clairambault and Peter Dybjer proved in detail that Martin-Löf's type theories and locally cartesian closed categories are equivalent. There, the syntax is presented as a generalized algebraic theory. Motivated by the goal of finding suitable semantics for the intensional level of the Minimalist Foundation, I am working on a formalization in Agda of an analogous result using Curien’s explicit syntax. I will argue that this syntactical choice can give us insights into categorical semantics, in particular concerning the coherence problem.
February 3, Wentao Yang — Deligne's completeness theorem
Deligne's theorem states that any coherent topos has enough points. The theorem can be viewed as a completeness theorem when specialized to the classifying topos of a geometric theory. First we explain this connection to logic and then present a proof of Deligne's theorem.
January 27, Henrik Forssell — Locales of models and the definability theorem for coherent logic
In his PhD Thesis (Stockholm University), Johan Lindberg gave an explicit description of the Joyal-Tierney representation theorem in terms of locales of models of geometric theories. We revisit this description and show an example application of it by giving a constructive formulation and proof of the Definability Theorem for coherent logic (Elephant, D3.5.1).
Johan Lindberg's Thesis
2022 Program
December 2, Jonathan Weinberger — Generalized Dialectica constructions via Skolemization
In the late 1950s, Gödel presented the Dialectica interpretation, a proof translation used to prove the consistency of intutionistic arithmetic relative to System T. Valeria de Paiva, in the late 1980s, introduced a categorical version of the Dialectica construction. This got extended and investigated on the level fibered categories in the works of Hyland, Biering, Hofstra, von Glehn, and Moss. In particular, in recent work Trotta--Spadetto--de Paiva showed that the ensuing notion of Dialectica fibration can be characterized via the existence of enough quantifier-free objects. This in particular entails the validation of a Skolem principle. We present work in progress to generalize this setting to a wider notion, with the aim of establishing an analogous characterization of a dependent version of Dialectica fibration over a display map category. This is joint work with Davide Trotta and Valeria de Paiva.
November 11, Philip Sink, Brittany Gelb — Modal Logic Without Possible Worlds
We will present a semantics for modal logic based on simplicial complexes that instead of possible worlds uses an "Agent Perspective". Philip will explain the details of the formalism, including a novel soundness and completeness proof exploiting the intuition of "knowledge as paths''. Brittany will follow up with some applications of these models to a distributed computing setting. Additionally, she will show how we can use tools from algebraic topology to study bisimulations.
November 7, 10am, (special online seminar), Sam Speight — Higher-dimensional realizability for intensional type theory
I will describe recent work on higher-dimensional realizability models of intensional type theory. The idea is that these models formalize a BHK reading of the topological/homotopical interpretation of type theory, analogous to how traditional realizability models formalize the usual BHK interpretation. The models are based on groupoids (as opposed to sets), but the key point is that realizers themselves carry higher-dimensional structure, so that a realizer of a path is a path between realizers.
October 26, Simon Henry — Factorization system on model categories and two-level model structures
I'll discuss a work in progress whose general idea is to study weak factorization systems and model structure on an infinity category E in terms of a presentation of E by a model category M. More precisely, given M a model category, and E the infinity category it presents, I'll explain how under various assumptions one can go back and forth between nice factorization systems on M and factorization systems on E, and between nice model structures on M and model structures on E. This will allow us to extend definitions and theorems on model categories and factorization systems developed in the 1-categorical case to the infinity categorical setting without too much effort.
October 14, Andrew Swan — Double negation stable h-propositions in cubical sets
When working in a constructive setting without the axiom of choice, models of type theory based on model structures, such as simplicial sets and cubical sets, make a strong distinction between propositions internal to the type theory (called homotopy propositions or just h-propositions) and propositions in the underlying locally cartesian closed category, which are just monomorphisms. Double negation stable h-propositions are an important exception to this - they are equivalent to monomorphisms. We use this to show cubical sets satisfy a restricted form of propositional resizing that applies only to double negation stable h-propositions. This restricted version suffices to show the Dedekind real numbers exist in cubical sets, and to formulate and show the consistency of an extended version of Church's thesis for partial functions ("all partial functions with double negation stable domain are computable"). This is based on a paper appearing at https://arxiv.org/abs/2209.15035.
August 12— Steve Awodey — Algebraic type theory (exceptional time 3pm)
A type theoretic universe U* —> U bears an algebraic structure resulting from the type-forming operations of unit type, identity type, dependent sum, and dependent product, which may be generalized to form the concept of a "Martin-Löf algebra". A free ML-algebra is then a model of type theory with special properties. The theory of such ML-algebras can be seen as a proof-relevant version of the theory of Zermelo-Fraenkel algebras from the algebraic set theory of Joyal-Moerdijk. (Work in progress)
July 12— Chaitanya Leena Subramaniam — Contexts as computads, linear dependent types, and dependent symmetric multicategories
Certain multisorted algebraic theories (a.k.a. cartesian multicategories) can be described by coloured Set-operads (a.k.a. symmetric multicategories). These are exactly those algebraic theories that are "linear" or "regular" --- namely, they admit presentations by equational theories where for each axiom/equation Γ⊢t=u, every variable of the context Γ appears exactly once in each of the terms t and u. When C is a direct category, finitary monads on [C^op, Set] correspond to certain contextual categories, and these provide a good candidate for the class of "dependent cartesian multicategories". In this talk I will describe work in progress towards characterising the subclass that arise from "dependent symmetric multicategories" or "linear dependently typed algebraic theories". This approach is a generalisation of a technique due to Weber, following Joyal and Girard, that characterises linear multisorted algebraic theories as those whose syntactic categories have "(free,generic)" factorisations. Our work arises from the following observation: while the objects of a contextual category are not necessarily free algebras, they are generalised computads --- and the left maps of the factorisations in question are the computad morphisms. These are better-known as the context morphisms that are variable renamings, and context morphisms that are right orthogonal to them are the elusive "linear dependently typed context morphisms". (joint work in progress with Simon Henry)
May 12 — Mike Shulman — Towards a Third-Generation HOTT (Part 3 of 3)
11:30am-1:00pm EST (UTC-04:00)
Zoom link: https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: the Brunerie number
Slides, Video
May 11 — Egbert Rijke — Univalent main classes of latin squares
A common theme in combinatorics is to count the number of objects of some kind, up to a naturally defined equivalence relation. A common theme in univalent mathematics is that when you define the type of objects of some kind, then the identity type is a naturally defined equivalence relation. There is clearly a match between these two subjects. I'll illustrate my approach to univalent combinatorics to a definition of the groupoid of main classes of latin squares, in which two latin squares are considered to be equivalent of one can reached from the other by some permutation of the set {r,c,s} denoting the rows, columns, and symbols, and permutations of the rows, columns, and symbols themselves. We will also introduce the notion of pi-finiteness, which can be used to show efficiently that a type has finitely many connected components and to show that all its homotopy groups up to a given level are finite. This notion has been used to construct the OEIS sequence A000001 of the number of isomorphism classes of groups of order n, and the sequence A003090 of main classes of latin squares, among other sequences. Our definitions of these sequences make heavy use of the univalence axiom, and so far any computations using the cubical Agda proof assistant have been unsuccessful.
May 10 — Fernando Larrain Langlois — Normalization of Lambda-calculus
May 6 — Wentao Yang — Some relations between μ-abstract elementary classes and accessible categories
We will investigate the relationship between μ-abstract elementary classes, which are generalizations of AECs by requiring only μ-directed unions to exist, and accessible categories, which are categories generated by certain “small” objects under μ-directed colimits.
May 5 — Mike Shulman — Towards a Third-Generation HOTT (Part 2 of 3)
11:30am-1:00pm EST (UTC-04:00)
Zoom link: https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: the Brunerie number
Slides, Video
April 29 — Reid Barton — Finite presentability of homotopy groups of spheres
Serre proved that the homotopy groups of spheres are finitely presented as one application of what we now call the Serre spectral sequence. I will outline a proof of the same theorem using "low-tech" methods. Based on joint work with Tim Campion.
April 28 — Mike Shulman — Towards a Third-Generation HOTT (Part 1 of 3)
11:30am-1:00pm EST (UTC-04:00)
Zoom link: https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: the Brunerie number
Slides , Video
In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure; but many desired equalities are not definitional, and univalence must be asserted by a non-computational axiom. Cubical type theories also define identity uniformly, but using paths instead. This makes more equalities definitional, and enables a form of univalence that computes; but requires inserting all the higher structure by hand with Kan operations.
I will present work in progress towards a third kind of homotopy type theory, which we call Higher Observational Type Theory (HOTT). In this system, identity is not defined uniformly across all types, but recursively for each type former: identifications of pairs are pairs of identifications, identifications of functions are pointwise identifications, and so on. Univalence is then just the instance of this principle for the universe. The resulting theory has many useful definitional equalities like cubical type theories, but also gives rise to higher structure automatically like Book HoTT. Also like Book HoTT, it can be interpreted in a class of model categories that suffice to present all Grothendieck-Lurie (∞,1)-toposes; and we have high hopes that, like cubical type theories, some version of it will satisfy canonicity and normalization.
This is joint work with Thorsten Altenkirch and Ambrus Kaposi.
April 22 — Owen Milner — Quillen equivalence between SSet and Top
April 15 — Kian Cho — Introduction to model categories
April 8 — No seminar (ASL meeting)
April 1 — Maru Sarazola — Introduction to K-theory
This talk will be a brief introduction to algebraic K-theory from a category theorist's point of view; that is, from someone who enjoys to study structures and universal properties much more than computations or concrete applications. We will go over some of the history of algebraic K-theory, starting in the 50's, and moving on to a more modern perspective. After describing several possible inputs for algebraic K-theory, we will define the K-theory of a ring, and show how this can be generalized to define the K-theory of a Lawvere theory.
March 25 — Steve Awodey — Kripke –Joyal semantics for type theory
We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. This is jww/ Nicola Gambino and Sina Hazrathpour, available as arXiv:2110.14576.
March 18 — Michele Contente — On the relationship between MF and HoTT
The goal of this talk is to provide an introduction to the Minimalist Foundation, a two-level type theory introduced by Maietti and Sambin, and to investigate its relationship with HoTT. In particular, I will discuss an interpretation of both levels of MF in HoTT and some problems related to this interpretation. If time permits, I will introduce an extension of MF with rules for inductively generated formal topologies and describe how these rules may be interpreted in HoTT. This is based on joint work (in progress) with Milly Maietti.
March 11 — No seminar (weekend in Claymont)
March 4 — Sina Hazratpour — A 2-Categorical Proof of Frobenius in HoTT
In the context of models of HoTT, the Frobenius condition says that the pushforward along fibrations preserve fibrations. This is used for the interpretation of dependent product (Π) types. Coquand gave a simple constructive proof of Frobenius in Cubical Type Theory, taking advantage of the fact that fibration structures can be reduced to composition structures. We give a 2-categorical proof of the Frobenius condition guided by the category-theoretic proofs by Gambino & Sattler and by Awodey. This is based on joint work with Emily Riehl.
February 25, Reid Barton — The rank and size of locally presentable categories
This talk will describe the viewpoint on locally presentable categories as the cocomplete categories that admit small presentations as cocomplete categories. We will discuss the two notions of rank and size of a locally presentable category, and describe how they relate to the various characterizations of locally presentable categories.
February 11, Jonas Frey — Characterizing clan-algebraic categories
Clans provide a categorical notion of dependent algebraic theory that can be seen as syntax-free abstraction of Cartmell’s generalized algebraic theories and as such is closely related to concepts like contextual categories and categories with families. Viewed as algebraic theories, clans are equally expressive as finite-limit theories but contain more information: the same finite-limit theory can have representations by different clans, and in particular different clans can have the same category of Set-models. The additional information encoded in a clan T gives rise to a weak factorization system (E,F) on the locally finitely presentable category Mod(T) (first considered by Henry), from which the clan can be reconstructed up to Morita equivalence. In earlier work I conjectured a characterization of “clan-algebraic categories” -- i.e. lfp categories equipped with a wfs arising as models of a clan -- in terms of an exactness condition that generalizes an analogous characterization of categories of models of ordinary algebraic theories. In this talk I give a proof of this conjecture, and illustrate the exactness condition by means of examples.
February 18, Rio Alvaro Jackson — Accessibility, Presentability & Adjointness
The goal of this talk is to provide an introduction to three core topics (as above) central to a more modern approach to category theory. In particular, I will discuss how these centrals notions allow for elegant characterizations and generalizations of well-established patterns in, e.g., algebra in the form of finitely generated abelian groups, as well as providing a workable solution to some size issues. Moreover, I will demonstrate a relatively concise proof of the Adjoint Functor Theorem using these same tools.
February 4, Carlo Angiuli — Normalization, logical frameworks, and the LCCC of judgments (part 3)
The purpose of this three-lecture series is to provide some general background for the normalization result for cubical type theory recently established by Sterling and myself (https://arxiv.org/abs/2101.11479).
I will begin by defining (reduction-free) normalization, and motivating its importance to the implementation of proof assistants. Next, I will recall Awodey's natural models of type theory and explain how the internal language of a presheaf topos is a "logical framework" in which one can define the theory of MLTT with connectives. Then, I will review Uemura's representable map categories and second-order generalized algebraic theories, before concluding with the locally Cartesian closed category of judgments, a perspective recently advocated by Gratzer and Sterling.
2021 program
December 10, Carlo Angiuli — Normalization, logical frameworks, and the LCCC of judgments (part 2)
December 3, Carlo Angiuli — Normalization, logical frameworks, and the LCCC of judgments (part 1)
The purpose of this two-lecture series is to provide some general background for the normalization result for cubical type theory recently established by Sterling and myself (https://arxiv.org/abs/2101.11479).
I will begin by defining (reduction-free) normalization, and motivating its importance to the implementation of proof assistants. Next, I will recall Awodey's natural models of type theory and explain how the internal language of a presheaf topos is a "logical framework" in which one can define the theory of MLTT with connectives. Then, I will review Uemura's representable map categories and second-order generalized algebraic theories, before concluding with the locally Cartesian closed category of judgments, a perspective recently advocated by Gratzer and Sterling.
November 19, Andrew Swan — W Types with reductions in presheaf categories (part 2)
November 12, Andrew Swan — W Types with reductions in presheaf categories (part 1)
Inductively defined types are ubiquitous in mathematics. It is very common to specify a type or set by listing ways to construct new elements from families of old elements. A simple example is the set of natural numbers, which is inductively generated as the smallest set satisfying the following: There is a natural number 0, and for every natural number n, there is a successor S n. The most natural way to phrase inductive types in category theory is via W-types, which are initial algebras of endofunctors of a certain simple form (called polynomial endofunctors). The small object argument is almost, but not quite an inductively defined type. It is not enough to keep adding new elements: you have to simultaneously do some quotienting for the argument to work. This makes it not an inductive type, but a *higher* inductive type. W types with reductions are a simple kind of higher inductive type that suffice to carry out an internal version of the small object argument, as well as some other constructions, such as localisations of cubical sets. They work very similar to W types, except that in place of algebras for endofunctors we use algebras for *pointed* endofunctors. I'll give an explicit construction of a special case of W types with reductions in presheaf categories. The argument is designed to work in settings where we don't have exact quotients, so we need to only use quotienting in a very limited way. We also avoid using universes or replacement, by using W types in our metatheory instead of regular ordinals. Several explicitly given constructions in cubical sets by Coquand and Huber can be seen as special cases of this one argument.
November 5, Jonas Frey — The fat small object argument
I will discuss ideas around the *fat small object argument*, focussing especially on the "finitary" version that is relevant to the theory of clans.
October 22, Kian Cho — Lifting properties and the small object argument
In this talk we will discuss lifting properties of collections of morphisms in a category. Given a class of morphisms, we can define another class of maps that have left lifting property with respect to the given class. We will show such classes are closed under common categorical constructions such as retracts, pushouts, and compositions. We will also define weak orthogonal systems and weak factorization systems and see when a given collection of morphisms can be promoted to a weak factorization system, and as a corollary, when we can obtain a (strict) factorization system.
October 15, No seminar (MURI Meeting)
October 8, Mathieu Anel — Localizations of categories (part 3)
October 1, Mathieu Anel — Localizations of categories (part 2)
September 24, Jacob Neumann — Groundwork to Higher Allegory Theory
I will enumerate several interesting possible avenues of research which connect the theory of binary relations to Homotopy Type Theory. Binary relations are indispensable in classical mathematics, and higher-dimensional analogues of binary relations promise to occupy an important (and interesting!) place in univalent mathematics. After rehearsing some of the theory of allegories in the setting of homotopy type theory (and speculating about possible generalizations), I'll discuss how we can adapt certain allegory-theoretic notions to better describe and reason about constructions in type theory. If possible, I hope to also touch on some semantic considerations related to this work, as well as describe some circumstances in functional programming and type theory where binary relations are particularly helpful. The content of this talk is all very much work-in-progress, so suggestions & feedback are very welcome!
September 17, Mathieu Anel — Localizations of categories (part 1)
I will review a number of results around localizations of categories, both in the context of 1‑categories and ∞‑categories. The purpose is to present homotopy theory as a toolbox to compute within ∞‑localizations, as developped in Cisinski's book. (The talk will go over some of the material presented here.)
September 10, Reid Barton — TBA
May 21, Fernando Larrain Langlois — A Higher Inductive Presentation of the Integers
Final public examination for the degree:
MASTER OF SCIENCE IN LOGIC, COMPUTATION AND METHODOLOGY:
Advisor: Steve Awodey
Committee: Jonas Frey
1pm, in the Zoom room of the seminar
May 14, Mathieu Anel — An example of elementary ∞-topos
A homotopy type is called bounded coherent if it is truncated and if all its homotopy invariants are finite sets. We shall prove that the ∞-category BCoh(S) of bounded coherent spaces has many of the expected features of elementary ∞-topoi: it is a lex category, with extensive finite sums, and with universal and effective quotients of Segal groupoid objects, it is locally cartesian closed, it has a subobject classifier, enough univalent families and all k-truncation modalities (and all these structures can be computed in the category of all spaces). However, it does not have pushouts and none of the univalent families seems to be closed under ∑ and ∏, which prevent BCoh(S) to be an instance of Shulman's definition of elementary ∞-topos. But, bounded coherent spaces do define a non-trivial universe in the Grothendieck ∞-topos of small spaces.
Slides of the talk
April 9, Greg Langmead — Several Angles on the Theory of Connections
Homotopy Type Theory provides a means to reinvent existing mathematics. By selecting, or discovering, the right definitions of classical constructions, smart people have imported many structures into HoTT already, thereby simultaneously formalizing the material (often in a computer as well) and vastly generalizing it. So how might we import gauge theory and Chern-Weil theory? These are topics that become available after one has constructed principal bundles. These provide a source of topological invariants, both of bundles and of the base-space manifold as well. They offer obstructions to orientation, nonvanishing vector fields, and other constructions. Consider the Gauss-Bonnet theorem: by integrating the scalar curvature of a connection over a surface, you obtain the Euler characteristic. Moreover gauge theory is the gateway to the standard model of physics, where gauge fields (connections) are the forces and the matter fields are given by sections of associated vector bundles. To unlock all of this we need the theory of connections and curvature on a principal bundle. In this talk I will give an overview of connections _from the classical perspective_. We may speculate together about a HoTT version, but I will not be offering one. The prerequisites are smooth manifolds and tangent bundles (a vague familiarity will suffice). I'll be going breadth-first so I can hasten to show a few different definitions, calling out material that I'm glossing over so that we can circle back in breakout sessions on future occasions.
April 2, Nima Rasekh — Every Elementary Higher Topos has a Natural Number Object
One key aspect of elementary topos theory is the existence of a natural number object. While it does not exist in every elementary topos (such as finite sets) we often need it to study more advanced aspects of topos theory (such as free monoids). In this talk we want to see how in the higher categorical setting, the existence of a natural number object can in fact be deduced from a very small list of axioms that any reasonable definition of elementary higher topos should satisfy, hence proving that every elementary higher topos has a natural number object. We will observe how the main challenge of the proof is not to construct the relevant object, but rather how to prove it has the desired universal property (the Peano axioms) in a higher categorical setting and how we will import ideas from homotopy type theory to overcome this challenge.
Slides of the talk
Article
March 19, David Jaz Myers — Modal Fracture for Higher Groups
In his nLab page "Differential Cohesion and Idelic Structure", Urs Schreiber shows how a family of fracture theorems for spectra --- including the traditional fracture theorem of Sullivan and the differential cohomology hexagon of Bunke, Nikolaus, Völkl --- can be expressed through the interplay of an adjoint modality/comodality pair. In this talk, we will construct an unstable version of this modal fracture hexagon in "strongly oo-connected homotopy type theory", which is Mike Shulman's cohesive homotopy type theory without the sharp modality. The modal fracture hexagon relates the universal oo-cover of a higher group with the group's infinitesimal remainder, the quotient of the group by its discrete reflection. Through the course of the talk, we'll meet these two characters and learn of their drama. This tension culminates in the modal fracture hexagon, and our calculation of the homotopy type of the infinitesimal remainder.
Slides of the talk
March 12, Dan Christensen — Non-accessible reflective subuniverses in HoTT
I will review the theory of reflective subuniverses ("localizations") as described in [RSS] and [CORS]. These include modalities such as n-truncation, as well as non-modalities such as localization at a prime. Every small family of maps determines a reflective subuniverse, and the ones determined in this way are called "accessible". I will describe the construction in [CORS] of a new reflective subuniverse L' associated to any reflective subuniverse L, noting that care was taken to avoid the assumption that L is accessible. But are there any interesting non-accessible reflective subuniverses? The second part of the talk will outline a new proof that for a not-necessarily small family of n-connected maps there is still an associated reflective subuniverse, generalizing classical work of Casacuberta, Scevenels and Smith. In order to prove this, I'll prove some results that extend Rijke's join construction [R] to prove that certain types are small.
[CORS] J.D. Christensen, M.P. Opie, E. Rijke, and L. Scoccola. Localization in homotopy type theory. Higher Structures 4(1) (2020), 1-32.
[R] E. Rijke. The join construction.
[RSS] E. Rijke, M. Shulman, and B. Spitters. Modalities in homotopy type theory. Log. Methods Comput. Sci. 16(1) (2020), Paper No. 2, 79 pp.
Slides of the talk
March 5, Karol Szumilo — Infinity groupoids in lextensive categories
I will discuss a construction of a new model structure on simplicial objects in a countably extensive category (i.e., a category with well behaved finite limits and countable coproducts). This builds on previous work on a constructive model structure on simplicial sets, originally motivated by modelling Homotopy Type Theory, but now applicable in a much wider context. This is joint work with Nicola Gambino, Simon Henry and Christian Sattler.
Slides of the talk
Article
February 19, Eric Finster — Types are Internal ∞-Groupoids
I will explain an approach to defining infinitely coherent algebraic structures in type theory by exploiting a universe of structures with explicitly prescribed computation rules. Among the structures which can be defined using these techniques are A_oo-monoids and groups, oo-categories, planar oo-operads (i.e. oo-multicategories) and more. As a special case, one obtains an internal definition of oo-groupoid, and I will describe how to use this setup to describe the type of oo-groupoids explicitly by showing that it is in fact equivalent to the universe U of types. In other words: every type admits the structure of an oo-groupoid internally, and that structure is unique.
Slides of the talk
Article
February 5, Jon Sterling — Normalization for Cubical Type Theory
(J.w.w. Carlo Angiuli) We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. The main difficulty in comparison to conventional type theory is located in a new feature of cubical type theories, the absence of a stable notion of neutral term: for instance, the path application (p @ i) ceases to be neutral within its “locus of instability” ∂(i) and must compute to an endpoint. We introduce a new, geometrically-inspired generalization of the notion of neutral term, stabilizing neutrals by gluing them together with partial computability data along their loci of instability — when the locus of instability is nowhere, a stabilized neutral is a conventional neutral, and when the locus of instability is everywhere, a stabilized neutral is just computability data. Our normalization result is based on a reduction-free Artin gluing argument, and yields an injective function from equivalence classes of terms in context to a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality, as well as injectivity of type constructors in contexts formed by assuming variables x : A and dimensions i : 𝕀.
Article
2020 program
December 11, Sina Hazratpour — Kripke-Joyal semantics for dependent type theory
Every topos has an internal higher-order intuitionistic logic. The so-called Kripke–Joyal semantics of a topos gives an interpretation to formulas written in this language used to express ordinary mathematics in that topos. The Kripke–Joyal semantics is in fact a higher order generalization of the well-known Kripke semantic for intuitionistic propositional logic. In this talk I shall report on joint work with Steve Awodey and Nicola Gambino on extending the Kripke–Joyal semantics to dependent type theories, including homotopy type theory.
Slides of the talk
December 4, Colin Zwanziger — Sheaf Universes via Coalgebra
There is a well-known construction of a universe for presheaf models of type theory, which does not extend to arbitrary sheaf models (Hofmann and Streicher 1999). This issue is naturally understood in the context of a framework such as natural models of type theory (Awodey 2012). We would like to leverage the fact that any sheaf topos arises as the category of algebras for a Cartesian reflector on a presheaf category. Unfortunately, it is not the case that natural models are closed under the construction of algebras for the corresponding notion of Cartesian reflector (c.f. Coquand et al. 2020). In my dissertation work, I show that natural models are closed under the construction of *co*algebras for Cartesian comonads. This construction generalizes the presheaf case in a direction that includes many sheaf toposes. I will focus in this talk on the example of sheaves on a topological space. We will use a coalgebraic presentation of sheaves. This is similar to the local homeomorphism presentation, but with the advantage that the inverse image of sheaves is strictly coherent (Marmolejo 1998). The natural model and universe structures can be described in relatively familiar terms.
Slides of the talk
November 20, Tslil Clingman — More than merely composition: towards the theory of proof-relevant categories and algebras
Homotopy Type Theory has profited immensely from the key insight that precisely how two things are equal is important. This has, in some areas, liberated the mathematician from the necessity of making choices and performing the complex combinatorial computations of manipulating presentations of objects and their equalities. By analogy, in Category Theory many questions of coherence arise when we are forced to choose a `the' composite for some given morphisms. One approach to remedy these issues is by means of addressing composites by their universal property. However, the theme of this talk is that such a stance is not analogous to the key insight of Homotopy Type Theory. Rather, as we will propose, the analogous view would entail that the universal property of a composite ought to be data, and tracking precisely how the universal property is implemented should be important. To that end, in this talk we will introduce the idea of proof-relevant categories and proof-relevant functors with the explicit aim of capturing such data. The former objects are (potentially infinite dimensional) category-like structures in which, for a given arrangement of composable cells, there may be in general many proofs that the arrangement interprets to another cell via composition. The latter objects suitably generalise the anafunctors of Makkai to this setting: on a given input, there may be in general many proofs that the functor obtains a given value. We will strive to motivate these structures by examples, and make connections to the univalent categories of Homotopy Type Theory. These notions all emerge from the general framework of proof-relevant algebras for globular T-categories. Time and interest allowing we will examine how an arbitrary strict omega-category X may be combined with a T-category A so that proof-relevant algebras over the result are proof-relevant algebras for A with proof-relevant morphisms ``in the shape of X''. From this point of view we will consider `compositions' of proof-relevant functors as well as progress towards an appropriate proof-relevant category of proof-relevant categories.
Slides of the talk
November 13, Anders Mörtberg — Programming and proving with the structure identity principle in Cubical Agda
One of the most striking consequences of univalence is the structure identity principle (SIP) which states that equivalent structured types are identifiable. There are multiple ways to formalize this principle in homotopy type theory and I will discuss a variation that we have recently formalized in Cubical Agda. The constructive nature of cubical type theory allows us to reap the full benefits of the SIP, making it possible to transport programs and proofs along paths constructed using the SIP without losing computation. We furthermore generalize the SIP to encompass also relational representation independence results. By using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them the correspondence becomes an equivalence between the quotiented types, thereby allowing us to obtain an equality of implementations by the SIP. We have applied this to a wide variety of examples in the Cubical Agda library, including algebraic structures, unary and binary numbers, matrices, queues, and finite multisets. (This is joint work with Carlo Angiuli, Evan Cavallo and Max Zeuner. Preprint can be found at arXiv:2009.05547.)
Slides of the talk
November 6, Joachim Kock — Decomposition spaces, incidence algebras and Möbius inversion
I'll start rather leisurely with a review of incidence algebras and Möbius inversion, starting with the classical Möbius function in number theory, then incidence algebras and Möbius inversion for locally finite posets (Rota) and monoids with the finite decomposition property (Cartier-Foata), and finally their common generalisation to Möbius categories (Leroux). From here I'll move on to survey recent work with Gálvez and Tonks taking these constructions into homotopy theory. On one hand we generalise from categories to infinity-categories in the form of Rezk-complete Segal spaces, taking an objective approach working directly with coefficients in infinity-groupoids instead of numbers. (Under certain finiteness conditions, numerical results can be obtained by taking homotopy cardinality.) On the other hand we show that the Segal condition is not needed for these constructions: it can be replaced by a weaker exactness condition formulated in terms of the active-inert factorisation system in Delta. These new simplicial spaces we call decomposition spaces: while the Segal condition expresses composition, the new condition expresses decomposition. (An equivalent notion, formulated in terms of triangulations of polygons, was discovered independently by Dyckerhoff and Kapranov under the name unital 2-Segal space.) Many convolution algebras in combinatorics arise as the incidence algebra of decomposition spaces which are not categories, for example Schmitt's chromatic Hopf algebra of graphs or the Butcher-Connes-Kreimer Hopf algebra of trees. The Waldhausen S-construction of an abelian (or stable infinity-) category is another example of a decomposition space; the associated incidence algebras are versions of (derived) Hall algebras. I will finish with some recent applications to free probability (joint work with Ebrahimi-Fard, Foissy, and Patras).
October 30, Ivan Di Liberti — Formal Model Theory and Higher Topology
Motivated by the abstract study of semantics, we study the interaction between topoi, accessible categories with directed colimits and ionads. This theory amounts to a categorification of famous construction from general topology: the Scott topology on a poset and the adjunction between locales and topological spaces. This technology is then used in order to establish syntax-semantics dualities. Among the significant contributions, we provide a logical understanding of ionads that encompasses Makkai ultracategories.
Slides of the talk
October 23, Denis-Charles Cisinski — The ∞-category of ∞-categories
This is a report on a joint work with Hoang Kim Nguyen which establishes a new way to construct the straightening/unstraightening correspondence in the context of quasi-categories.
https://arxiv.org/abs/2210.08945
October 16, Andrew Swan — The Nielsen-Schreier Theorem in Homotopy Type Theory
The Nielsen-Schreier theorem states that subgroups of free groups are themselves free groups. Although the statement of the theorem is simple, it is quite tricky to give a direct proof. However there is a conceptually clear proof using ideas from algebraic topology. This makes the Nielsen-Schreier theorem an ideal candidate for formalisation in homotopy type theory. I will use the characterisation of groups in homotopy type theory as pointed connected 1 truncated types. Under this characterisation it is known that free groups are exactly wedges of circles and that subgroups correspond to pointed connected covering spaces (i.e. families of hSets indexed by the group). With these definitions the ideas of the algebraic topology proof can be applied directly. I will give a constructive proof of the special case of finite index subgroups and a proof of the full theorem using the axiom of choice. The finite index version has been verified electronically using Agda. I will show the axiom of choice is necessary for the full theorem by giving an example of a boolean infinity topos where it is false. A related argument shows that the "untruncated" version of the theorem is provably false in HoTT even for finite index subgroups of finitely generated free groups.
Preprint arXiv:2010.01187 and Agda formalization
October 9, Nicolai Kraus — Internal ∞-Categories with Families
It is natural to formalize the notion of a model of type theory (especially the syntax = intended initial model) inside type theory itself. This is often done by writing the definition of a category with families (CwF) as a generalized algebraic theory. What could be the success criterion from a HoTT point of view? The typical first goal is that the initial model is an h-set or even has decidable equality. Our second goal is to make the "standard model" work, i.e. the universe U should be a CwF in a straightforward way (cf. Mike Shulman's 2014 question whether the n-th universe in HoTT models HoTT with n-1 universes). Unfortunately, it is hard to combine these two goals. If we include set-truncatedness explicitly in the definition of a CwF, then the "standard model" is not a CwF. If we don't, then the initial model is not an h-set. The root of the problem is that 1-categories are not well-behaved concepts in an untruncated setting. The natural approach are higher categories, which corresponds to "equipping the syntax with all coherences" instead of truncating. In this talk, I will explain one approach to this based on a type-theoretic formulation of Segal spaces, expressed in HTS/2LTT. I will discuss what works and what is still open. The talk will be based on arXiv:2009.01883.
October 2, Simon Henry — Left, right and weak model structures
Left semi-model structure, right semi-model structure and weak model structure are weakening of the notion of Quillen model structures that are still enough to formalize homotopy theory categorically, but are often easier to construct and enjoys better stability properties. I will review these notions, how they relates to each other and to other framework for categorical homotopy theory. This will include several recent or new results about construction of left, right and weak model structure that generalizes known results about Quillen model structure, and tends to be simpler.
Slides of the talk
September 25, Jonathan Weinberger — Cocartesian fibrations in Simplicial Type Theory
In 2017, Riehl and Shulman introduced Simplicial Type Theory (STT) which is an extension of Homotopy Type Theory allowing to reason not only about infinity-groupoids, but infinity-categories. A key gadget are judgmental extension types, based on ideas by Lumsdaine and Shulman, allowing for defining directed hom types. The prime model is the infinity-topos of simplicial spaces, hence STT can be seen as a synthetic language for simplicial infinity-groupoids which allows for reasoning about infinity-categories interpreted as Rezk spaces. We discuss aspects of the theory of cocartesian fibrations in this setting. This is joint work with Ulrik Buchholtz.
Slides of the talk
September 18, Thierry Coquand — Descent data operations and constructive sheaf models of type theory
This talk will present a higher generalisation of Lawvere-Tierney modalities that appear naturally in the setting of constructive presheaf models of type theory with univalence axiom and higher inductive types. Using the elementary and essentially algebraic character of these models, they relativise to any presheaf models over a base category. Any Grothendieck topology on this base category gives then rise to a family of modal operations on types, that we can call “descent data operations”. One main result is that these operations are left exact modalities (and each universe of modal types is itself modal). Even in the case of a trivial topology, the associated descent data operation may be non trivial and defines a new internal model where equivalences are pointwise equivalences. (This is closely connected to the recent use of the “cobar” operations by Mike Shulman.) If time allows, we will end with some questions connected to an example where the base site has already been used for an effective definition of the separable closure of a field and for which we should be able to recover, in a constructive setting the cohomological interpretation of the Brauer group of this field.
Notes of the talk
September 11, Steve Awodey — The equivariant model structure on cubical sets
The category of cubical sets has a model structure that can be described axiomatically in a way that is inspired by the model of type theory that it supports. Univalence, for example, plays a key role. This model category is not Quillen equivalent to the standard Kan one on simplicial sets, however. But there is another model structure taking the symmetries of the cubes into account, and that one is equivalent, according to a result by Christian Sattler. In this talk I will explain this more refined "equivariant model structure". Joint work with Thierry Coquand and Emily Riehl.
Slides of the talk
- April 3: Reid Barton (Pitt), Model Categories for o-Minimal Homotopy Theory
- March 27: Mathieu Anel (CMU) Clans from Lurie’s Geometries
- March 4: Samuele Maschio (Padua) The Minimalist Foundation and Axiomatic Set Theories
- February 28: Milly Maietti (Padua) Compatibility of the Minimalist Foundation with Homotopy Type Theory
- February 21: Jonas Frey (CMU), Duality for Clans
- February 14: Colin Zwanziger (CMU), Generalizing the Topos of Coalgebras to the Natural Model of Coalgebras
- February 7: Reid Barton (Pitt), The Algebra of Combinatorial Premodel Categories
- January 31: Steve Awodey (CMU), A Cubical Universe of Fibrations
- January 17: Jon Sterling (CMU), Gluing Models of Type Theory Along Flat Functors
2019
- December 6: Jonas Frey (CMU), Categories of Partial Equivalence Relations as Localizations
- November 22: Mathieu Anel (CMU), A Small Object Argument for Unique Factorization Systems
- November 15: Evan Cavallo (CMU), Modelling Identity Types with a Fibred Factorization System
- October 11: Andrew Swan (CMU), Lifting Problems and Algebraic Weak Factorisation Systems over a Grothendieck Fibration
- October 4: Jonathan Weinberger (Darmstadt), Modalities and Fibrations for Synthetic (∞,1)-Categories
- May 3: Greg Langmead (CMU), Categories and Modalities for Smoothness: Part 2
- April 26: Adam Millar (CMU), The Groupoid Model; Zesen Qian (CMU) Induction and Coinduction
- April 19: Anders Mortberg (CMU), UniMath – Univalent Foundations of Mathematics
- March 29: Jonathan Sterling (CMU), Algebraic Type Theory and the Gluing Construction
- March 22: Mathieu Anel (CMU), Small Objects and Their Arguments
- March 11-15: Geometry in Modal Homotopy Type Theory (workshop)
- February 28: Loïc Pujet (Nantes), Synthetic Homotopy Theory in Cubical Type Theory and the Hopf Fibration
- February 22: Iosif Petrakis (LMU Munich), Dependent Sums and Products in Bishop Set Theory
- February 15: David Spivak (MIT), A Higher-Order Temporal Logic for Dynamical Systems
- February 8: Bruno Bentzen (CMU), Informal Cartesian Cubical Type Theory
- February 1: Steve Awodey (CMU), A Quillen Model Structure on the Cartesian Cubical Sets
- January 25: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 2
- January 18: Felix Wellen (CMU), Covering Spaces in Modal HoTT
2018
- December 14: Colin Zwanziger (CMU), Modal Categories with Attributes: Part 1
- December 7: Siva Somayyajula (CMU), Perspectives on Sessions
- November 30: Koundinya Vajjha (Pittsburgh), Voevodsky’s Simplicial Modal of HoTT
- November 21: Egbert Rijke (UIUC), The Small Object Argument in Terms of the Pushout-Product.
- November 20: David Jaz Myers (Johns Hopkins)
- November 16: Adam Millar (CMU), The Groupoid Model as a Category with Families
- November 9: Greg Langmead (CMU), Categories and Modalities for Smoothness
- November 2: Steve Awodey (CMU), Lax and Strict Models of Dependent Type Theory
- October 25: Marcelo Fiore (Cambridge), 2-Dimensional Lambda Calculus
- October 5, 12, 19: Jonas Frey (CMU), Semantics of Type Theory
- September 21, 28: Mathieu Anel (CMU), Type Theory v. Higher Category Theory
- September 7: Max Doré (LMU Munich) and Colin Zwanziger (CMU), Intension and Extension in Type Theory
- April 27: Dan Christensen (Western Ontario), Vector Fields on Spheres
- April 13: Colin Zwanziger (CMU), I ntensional Predicates in Comonadic Intensional Type Theory
- April 6: Marcelo Fiore (Cambridge), An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
- March 8: Andrew Pitts, Pursuing Univalence with Categorical Logic
- February 16: Mathieu Anel (Paris), What’s New in oo-Topoi?
- February 8: Eric Finster (Paris), Lex Modalities in Type Theory
- February 6, 13: André Joyal (Montreal), Theory of Tribes.
- February 2: Felix Wellen (CMU), Algebraic Geometry and Modal Type Theory
- January 26: Joseph Helfer (Stanford), First-Order Homotopical Logic
- January 19: Felix Wellen (CMU), Fiber Bundles in HoTT
- January 15: Ian Orton (Cambridge), An internal presentation of cubical models
talks in 2017
- December 8: Marco Larrea (Leeds), Models of Martin-Löf Type Theory from Algebraic Weak Factorisation Systems
- November 3, 10, 17: Anders Mörtberg (CMU), Introduction to Cubical Type Theory.
- October 20: Simon Boulier (Nantes), Model Structure on the Universe in a Two Level Type Theory
- October 13: Felix Wellen (CMU), Differential Homotopy Type Theor
- September 22: Clive Newstead (CMU), Polynomials, Representability and Dependent Type Theory
- September 1: Pino Rosolini (Genova), Dominance