Types and Topology

Martín Escardó, professor in Theoretical Computer Science at the University of Birmingham, will turn 60 in November 2025. We are organizing a workshop to celebrate this occasion as well as Martín's diverse contributions to constructive mathematics, domain theory, locale theory, logic, topology and homotopy/univalent type theory.

The workshop will take place in Birmingham on 17 and 18 December 2025 and is co-located with the MGS Christmas Seminar on 16 December 2025.

There will be a Zoom livestream for the workshop.

Venue

Lecture Theatre 2
Alan Walters Building
University of Birmingham
Birmingham B15 2SB, United Kingdom

OpenStreetMap  Google Maps  Apple Maps

Registration

Attendance is by registration only and registration closed on 21 November.

Programme

Talk abstracts

Alex Simpson (University of Ljubljana, Slovenia)
Martín's interval in Scotland
(Provisional) I shall talk about the closed interval [1997,2000].

Andrej Bauer (University of Ljubljana, Slovenia)
How to use excluded middle safely
(Provisional) I will present preliminary joint work with Danel Ahman on oracle modalities.

Andrew Swan (University of Ljubljana, Slovenia)
The cohomology of the natural numbers in cubical assemblies
Cohomology groups have a natural definition for types internal to homotopy type theory (HoTT) and so can also be defined for objects of any model of HoTT. Since the cohomology groups are trivial for projective objects, one way of thinking about cohomology is as a "measure" of how the axiom of choice fails. In particular the cohomology group of the natural numbers being non trivial witnesses the failure of countable choice.
I will provide an explicit description of a suitable "externalisation" of the cohomology group of the natural numbers in cubical assemblies from an internal group in the model to an actual group. We can get an explicit description of the externalisation by examining details of the cubical set model, in particular propositional truncation, in a metatheory where the non classical axiom of Church's thesis holds. I will briefly sketch how to show some non trivial group theoretic properties of the resulting torsion free abelian group using some arguments based on computability theory: it has infinite rank, contains infinitely many copies of the rational numbers, and contains infinitely many pure elements but cannot be decomposed as a direct sum of the form Z ⊕ A.

Christopher Townsend (Independent researcher, UK)
Escardo's Patch
In this talk I will describe the context of the Patch construction as it was in 1995/6 when Escardo introduced his version. I was working on a very similar problem at the time, also at Imperial (we shared an office), but came up with a different construction. It was not until 2011 that I could answer the question: why are there different constructions? In the body of the talk I will show how this naturally comes about once we see the Patch construction process as the compact Hausdorff dual to the process of backing out the compact elements of an algebraic dcpo. I will then outline how Escardo’s Patch provides us with an example of a statement about compact Hausdorff locales that is expressible within the regular fragment of logic, but which is not mirrored by its discrete dual.
Time permitting I will point to areas where I think further research on the Patch could be considered; specifically an idea about extending the domain of definition to certain localic presheaves.

Dag Normann (University of Oslo, Norway)
Quantifiers in real analysis
Based on jww Sam Sanders
Inspired by results due to Martı́n Escardó we can see that a set X ⊆ 𝟚^ℕ admits a quantifier ∃x ∈ X(P(x)), computable in some f ∈ ℕ^ℕ and working for all predicates P, if and only if X is closed and countable. These quantifiers can be seen as functionals of type 3 computable in some f. For classical applications of quantifiers in real analysis we must go beyond this, make use of quantifiers normally represented by the functionals ∃²(∃n⁰) or ∃³(∃f¹), where the first is too weak for most purposes in ordinary mathematical analysis while the latter is far too strong.
In the NorSan project we consider partial quantifiers, subfunctionals of ∃³, and consider for how complex predicates P we need an oracle answering questions of the sort ∃f(P(f)). This is in analogy with how comprehension axioms are used in Reverse Mathematics.
In this talk we will survey some of the old results, and then discuss some recent observations relating the classes Fσ, Gδ and Fσ ∩ Gδ of subsets of reals. For the first two classes, we will need the axiom of choice to select a Borel code for each element of the class while for the third one we can select one computably in a very modest partial functional of type 3.
There will be some focus on motivation and on the foundational impact.

