Memorial Conference for Erik Palmgren, 1963–2019

Rescheduled to online, 19–21 Nov 2020

Erik Palmgren, professor of Mathematical Logic at Stockholm University, passed away unexpectedly in November 2019.

This conference will be an online workshop to remember and celebrate Erik's life and work. There will be talks by Erik’s friends and colleagues, as well as time for discussions and exchange of memories during breaks. Talks may be about any topics that Erik would have enjoyed, including but not limited to (in Erik’s words):

Obituary — Erik’s homepage

Registration

The meeting will take place online, over Zoom.

To receive the Zoom link/password and other updates, please register by sending your name + email address to palmgren-memorial@math.su.se in advance. The Zoom details will be sent to registered participants the day before the conference starts. (We are not posting them publicly, to prevent Zoom-bombing.)

If you are registering later, or didn't receive the email, please write to palmgren-memorial@math.su.se and we will reply as soon as possible with the Zoom information.

Program

Recordings of the talks can be found here.

All times are Central European Time (UTC+1).

Thursday 19 Novmorning (chair: Anders Mörtberg)
9:00–10:00 Douglas Bridges — Representing preferences on a metric space. Abstract, video.
10:00–10:40 Peter LeFanu Lumsdaine — From setoids to e-categories to (un-)saturated categories; or, how Erik taught me to stop worrying and love the setoids. Abstract, slides, video.
10:40–11:20 Christian Espíndola — An extension of Morley's categoricity theorem to infinite quantifier languages. Abstract, slides, video.
Thursday 19 Novafternoon (chair: Håkon Gylterud)
13:30–14:30 Benno van den Berg — A topos for continuous logic. Abstract, video.
14:30–15:10 Chaitanya Leena Subramaniam — Dependently typed theories as generalised Lawvere theories. Abstract, slides, video.
15:10–16:10 Steve Awodey — An algebraic proof of the Frobenius condition for cubical sets. Abstract, slides, video.
Friday 20 Novmorning (chair: Peter LeFanu Lumsdaine)
9:00–10:00 Hajime Ishihara — Yet another predicative completion of a uniform space. Abstract, slides, video.
10:00–10:40 José Siqueira — A tripos-theoretic approach to nonstandard analysis. Abstract, video.
10:40–11:20 Anders Mörtberg — The structure identity principle in Cubical Agda. Abstract, video.
Friday 20 Novafternoon (chair: Christian Espíndola)
13:30–14:30 Nicola Gambino — Type-theoretic interpretations of constructive set theories: a survey. Abstract.
14:30–15:10 Håkon Gylterud — Univalent set theory. Abstract, video.
15:10–16:10 Steve Vickers — Arithmetic universes: Home of free algebras. Abstract, slides, video.
Friday 20 Novevening
18:00– Social event over Zoom: please bring a drink (preferably whisky) for a toast in Erik's memory. Group photo

Saturday 21 Novafternoon (chair: Henrik Forssell)
13:30–14:30 Maria Emilia Maietti — What notion of predicative topos? Abstract, video.
14:30–15:10 Jacopo Emmenegger — Equality is coalgebraic. Abstract, video.
15:10–15:50 Johan Lindberg — Palmgren's Intuitionistic Ramified Type Theory. Abstract, video.
15:50–16:30 Peter Dybjer — Erik Palmgren and the Higher Infinite in Type Theory. Abstract, video.

Talks

Douglas Bridges — Representing preferences on a metric space

Among the many theorems proving the existence of utility functions representing abstract preference relations in mathematical microeconomics, one of the most attractive is the Arrow-Hahn theorem, a constructive version of which I developed in the 1980s. However, that theorem applies only to preferences on convex subsets in Euclidean space, whereas other classical theorems are set in more general topological spaces. In this talk, I present a new, more general, constructive version of the Arrow-Hahn theorem where the consumption set is a metric space.

Peter LeFanu Lumsdaine — From setoids to e-categories to (un-)saturated categories; or, how Erik taught me to stop worrying and love the setoids

