Carnegie Mellon University

SPRING 2023 Program

Fridays 1-3pm in BH 150

January 20, Mathieu Anel — Smooth and proper objects for a fibration

I will show how ideas of dependent type theory (dependent sums and dependent products) can be used to revisit features of topology (locally contractible and compact spaces). I will present a general framework for dependent sums and dependent products, and apply it to study the fibration of etale maps over the category of topoi. We shall see that the morphisms of topoi along which this fibration has dependent sums are the locally contractible morphisms, and the morphisms along which dependent products exists are proper morphisms. This is jww Jonathan Weinberger.

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

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.

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 17, Eric Finster —

Earlier seminars are listed  here.