StockholmGoteborgMeeting231128
Stockholm - Göteborg meeting on Tuesday, 28 November 2023 in Göteborg
Schedule
| 11:40 - 12:15 | Loīc Pujet |
| Lunch | |
| 13:15 - 13:50 | Nils Anders Danielsson |
| 13:50 - 14:25 | Christian Sattler |
| 14:25 - 15:00 | Max Zeuner |
| Coffee | |
| 15:40 - 16:15 | Robin Adams |
| 16:15 - 16:50 | Thierry Coquand |
| 18:00 | Dinner Andrum (map) |
The talks are in Analysen on the third floor of the EDIT building.
Titles and abstracts
Loīc Pujet: Countable choice in Observational Type Theory
Observational Type Theory is an internal language for types equipped with a proof-irrelevant propositional equality. As such, it natively supports extensionality principles, UIP, and quotients of types by proof-irrelevant relations (ā la Lean).
Unfortunately, it is difficult to use these quotients without any choice principles to extract information from proof-irrelevant truncations. In this talk, I will use ideas from Higher Observational Type Theory to sketch a version of OTT that supports countable choice for Delta00 predicates.
Nils Anders Danielsson: Graded modal type theory with identity types
Agda has support for erasure: one can mark things as erasable, and those things will be erased by at least one compiler backend. The idea is that the type system should ensure that the erasure does not affect the result of the compiled program.
Graded modal type theory is a formalism for type theory extended with a modality such as erasure. I will describe work on extending a formalisation of graded modal type theory, developed together with Andreas Abel and Oskar Eriksson, with identity types. One key result is that a well-typed, well-resourced term t of type ℕ reduces to a numeral n, and if one erases the erasable parts of t, then the resulting program also reduces to n. If "erased matches" are not allowed this holds even if t is an open term, as long as the free variables are marked as erasable and their types are mutually consistent.
Christian Sattler: Generalized algebraic homotopy theories
Generalized algebraic homotopy theories are a homotopical generalisation of generalized algebraic theories. As one instance, we recover the homotopy theory of type theories by Kapulkin and Lumsdaine. Inspired by recent work of Rafael Bocquet. Find notes here: https://www.cse.chalmers.se/~sattler/docs/gaht.txt
Max Zeuner: Schemes and size issues in constructive type theory
Schemes, the fundamental objects of modern algebraic geometry, are usually defined through locally ringed spaces. However, from the constructive point of view it seems advantageous to regard them as well-behaved functors from rings to sets. This comes at the cost of introducing size issues that pose a serious problem for a formalization in constructive type theory. In this talk we want to investigate to what extent these problems can be mitigated in a predicative type theory like Agda's. Parts of this have already been formalized in Cubical Agda and we will comment on how HITs and univalence can be of help.
Robin Adams: A(nother) fully formal Elementary Theory of the Category of Sets
The Elementary Theory of the Category of Sets (ETCS) is a first-order structural set theory which is often named as a categorical foundation of mathematics. Its primitive terms are set, function and composition (as opposed to set and membership as in ZFC). It is a structural set theory, meaning we can only talk about sets, groups, rings etc. up to isomorphism, not up to equality.
Its axioms are usually given in informal language. I am only aware of one attempt (by Trimble) to define it with a precise formal definition of its syntax and rules of deduction, and that attempt does not present it as a structural set theory; we can form the proposition f = g when f and g are functions between different sets.
I present a formal syntax and rules of deduction for ETCS as a dependently typed (or dependently sorted) first-order language. There is a type $\mathbf{Set}$ of sets and, for any terms $A$ and $B$ of type $\mathbf{Set}$, there is a type $A \rightarrow B$ of functions from $A$ to $B$. It is a structural set theory in that we may only form the proposition $f = g$ when $f$ and $g$ are functions with identical type $A \rightarrow B$.
This can be seen as a theory in Makkai's FOLDS (First-Order Logic with Dependent Sorts) or Aczel's DFOL (Dependently typed First-Order Logic), but we don't need anywhere near the full machinery of those frameworks.
I give semantics for the theory, and prove that the models are exactly the well-pointed toposes with a natural numbers object that satisfy the Axiom of Choice. I also prove the result that, if we can prove that a structure exists uniquely up to isomorphism, then adding constants for that structure to the theory is a conservative extension.