It is common in constructive/type-theoretic mathematics to work explicitly with setoids — types equipped with an equivalence relation — where classical mathematicians would take a quotient and work with the resulting set. This has clear advantages — less foundational commitment, better computational content — but also disadvantages — some pitfalls in definitions, more boilerplate lemmas, and (debatably) less mathematical clarity.

The HoTT development of category theory, with its notion of saturated (aka univalent) categories, sheds interesting new light on this situation: there is a precise analogy between the use of setoids in constructive mathematics, and the use of (non-saturated) categories in traditional mathematics. Indeed, the setoid based e-categories (developed by Erik, among others) show up naturally in the HoTT analysis as a maximally unsaturated notion of category.

I'll present this comparison, and (more hand-wavily) discuss what insights it may suggest about our use of setoids in practice.

Christian Espíndola — An extension of Morley's categoricity theorem to infinite quantifier languages

Morley's categoricity theorem states that a countable first-order theory categorical in some uncountable cardinal is categorical in all uncountable cardinals. Shelah's categoricity conjecture states that a similar eventual categoricity behavior holds for certain infinitary theories in finite quantifier languages. In this talk we will explain the main ideas behind a version of eventual categoricity for theories in infinite quantifier languages. On the categorical side this corresponds to accessible categories, where the notion of internal size is taken instead of the cardinality of the underlying model. We will motivate this first with some examples computing the categoricity spectrum of infinite quantifier theories. We will also mention how the use of large cardinals can replace model-theoretic assumptions like directed colimits or amalgamation and to which extent the Generalized Continuum Hypothesis can be avoided through forcing techniques.

Benno van den Berg — A topos for continuous logic

Continuous model theory is a branch of model theory with applications in analysis, in which one interprets formulas in metric spaces and logical connectives as uniformly continuous operations. Together with Daniel Figueroa, we tried to give an account of the basic concepts in the area in the spirit of categorical logic. I will sketch some ideas, results and conjectures.

Chaitanya Leena Subramaniam — Dependently typed theories as generalised Lawvere theories

Lawvere theories and (coloured, symmetric) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections.

We extend this to dependently-sorted algebraic theories: For a direct category C, we show how suitable "C-sorted contextual categories" may be viewed as monoids in a category of "C-collections", and also as generalised Lawvere theories in the sense of Berger–Melliès–Weber. When C is a set, we recover the usual definition of C-sorted Lawvere theory.

We obtain a correspondence between C-sorted contextual categories and finitary monads on [Cop, Set], generalising the well known theorem for Lawvere theories. This immediately gives us many examples of such theories from well known finitary monads on globular sets, opetopic sets, semi-simplicial sets and planar collections.

Operads correspond to those Lawvere theories that admit a regular or linear presentation. It is natural to ask whether certain "regular" C-sorted contextual categories correspond to "dependently coloured operads". I will present some possible ideas in this direction.

The original inspiration for this work was Erik Palmgren's DFOL signatures. This is j.w.w. Peter LeFanu Lumsdaine.

Steve Awodey — An algebraic proof of the Frobenius condition for cubical sets

In a paper from 2003, Erik showed that the 1-category of groupoids is not locally cartesian closed, but that the 2-category is weakly so, opening the door to higher categorical models of type theory. As he told me at the Mittag-Leffler special year in 2001, this result was related to the never-completed third paper in the series with Moerdijk, which was to be on higher categorical models of intensional type theory. Recent work on cubical models of homotopy type theory is directly descendent from these seminal ideas, with cubical Kan complexes figuring as higher-dimensional groupoids. In this setting, the Frobenius condition is equivalent to the existence of the dependent products required to model Pi-types. We give an entirely algebraic, and therefore constructive, proof of Frobenius for cubical sets. The proof is a reworking of one originally given by Thierry Coquand in cubical type theory.

Hajime Ishihara — Yet another predicative completion of a uniform space