Dan Christensen (University of Western Ontario, Canada)
Diagram chasing in the Coq-HoTT library
Many facts about abelian groups and R-modules are proved using the technique of diagram chasing. For example, to prove that a certain map is surjective, one takes an element of the codomain and traces it through a diagram to eventually get a preimage. In more general abelian categories, the objects don't have elements, so to make this technique possible, one often relies on embedding theorems that depend on classical principles. Mac Lane proposed a method that does not use an embedding theorem, but which had limitations. We show that a simple extension of this method works quite well in practice, with the aid of a tactic that makes it appear that we are dealing with elements in a naive way. We will illustrate this with proofs of some standard results that exactly parallel the traditional proofs.
This is joint work with Thomas Thorbjørnsen.

Fredrik Nordvall Forsberg (University of Strathclyde, UK)
Representing type theory in type theory with inspiration from natural models
As a constructive foundation of mathematics, we expect type theory to be able to reason about its own syntax and semantics. However to precisely and conveniently represent type theory inside itself has turned out to be a longstanding open problem, with notable contributions by Dybjer, Danielsson and Chapman. A breakthrough was achieved by Altenkirch and Kaposi, who realised that quotient inductive-inductive types are well suited to represent the syntax of type theory up to definitional equality. Nowadays, the proof assistant Agda has support for quotient inductive-inductive types in its cubical mode, but unfortunately Altenkirch and Kaposi's construction is not accepted as-is by cubical Agda, due to equality transports confusing the strict positivity checker. I will present an alternative construction of the syntax of type theory, which is accepted in cubical Agda, this time as an quotient inductive-inductive-recursive definition. The addition of a recursive component is inspired by Awodey's notion of a natural model of type theory. This is joint work with Liang-Ting Chen and Tzu-Chun Tsai.

Gordon Plotkin (Google Deepmind)
Using the selection monad
In 2010, Martin and Paulo Oliva invented the selection monad
S(X) = (X → R) → R. Then, in 2017, they showed how to combine the selection monad with an auxiliary monad T to obtain the extended selection monad
S_T(X) = (X → R) → T(R), with R a T-algebra. These monads have applications to game theory, search algorithms, and proof theory.
Martin Abadi suggested a natural optimization interpretation of the selection monad: a selection function i.e., an element of S(X) chooses an element of X, given a loss (or profit) function γ : X → R that gives the loss (or profit) associated with a particular choice. Argmax provides a natural example of such a selection function: it makes optimal choices.
We illustrated this idea via a programming language for making optimal choices combined with probabilistic ones. Its denotational semantics uses the selection monad combined with an auxiliary monad for probability and nondeterminism. It has an operational semantics involving games against nature. And there are adequacy and (limited) full abstraction theorems for expectedly optimal selection functions.
However, in practice, one cannot, of course, make optimal choices, and programmers must employ learning algorithms such as reinforcement learning or gradient descent. I hint at a selection monad approach to this problem. It combines the selection monad with (a monad for) algebraic effects to obtain algebraic effects with choice continuations (work with Ningning Xie).

Hajime Ishihara (Toho University, Japan)
A constructive theory of uniformity and its application to integration theory
We introduce the constructive notion of a uniformity (uniform structure) with the spirit of Sambin's notion of a basic pair, and show some natural properties of a uniform space, a setoid with a uniform structure.
Then we construct a completion of a uniform space as a setoid of (regular) nets, define topological linear spaces and topological vector lattices as linear spaces and vector lattices equipped with uniform structures, and show that these algebraic and topological structures are preserved under the completion.
We introduce the notion of an abstract integration space consisting of a vector lattice and a positive linear functional.
By defining two uniform structures on an abstract integration space, we define corresponding topological vector lattices, and spaces of integration and measurable functions as the completion of these topological vector lattices.
Finally, we show some convergence theorems on these spaces such as Lebesgue's monotone and dominated convergence theorems and Fatou's lemma.

