StockholmGoteborgMeeting250221
Stockholm - Göteborg type theory meeting on Friday, 21 February in Göteborg
Schedule
| 11:45 - 12:15 | Loďc Pujet |
| Lunch | |
| 13:20 - 13:50 | András Kovács |
| 13:55 - 14:25 | Daniël Apol |
| 14:30 - 15:00 | David Wärn |
| Coffee | |
| 15:45 - 16:15 | Axel Ljungström |
| 16:20 - 16:50 | Evan Cavallo |
| 18:00 | Dinner Andrum (map) |
The talks are in FL61 in the Physics Building at Chalmers.
Zoom: 65838770874
Titles and abstracts
Loďc Pujet: Strictified CwFs for simpler normalisation proofs
Abstract: Categories with families (CwF) are perhaps the most widely used notion of model for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant. In this talk, I will present a method based on Pédrot's “prefascist sets” to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to proofs of canonicity and normalisation by gluing. This is joint work with Ambrus Kaposi.
András Kovács: Logical frameworks of logical frameworks
Abstract: logical frameworks and the very closely related two-level type theories let us work in a mixture of a metatheory and an object theory. Here, we have a second-order view on the object theory where contexts, variables and substitutions are implicit and binders are represented as metalanguage functions. We'd like to generalize LFs and 2LTTs so that we can work with multiple object theories, and both with first-order and second-order models for each theory. The desired theory would embed all 2LTTs/LFs as syntactic fragments. There's a good candidate for a semantic domain that supports this: the category of categories. However, we have to make some compromises to get a usable syntax. One design point restricts the categorical language significantly, but we get a well-behaved fully structural syntax. Another design point is more expressive, but it seems to require modalities in the syntax.
Daniël Apol: Algebraic weak factorization systems in higher category theory
Abstract: It’s common in mathematics to have a map E -> B and a certain “thing” in B, perhaps parametrized over something else, and wonder if there is a thing in E (parametrized in a similar way) "lying over" our given thing in B. Interesting properties of objects, such as "being an actual type" in homotopical models for type theory, are often definable in terms of solvability of certain such lifting problems. Classically, these solutions are only asked to merely exist, but in constructive and homotopical mathematics we require specific choices of lifts for each lifting problem: solving lifting problems becomes an operation.
In practice it’s often possible to require the solutions to different lifting problems to interact nicely with each other and satisfy all kinds of relations. In non-homotopical mathematics, a popular approach to these highly structured lifting operations is given by the notion of an algebraic weak factorization system (AWFS). A natural question is therefore if one can generalize the theory of AWFSs towards the setting of (oo,1)-categories, i.e. towards the world of homotopical mathematics.
In this talk I will talk about the idea of an AWFS, and present some current work in progress, joint with Christian Sattler, that outlines such a generalization to oo-categories, together with some results obtained so far. If time permits, I will talk about both the double-oo-categorical approach and the comonad-monad approach, which should end up producing the same theory.
David Wärn: Steenrod squares via unordered joins
Abstract: Steenrod squares are mod 2 cohomology operations with important applications in algebraic topology. Their definition in HoTT was sketched by Brunerie, and involves the coherent symmetry of the cup product together with an analysis of the cohomology of the type RP∞ of two-element types. In this talk I will explain this definition as well as recent work with Axel Ljungström on going beyond the definition to prove important properties of the Steenrod squares.
Axel Ljungström: Cellular homology in HoTT
Abstract: Cellular cohomology and homology constitute particularly `computational' invariants which can be used to extract important information about a given CW complex. While the theory of cellular cohomology is well-understood in HoTT, little has been said about the corresponding homology theory. In this talk, I will give an overview of a recent project with Loďc Pujet on an attempt at developing cellular homology in HoTT. The main result is a definition of cellular homology satisfying the Hurewicz theorem. We get there by proving constructive analogues of classical approximation theorems.
Evan Cavallo: Replacement in cubical models and type theories
Abstract: Rijke's type-theoretic axiom of replacement, an extension to Martin-Löf type theory with a universe U, states that any map from a U-small type to a locally U-small type (i.e., one with U-small identity types) admits a U-small image. In univalent type theory, where the universe U is itself locally U-small, it becomes a weak but versatile higher inductive type principle: not only can it be used to construct set quotients as in set theory, but also n-truncations, Eilenberg-Mac Lane spaces, and more. Rijke shows by an involved construction that replacement is a theorem in univalent type theory with pushouts. I will present a more direct semantics (and effective) of the replacement axiom in cubical sets models, as well as a higher inductive-recursive formulation in cubical type theory. This is joint work with Thierry Coquand.