Carnegie Mellon University

SPRING 2024 Program

Fridays 1-3pm in BH 255A 

January 26, Johan Commelin —  Condensed type theory

Condensed sets form a topos, and hence admit an internal type theory. In this talk I will describe a list of axioms satisfied by this particular type theory. In particular, we will see two predicates on types, that single out a class CHaus of "compact Hausdorff" types and a class ODisc of "overt and discrete" types, respectively. A handful of axioms describe how these classes interact. The resulting type theory is spiritually related Taylor's "Abstract Stone Duality". The type OProp of "overt and discrete" propositions behaves as a directed interval. I will make this precise, by showing that ODisc is "directed univalent" in the sense that functions A → B between two overt and discrete types A and B correspond naturally and bijectively two "directed paths" OProp → ODisc with endpoints A and B. As a consequence, every function ODisc → ODisc is automatically functorial. If time permits, I will comment on some of the techniques that go into the proof. Joint work with Reid Barton.

February 2, Double Feature

Federica Pasqualone —  Observing the quantum world: A pragmatic introduction to prefactorization algebras

In this talk we will dive into the realm of quantum phenomena, focusing on the act of measuring and the related difficulties, starting from basic classical analytical mechanics. We investigate then the logical structure of the space, define the categorical machinery needed and develop a semantics able to capture deformation quantization. The talk aims at providing a primer both in the physics we are modelling and in the complex mathematical structures involved and it is intended for a general audience.

Tesla Zhang —  Three non-cubical applications of extension types

https://arxiv.org/abs/2311.05658

February 9, Double Feature

Joseph Hua —  Higher inductive types in cartesian cubical sets

Higher inductive types (HITs) in HoTT allow for spaces to be built by specifying their universal properties, and data to be built by specifying equalities between terms. In this talk I will first briefly review aspects of the Quillen Model Structure on cartesian cubical sets (cSet) given in Awodey 2023. Then imitating the work in Lumsdaine, Shulman 2017 I will demonstrate how HITs can be constructed in cSet, starting with the easy example of coproducts.

Owen Milner —  On Connected Covers in HoTT

This talk will lay out some of the theory of connected covers in the language of homotopy type theory. This includes the definition of the Whitehead tower, and a proof that the fibers of the tower are Eilenberg-MacLane spaces. This follows a development of the theory in Cubical Agda.

February 16, Double Feature

C.B. Aberlé —  The Past, Present & Future of Parametricity in Type Theory & Univalent Foundations

Both type theory and (higher) category theory are centrally concerned with the question of how to describe various notions of mathematical structure and transformations of such structure that are suitably invariant or generic. In the case of category theory, such structural invariance/genericity is principally captured by properties of functoriality, naturality, and their higher analogues. On type theory's side of the equation, however, there exists a stronger notion of genericity – parametricity – the categorical semantics of which have yet to be fully settled. However, some recent developments suggest that internalizing a form of parametricity into homotopy type theory and its categorical semantics may be key to making progress on several open problems in Univalent Foundations relating to higher inductive types, higher categories, etc.

In this talk, I outline my own work on such internalization of parametricity and its applications. I begin with a survey of three strategies for such internalization that have emerged in recent years: observational, cubical, and modal, each of which builds upon the last. I then show how modal parametricity can be used to construct representations of higher inductive types and coinductive types. I subsequently develop a semantics for such modal parametricity in any model of HoTT equipped with a suitable higher modality as defined by Rijke, Shulman & Spitters. Time permitting, I shall also describe how a form of observational parametricity has recently been employed by Kolomatskaia & Shulman to solve the problem of defining semi-simplicial types, and indicate how other approaches to internal parametricity may fit into this picture.

Anthony Agwu —  On the Effective Topos

The Effective Topos is an important model of constructive higher order logic as it is the first example an an elementary topos that internally is constructive and is not a Grothendieck topos; in fact it doesn't even have countable limits and colimits. The Effective Topos is built out of the theory of partial recursive functions. As such, it is a model a recursive mathematics. However, the Effective Topos has some peculiar properties. In this talk I will briefly talk about the construction of the Effective Topos and a few interesting facts about it.

February 23, Jonas Frey —  Lax idempotent monads and PCAs