Ho Weng Kin (Nanyang Technological University, Singapore)
The "Collatz Problem" of domain theory: Is FS = RB?
In domain theory, finitely separated (FS) domains occupy a central place as they form one of the maximal Cartesian Closed subcategories of pointed domains. It is well-known that algebraic FS are exactly the bifinite domains, and this immediately raises the question: Are FS-domains exactly the same thing as retracts of bifinite domains? Domains of this latter form are referred to as RB-domains. The guiding analogy comes from the classical fact that every continuous domain can be realized as a retract of an algebraic domain, suggesting that a similar correspondence might hold in the context of FS-domains. This talk provides an accessible introduction to the problem of whether FS = RB. I will review the definitions of FS-domains, bifinite domains, and RB-domains, illustrating each with examples. We will then trace the motivations behind the conjecture, survey the latest known results, and discuss why the problem has remained resistant to solution. While this problem may seem to be a boondoggle as the title suggests, I hope to articulate the technical challenges explicitly and encourage the building of new tools to bring it down. This talk is a belated spin-off from one of those many weekly discussions with Martín Escardó during my good old PhD days.

Jon Sterling (University of Cambridge, UK)
What do mapping cylinders classify?
Although a mapping cylinder is a certain kind of (op)lax colimit, in some 2-categories like CAT and BTOP/S, mapping cylinders also enjoy a right-handed universal property that generalises the classification of (co)partial maps. If formulated naïvely as a principle of synthetic domain theory in Martin-Löf type theory extended by a dominance, this two-handed universal property is unexpectedly strong and renders the dominance discrete. We describe a more refined perspective in the setting of univalent foundations based on a strengthening of the Segal completeness law; from this we obtain a number of accessible reflective subuniverses of untruncated synthetic spaces within which mapping cylinders may be computed in terms of partial map classifiers, where lax and oplax orientation correspond to the choice of dominance.

Maria Emilia Maietti (University of Padua, Italy)
On the compatibility of dependent type theory with Brouwer's intuitionistic principles
In [Tro77], Troelstra showed that on Heyting arithmetic with finite types, the axiom of choice together with extensionality of functions contradict Brouwer's Local Continuity principle (LCP).
In [EX15], Martín Escardó and Chuangjie Xu refined such a result by showing that on Heyting arithmetic with finite types, it is enough to take the xi-rule of definitional equality between typed terms to show that the axiom of choice contradicts LCP. In particular, Martin-Löf's intensional type theory contradicts LCP and is therefore incompatible with Brouwer's intuitionism.
We show that there are dependent type theories compatible with Brouwer's intuitionism, and these include Coquand-Huet-Paulin’s Calculus of Constructions (CC_rocq) as implemented in the proof-assistant Rocq, and the two-level Minimalist Foundation (MF) in [MS05] and [M09].
Indeed, by modeling both foundations within constructive quasi-toposes of assemblies in [MST25], we show that CC_rocq and each level of MF are consistent with all Brouwer's intuitionistic principles, including LCP, the Zermelo (or relational) instance of the axiom of choice from the Baire space to the natural numbers; extensionality of functions; and a restricted form of Church's thesis establishing that all lambda-terms between natural numbers are computable, with the proviso that choice sequences are interpreted as functional relations.
This result is drawn as a consequence of the following other key facts:
- a suitable extensional version of CC_rocq, called eCC_rocq, is "the internal language of arithmetic solid quasi-toposes";
- CC_rocq can be interpreted in eCC_rocq (and it is equi-consistent with it) by using the same technique in [MS24];
- the intensional/extensional levels of MF are respectively predicative variants of CC_rocq and eCC_rocq without any large elimination of propositions.

This is joint work with Pietro Sabelli (Czech Academy of Sciences).

[EX15] M. Escardó, C. Xu. "The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation." TLCA, 2015
[M09] Maietti, M.E. "A minimalist two-level foundation for constructive mathematics." Annals of Pure and Applied Logic, 2009
[MS24] M. E. Maietti, P. Sabelli. "Equiconsistency of the Minimalist Foundation with its classical version." Annals of Pure and Applied Logic, 2025
[MS05] M. E. Maietti, G. Sambin. “Toward a minimalist foundation for constructive mathematics”. Oxford Logic Guides, 2005
[MST25] M. E. Maietti, P. Sabelli, D. Trotta. "Effectiveness and Continuity in Intuitionistic Quasi-toposes of Assemblies”. Submitted, 2025
[Tro77] A.S. Troelstra. "A note on non-extensional operations in connection with continuity and recursiveness." Indagationes Mathematicae, 1977

