FALL 2024 Program
Fridays 1-3pm in BH 150
(Anti-chronological order)
November 22, Steve Awodey — Identity Types in Polynomial Models of Type Theory
November 15, C.B. Aberlé — Polynomial Universes & Natural Models of (Linear) (Dependent) Type Theory, part II
November 8, C.B. Aberlé — Polynomial Universes & Natural Models of (Linear) (Dependent) Type Theory, part I
Natural models provide an elegant solution to problems of strictness in the categorical semantics of dependent type theory, and are naturally regarded as polynomial functors that behave, in a suitable sense, like proof-relevant partiality monads for certain type-theoretic universes in the internal languages of various presheaf categories. In this talk, I will present some work I have conducted over the past summer at the Topos Institute, joint with David Spivak, wherein we have aimed to extend, refine, and generalize this treatment of models of type theory by studying properties of such polynomial universes in various categories of polynomial functors. We shall see how the language of polynomial functors can be used to elegantly capture all of the usual constructs of dependent type theory, including some that have previously proved difficult for such treatments. As a demonstration of this, I shall sketch our proof that a natural model is closed under ∏ types if and only if the associated polynomial functor, regarded as a Cartesian (pseudo)monad, possesses a (pseudo-)distributive law over itself that is also Cartesian, in an appropriate sense. Time permitting, I shall also discuss some of my own ongoing work on extending this approach further to handle inductive types and (intensional) identity types, and to novel applications, such as the categorical semantics of substructural type theory and even linear dependent type theory.
November 1, Joseph Hua — Fibrant Inductive Types from Universal Monads
Assuming an algebraic fibration structure on cubical sets, we can prove existence of fibrant W-types over a fibrant signature. This does not capture much of the "higher" nature of HITs, but could be combined with homotopy pushouts (for example) to produce other interesting constructions. To prove existence of such inductive types we combine (take the algebraic coproduct of) the monad for the algebraic fibration structure with the algebraically free monad of the polynomial endofunctor representing the (not necessarily fibrant) universal property of the W-type.
October 25, Owen Milner — Formalisation of Postnikov effectiveness
This talk will be a report on the formalization of a recent proof, due to Anel and Barton, that countable choice implies Postnikov effectiveness in HoTT. Time permitting, some possible extensions of this work will also be discussed.
October 18, Kohei Kishida ( Univ. of Illinois Urbana-Champaign) — Gödel, Escher, Bell: A Topological and Categorical Perspective on Quantum and Logical Paradoxes
Quantum physics exhibits various non-classical and paradoxical features. Among them are non-locality and contextuality (e.g. Bell's theorem or the EPR paradox). Since they are expected to constitute a key resource in quantum computation, several approaches have been proposed to provide high-level expressions for them. In one of these approaches, Abramsky and others (including me) use the mathematics of algebraic topology and characterize non-locality and contextuality as the same type of phenomena as M. C. Escher's impossible figures. In this talk, I expand this topological insight and demonstrate that logical paradoxes arising from circular references (cf. Gödel as in _Gödel, Escher, Bach_) share the same topological structure as the quantum paradoxes, by reformatting the topological model of contextuality into a categorical semantics of logical paradoxes. This topological and categorical semantics indeed provides a unifying perspective from which previous approaches of philosophers and logicians to logical paradoxes can be understood as diverse ways of fine-tuning topologies to model the paradoxes.
October 11, Steve Awodey — Toward the Higher Effective Topos
The Hofmann-Streicher groupoid model of HoTT can be regarded as an interpretation into a 2-topos, in the sense of Weber, with a weak factorization system of fibrations interpreting the type families, and a classfier E —> U for small discrete fibrations, generalizing the subobject classifier of a 1-topos. Recent work has shown that (a cubical presentation of) this model is entirely constructive; so it can also be carried out in Hyland’s Effective topos Eff. An open question regarding this realizability model is whether the 1-category of sets therein is equivalent to Eff. Toward an answer, we consider the subcategory of groupoid assemblies, and show that a modified subcategory of the discrete ones is indeed equivalent to the Effective topos.
Wednesday September 4, 9-11am, BH150 (exceptional day and time!)
Jon Sterling — Hofmann–Streicher lifting of fibred categories
In 1997, Hofmann and Streicher introduced an explicit technique to lift a Grothendieck universe 𝓤 from 𝐒𝐞𝐭 into the category of 𝐒𝐞𝐭-valued presheaves on a 𝓤-small category 𝓑. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the ‘categorical nerve’, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, applying the categorical nerve to the universal 𝓤-small discrete fibration gives the generic family of 𝓤’s Hofmann–Streicher lifting.
Although Awodey has investigated Hofmann–Streicher lifting in terms of a 1-functor 𝐂𝐚𝐭→𝐏𝐫(𝓑), his analysis can be extended to a 2-functor 𝐂𝐚𝐭→𝐅𝐢𝐛(𝓑) that is observed by Weber to be right 2-adjoint to the 2-functor that takes a fibred category to its total category (i.e. the oplax colimit of the corresponding diagram of categories under straightening). A generalised form of Hofmann–Streicher lifting that can be applied to categories other than universes is then obtained by conjugating this right 2-adjoint with duality involutions.
In joint work with Daniel Gratzer and Andrew Slattery, we have constructed a relative version of the 2-functorial Hofmann–Streicher lifting: given a fibration p:𝓐→𝓑, we have a 2-functor Δ[p]:𝐅𝐢𝐛(𝓑)→𝐅𝐢𝐛(𝓐) which is not base change but rather (we conjecture) right pseudo-adjoint to the 2-functor Σ[p]:𝐅𝐢𝐛(𝓑)→𝐅𝐢𝐛(𝓐) that sends a fibration q:𝓔→𝓐 to the composite fibration p∘q:𝓔→𝓑. A relative version of Hofmann–Streicher lifting could give a more regular theory to the practice of computing internal liftings of lifted universes.
Earlier seminars are listed here.