We give a predicative completion of a uniform space with pseudometrics by means of the notion of a net. Since the notion of a net is a generalisation of the notion of a sequence, the completion is a generalisation of, and parallel to the usual completion of a metric space. The completion is given in the elementary constructive set theory ECST with Exponentiation Axiom Exp. Since ECST+Exp is a subsystem of the constructive and predicative Zermelo-Fraenkel set theory CZF, we do not make use of Fullness, an axiom of CZF.

José Siqueira — A tripos-theoretic approach to nonstandard analysis

A natural approach to nonstandard analysis is to categorify the classical semantics for it by suitably replacing the notion of ultrapower, as done by E. Palmgren and I. Moerdijk. Alternatively, one could start with a syntactic perspective such as E. Nelson's internal set theory (IST), which partly inspired Palmgren's constructive type-theoretic version, and use tripos theory to turn the new quantifiers ∀st and ∃st into the quantifiers of a topos. This turns out to be in line with the point of view brought forth by A. Kock and C. J. Mikkelsen, according to which the transfer principle is captured by the idea that any Heyting functor between toposes factors through a third one, whose objects represent the internal subsets of standard sets. I will discuss how such "triposes of internal objects" can be built, and how the axioms of IST should be interpreted in this setting.

Anders Mörtberg — The structure identity principle in Cubical Agda

One of the most striking consequences of univalence is the structure identity principle (SIP) which states that equivalent structured types are identifiable. There are multiple ways to formalize this principle in homotopy type theory and I will discuss a variation that we have recently formalized in Cubical Agda. The constructive nature of cubical type theory allows us to reap the full benefits of the SIP, making it possible to transport programs and proofs along paths constructed using the SIP without losing computational content. We have applied this to a wide variety of examples in the Cubical Agda library, including algebraic structures, unary and binary numbers, matrices, queues, and finite multisets.

Nicola Gambino — Type-theoretic interpretations of constructive set theories: a survey

Erik Palmgren kindly acted as external examiner for my PhD thesis as well as for the one of my first PhD student, Cesare Gallozzi. Both theses include variations over Peter Aczel's celebrated type-theoretic interpretations of Constructive Zermelo-Fraenkel (CZF), which Erik used also in his work on setoids and Algebraic Set Theory. These variations are obtained by modifying how set-theoretic formulas are interpreted in type theory, using alternatives to the propositions-as-types idea. In particular, Cesare Gallozzi studied intepretations of CZF in type theory using ideas of Homotopy Type Theory. This talk will give a survey of these interpretations and outline some directions for future work.

Håkon Gylterud — Univalent set theory

From the perspective of HoTT, classical and constructive set theory are situated on homotopy level zero. However, many set theoretical axioms have natural extensions to ∈-structures on higher h-levels. This talk will present some of these generalised axioms, in particular Aczel's anti-foundation axiom.

There are two natural hiearchies of ∈-structures stratified by h-levels – one inductive, the other coinductive – which generalise the model for set theory presented in the HoTT book. The inductive hierarchy presented here is related to, but not the same as the one given by Cesare Gallozzi.

Steve Vickers — Arithmetic universes: Home of free algebras

Every algebraic theory (operators and equational axioms) has an initial model using a well known term/congruence construction, a term algebra modulo a congruence generated from the axioms. The result also holds (see [BarrWells:TTT]) for finite limit theories, aka cartesian or essentially algebraic; however, the term/congruence proof breaks down. Operators may be partial, and factoring out the congruence may cause new terms to be defined.

In my 2007 paper with Erik, Partial Horn logic and cartesian categories [PV:PHLCC], we showed how to simplify the development using a logic of partial terms, with definedness as self-equality. In this logic the term/congruence process uses partial terms and a partial congruence, and does construct an initial model. One class of cartesian theories that we discussed is that of category with structure and internal T-model, and the initial model is then a classifying category for T.