Nicolai Kraus (University of Nottingham, UK)
From Hedberg's theorem to truncation elimination and two-level type theory
In the early 2010s, when homotopy type theory was young, Martín and I had many discussions on Hedberg's Theorem and propositional truncation. These discussions shaped my PhD. At the workshop, I will talk about results that we found together, how they inspired me to study Shulman's Reedy fibrant inverse diagrams and Makkai's FOLDS, and eventually convinced me of the need for a second type-theoretic layer on top of homotopy type theory.

Paulo Oliva (Queen Mary University of London, UK)
Higher-order game theory
My collaboration with Martín Escardó on Higher-Order Game Theory began in 2007 (when we met in conferences in Brazil and Poland), with our first paper [1] published in 2010. At the time, I was studying bar-recursive interpretations of analysis, while Martín was developing selection functions as a computational interpretation of the topological notion of compactness. We soon observed that the construction underlying Tychonoff’s theorem (the product of selection functions) was very similar to Spector’s bar recursion. This insight led us to generalise the theory of selection functions and discover a new connection to the backward induction principle in game theory, used to compute sub-game perfect equilibria. In the years that followed, we continued to collaborate, now with a dozen papers exploring new applications of this theory to proof theory, game theory, and topology. In this talk, I will survey our main results and present an overview of our ongoing work in this area.
[1] Martín Escardó and Paulo Oliva, Selection functions, bar recursion and backward induction, Mathematical Structures in Computer Science, 20(2):127-168, 2010

Peter Dybjer (Chalmers University of Technology, Sweden)
Are universes open or closed?
In dependent type theory universes play a central role. It is sometimes discussed whether they are “open” or “closed”. On the one hand in a proof assistant such as Agda they are open in that you can add new data types in them at any point in your development. On the other hand, universes à la Tarski are special kinds of inductive-recursive definitions, which means that they closed and admit an induction principle. With this as a starting point I will discuss various aspects of universes.

Peter Schuster (University of Verona, Italy)
Terms for termination
When computing with polynomials over a field, (monic) monomials are the prime tool for termination and finite generation: among monomials, ideal membership is divisibility by a generator, and divisibility is the natural order on the exponents; in particular, Dickson’s lemma applies. Over a field, every non-zero term, i.e. monomial with coefficient, can be made monic, by inverting the coefficient. Over a general commutative ring, terms proper have proved a pivotal link to the polynomial ring, and in fact help to a constructive proof of the iterative Hilbert basis theorem with Noether's chain condition in Richman’s guise.
Joint work with Ihsen Yengui.

Steve Vickers (University of Birmingham, UK)
Escardó-Simpson interval objects and point-free trigonometry
In 2001 ([1]; but see [2] for a fuller version) Martín, together with Alex Simpson, gave a universal characterization of the closed Euclidean interval I = [-1, 1]. It addressed the problem of defining a path I -> X between two given endpoints in X. We wish the path to be analogous to the straight line for the case where X is a real vector space, and obviously some structure on X is needed if this is to be defined; but it would be cheating just to require X to be a real vector space because we seek an independent characterization of the reals.
Martín and Alex identified the structure on X as being information to specify the midpoint of any two points of X, together with an “iterativity” condition. Then the characterization of I is that it is the free iterative midpoint algebra on two points (its endpoints).
They proved this for point-set versions of I, but they also conjectured it might hold point-free, and I proved this in [3]. I shall briefly outline my proof: it illustrates some features of the “ultraminimalist” geometric point-free reasoning that set it apart from other styles of constructive reasoning.
I shall follow by explaining how arcs on the circle can be proved to be iterative midpoint algebras, and this can then be used towards defining sin and cos by wrapping I around parts of the circle.

[1] M. Escardó and A. Simpson, A universal characterization of the closed Euclidean interval, in: Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on, (2001), pp. 115–125.
[2] M.H. Escardo and Alex K. Simpson. Euclidean interval objects in categories with finite products. arXiv:2504.21551, 30 Apr 2025.
[3] Steven Vickers “The localic compact interval is an Escardó-Simpson interval object", Mathematical Logic Quarterly 63(6) (2017), pp. 614-629