I present a characterization of realizability triposes (Theorem 2.8 here) over inclusions of partial combinatory algebras, in terms of a primality condition expressing that a tripos P is a cocompletion under existential quantification, and a discreteness condition, expressing that the indexed sub-preorder prim(P) on prime predicates is is freely generated from an indexed preorder on the category Set_{inj} of sets and injections. The ∃-completion and the extension of indexed posets from Set_{inj} to Set give rise to a lax idempotent monad, and a colax idempotent 2-monad respectively. Time permitting, I will discuss other instances of these notions, and in particular the concept of *injective algebra* of a lax idempotent monad.

March 1, Sanjeevi Krishnan —  Cubical sets as models for directed homotopy types

We present an equivalence between homotopy theories of directed combinatorial spaces and directed topological spaces. Specifically, we describe how directed realization induces a categorical equivalence between localizations on cubical sets and directed topological spaces by suitable notions of directed weak equivalence. Along the way, we develop a directed analogue of test fibrant cubical sets which we call cubcats. Cubcats are like higher categories except that coherence conditions hold not up to higher isomorphisms but instead higher zig-zags of morphisms. We identify cubcats in nature, such as cubical nerves of small categories and singular cubical sets of spacetimes; the latter class of examples do not generally form cubical versions of higher categories. As an application, we can compute a directed singular 1-cohomology, taking coefficients and values in commutative monoids, for directed topological spaces in nature. We discuss important differences between directed homotopy types and higher categories as models of computation and sketch how directed homotopy theory likely fits into a type-theoretic model structure. The cubical sets we discuss are presheaves over the minimal symmetric monoidal variant of the box category; we discuss current limitations and future possibilities of generalizing the results for other variants.
slides powerpointslides pdf

March 8, Spring break — no seminar

March 15, Wentao Yang —  On successive categoricity, stability and NIP in abstract elementary classes

We give an overview of results in the study of abstract elementary classes, including progress towards answering the successive categoricity question (joint work with Marcos Mazari-Armida), approximation to the categoricity conjecture and equivalence between model existence and stablility (joint work with Marcos Mazari-Armida and Sebastien Vasey) and a parallel of NIP in abstract elementary classes.

March 22, Claymont retreat — No seminar

March 29, Double Feature

Adam Hill —  Dedekind Cubical Nerve and Cubical Kan Complexes

In this talk, we will first define the Dedekind Cube Category as a Lawvere theory for Bounded Distributive Lattices, then point to a particular model of interest in Top. From here we will construct a "geometric realization" functor from the presheaf category on Dedekind cubes to topological spaces. This construction will admit a right adjoint called the "cubical nerve" (of spaces). At the end of this talk, we will have described what a "Kan complex" is in this context and showed that (similar to the simplicial set case) the Cubical Nerve of any space is a Kan complex.

Fernando Larrain Langlois —  Strictification of Generalized Algebraic Theories

We shall review the standard left- and right-adjoint strictifications of Grothendieck fibrations as they relate to the semantics of generalized algebraic theories. More precisely, we shall describe and compare the two canonical ways of producing natural models out of display categories.

April 5, Spring break — no seminar

April 12, Wojciech Nawrocki —  Kripke-Joyal Semantics as a Modality in Lean 4

Propositions about categories are sometimes better viewed from a synthetic perspective, namely as statements in an internal language L that axiomatizes the relevant domain of inquiry. A well-designed internal language can clarify the essence of a class of problems, and constructions carried out therein can be more general (by applying to all the models of L). However, unfolding an internal statement into its interpretation is often burdensome on paper, at least because interpretations can be highly non-trivial. This presents a barrier to the adoption of synthetic approaches. Our working hypothesis is that a proof assistant can take care of this bureaucracy, granting the user more confidence in their results.

To date, no framework mixing internal and external reasoning has been implemented in a proof assistant. We present preliminary work towards a library of Lean 4 tactics and macros for Kripke-Joyal semantics. Kripke-Joyal semantics provides a convenient notation for working with the interpretation of higher-order logic in a sheaf topos, in particular when reasoning about local data. A design goal of the implementation is to feel natural to users of proof assistants based on dependent type theory (for instance by allowing the use of existing tactics while reasoning internally). To do this, we formulate Kripke-Joyal notation as a modality in the host type theory. We view the added modality as a conservative extension of the original language which is eliminable by means of the interpretation function. This is joint work with Gabriel Ebner.

 

Earlier seminars are listed  here.