In my talk I shall focus on Joyal’s arithmetic universes (AUs), pretoposes with parametrized list objects. They face two ways. On the one hand, the theory of AUs is cartesian. On the other, the internal logic of AUs is sufficient to support our term/congruence construction of initial models. I shall present an overview of facts, conjectures, and mysterious phenomena. These include internalization (Joyal’s original motivation, for Goedel’s Incompleteness Theorem) and applications to base-independent geometric logic and classifying toposes.

[PV:PHLCC]: https://www.cs.bham.ac.uk/~sjv/papersfull.php#PHLCC
[BarrWells:TTT]: http://www.tac.mta.ca/tac/reprints/articles/12/tr12abs.html

Maria Emilia Maietti — What notion of predicative topos?

I. Moerdijk and E. Palmgren [MP02] were the first to propose a predicative analogue of the notion of elementary topos, with the aim of providing a categorical setting in which to model a constructive predicative theory such as Aczel's CZF. Their work actually opened a line of research later pursued also by other authors with different proposals.

In this talk, after discussing our general criteria for naming a structure "predicative topos", we present a definition of predicative topos such that:

  1. its generic internal language is strictly predicative à la Feferman, and when it satisfies a reducibility property à la Russell it becomes an elementary topos; hence each elementary topos is an instance of a predicative topos;
  2. it includes as examples the category of setoids over Martin-Löf's type theory (whose properties have been recently proof-checked in Agda by Palmgren in [P19]) and predicative realizability toposes including [MM20];
  3. it allows a straightforward generalization to a notion of "predicative quasi-topos".

[MM20] A predicative variant of Hyland's Effective Topos. M.E. Maietti and S. Maschio. To appear in Journal of Symbolic Logic, 2020
[MP02] Type theories, toposes and constructive set theory: predicative aspects of AST. I. Moerdijk, E. Palmgren. Annals of Pure and Applied Logic 114 (2002) 155–201
[P19] From type theory to setoids and back. E. Palmgren 2019, arXiv:1909.01414

Jacopo Emmenegger — Equality is coalgebraic

Lawvere’s hyperdoctrines mark the beginning of applications of category theory to logic. Recall that a doctrine is just a family of posets indexed on a category with finite products. In the spirit of functorial semantics, equality is specified requiring left adjoints to certain reindexing functors. These are most naturally formulated in the presence of conjunctions, giving rise to elementary doctrines. I shall present a recent result, obtained with Fabio Pasquali and Pino Rosolini, showing that elementary doctrines are 2-comonadic over doctrines with conjunctions. As it turns out, the underlying functor is the well known functor that adds quotients of equivalence relations. Indeed, the comonad giving rise to elementary doctrines is tightly related to the monad giving rise to elementary doctrines with quotients. After describing the connection, and if time allows, I shall discuss how to generalise this result to show that (non-faithful) elementary fibrations are comonadic over fibrations with products.

Johan Lindberg — Palmgren's Intuitionistic Ramified Type Theory

I’ll discuss Palmgren’s Intuitionistic Ramified Type Theory from [Pal18] as a syntactic approach to predicative/ramified topos-theory. This talk will mostly be expository, where I will present this formal system, and an extension with inductive definitions, as well as some work of mine regarding its categorical properties.

[Pal18] E. Palmgren, A constructive examination of a Russell-style ramified type theory, Bulletin of Symbolic Logic, 24(1), 2018, arXiv:1704.06812

Peter Dybjer — Erik Palmgren and the Higher Infinite in Type Theory

Erik Palmgren's work on universe operators, the superuniverse, and higher order universe operators was a starting point for the exploration of the higher infinite in type theory. I will recall some of Erik's contributions and emphasise their importance for the foundations of constructivism. Moreover, the advent of univalent mathematics has highlighted the need for a good formulation of rules for universes and universe polymorphism in type theory. Marc Bezem, Thierry Coquand, Martin Escardo and I are currently investigating several options, and I will discuss the relevance of Erik's work here too.

Organizers

The memorial conference is organized by Erik’s students and colleagues at Stockholm University:

For any questions, please email palmgren-memorial@math.su.se.