Thierry Coquand (University of Gothenburg, Sweden)
Sheaf models of dependent type theory
I have had several interactions with Martin on the topic of sheaf models for type theory, in a constructive meta theory. In particular, we had several discussions in Princeton, 2012 and I started to write a suggestion for a sheaf model for choice sequences. As Martin found out with his former student Chuanghie Xu, this suggestion was too simple: Hofmann’s construction of universes in presheaf models cannot be simply generalised to sheaf models. I will try to present current research on this topic, with two possible examples.

Thomas Powell (University of Bath, UK)
Applications of proof theory in probability and stochastic optimization
It is an elementary fact from real analysis that any monotone bounded sequence of real numbers converges. It turns out that the monotone convergence theorem can be given an equivalent finitary formulation: roughly that any sufficiently long monotone bounded sequence experiences long regions where the sequence is metastable. This so-called "finite convergence principle" is carefully motivated and discussed by Terence Tao in a 2007 blog post ('Soft analysis, hard analysis, and the finite convergence principle'), but was already known to proof theorists, where the use of logical methods to both finitize infinitary statements and provide uniform quantitative information for the finitary versions plays a central role in the so-called proof mining program. The goal of my talk is to discuss how methods from proof mining can be applied to the theory of stochastic processes, an area of mathematics hitherto unexplored from this perspective. I will begin by discussing the simple monotone convergence principle, and will then focus on how everything I mentioned above can be generalised to the analogous result in the stochastic setting: Doob's martingale convergence theorems. This then sets the groundwork for new applications of proof theory in stochastic optimization, and I will give a high level overview of some recent work in this direction, joint with Morenikeji Neri and Nicholas Pischke.

Thorsten Altenkirch (University of Nottingham, UK)
The reals as a higher coinductive type
I will discuss how to define the signed digit reals à la Escardo/Simpson as a higher coinductive type. This is work in progress and I hope to get some input from Martin.

Ulrich Berger (Swansea University, UK)
Non-strictly positive induction for breadth-first search
Martin Escardo is well-known for his many contributions to mathematics and computer science. One of them is his analysis of "seemingly impossible functional programs" (see e.g. "Infinite sets that admit fast exhaustive search", Lics 2007). In his joint work with Paulo Oliva, he applied these types of programs to an amazing variety of areas such as sequential games, computable analysis, topology and logic (see e.g. "What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common", MSFP 2010).
In this talk I discuss another program, that has some similarity with Escardo/Oliva search, and that uses - somewhat surprisingly - a non-strictly positive inductive type to performs breadth-first search in a tree. The program goes back to Martin Hofmann ('Non strictly positive datatypes in system F', http://www.seas.upenn.edu/~sweirich/types/archive/1993/) and has been analysed from a type-theoretic and logical perspective (Ralph Matthes, Anton Setzer, B: "Martin Hofmann’s case for non-strictly positive data types", TYPES 2018 post-proceedings, LIPIcs 130).

Ulrik Buchholtz (University of Nottingham, UK)
Towards a synthetic mathematics of synthetic mathematics
I'll give an update on joint work with Johannes Schipp von Branitz and Mark Damuni Williams on devising a type theory for reasoning synthetically about synthetic mathematics. Synthetic mathematics using type theory leverages the interpretation of types as sheaves over a suitable (higher) topos, using principles that are only valid in that interpretation. This works one topos at a time. Recent work by Ingo Blechschmidt and others point the way towards systematically deriving these principles, and we build on this to propose a synthetic mathematics for synthetic mathematics, allowing a single theory to relate the synthetic mathematics of several toposes (including the base), beginning with the case of localic toposes. This touches on several aspects of Martín's work: constructive topology and domain theory, topos semantics, and constructive type theory.

Local information

For information on travel and accomodation, we kindly refer you to the local information page for FSCD 2025 which was also held in Birmingham.

Organizers

• Eric Finster (University of Birmingham)
  e.l.finster@bham.ac.uk
• Tom de Jong (University of Nottingham)
  tom.dejong@nottingham.ac.uk