My research blog posts.

Introduction to HoTT/UF with Agda.

(1) Timetable, (2) teaching, (3) Published and unpublished work, (4) research talks, (5) cv. (6) Mastodon (7) Twitter archive of the account I deactivated.

**Research interests:** Topology, topology in higher-type computation,
constructive mathematics, dependent type theory, univalent type
theory, homotopy type theory, domain theory, locale theory, exact real-number computation. My
research often stumbles upon category theory, proof theory and game
theory. (Dependent) functional programming is a useful and enjoyable tool for
practical manifestations of theoretical ideas in computation.

In research in mathematics and the theory of computation, what is interesting is what is incredible but true, defying our intuitions, giving new light to our understanding. This is of course the case for all sciences, and for engineering too. In the theory of higher-type computation, in the sense of Kleene and Kreisel, my favourite example is the characterization of the sets that can be exhaustively searched by an algorithm, in the sense of Turing, in finite time, as those that are topologically compact. In particular, this understanding gives examples of infinite sets that can be completely inspected in finite time in an algorithmic way, which perhaps defies intuition.

I am
also interested in constructive mathematics, which I see as a
generalization, rather than as a restriction, of classical
mathematics. In constructive mathematics, in the way I conceive it,
computation is a side-effect, rather than its foundation. What
distinguishes classical and constructive mathematics is that the
latter is better equipped to explicitly indicate the *amount of
information* given by its definitions, theorems and proofs, which
is related to topology and domain theory. This is particularly the
case for Martin-Löf type theory, and even more so for its
univalent extensions, such as Book HoTT
(homotopy type
theory)
and Cubical Type
Theory. Constructivity is not a binary notion, but a matter of
degree. The correct question is not whether a mathematical theorem is constructive, but instead how much information its formulation (type) and proof (inhabitant of the type) give. A good foundation has a rich
supply of types and ways to build their inhabitants so that the
available amount of information can be precisely expressed.

The above is a probably misleading, and certainly incomplete, hint of what my mathematical and computational research are about.

*The only difference between reality and fiction is that fiction needs to
be credible.* **Mark Twain**

*At least in theoretical things, you never set out to discover something new. You stumble on it and you have the luck to recognise what you've found is something very interesting.***Duncan Haldane**

I joined Birmingham University in September 2000. My first degree was from the Universidade Federal do Rio Grande Sul, where I also obtained an MSc degree by research. During my undergraduate and MSc studies, I worked in industry. I then went to Imperial College of the University of London in October 1993 for my PhD under the supervision of Mike B. Smyth. After completing this in April 1997, I was a postdoc for one year at Imperial, a lecturer at the University of Edinburgh for two years, and then at the University of St Andrews for one year, after which I came here and have happily been part of a vibrant theory research group (and department, too!).

Some mathematical and computational developments in Haskell and Agda, which are not supposed to fully represent what my work is about:

- Seemingly impossible functional programs (in Haskell).
- Real number computation in Haskell with real numbers represented as infinite sequences of digits.
- A Haskell monad for infinite search in finite time (in Haskell).
- Running a classical proof with choice in Agda (a blog post summarizes this).
- What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common.
- Various new theorems in constructive mathematics developed in a constructive univalent type theory using Agda.
This includes, among other things:

- The conatural numbers (or extended natural numbers, or the one-point compactification of the discrete space of natural numbers) are exhaustibly searchable, despite the fact that they form an infinite space (also known as the generic convergent sequence), and so are many more infinite types.
- The universe of all types is indiscrete (see also a brief blog post with links to an older agda version).
- Rice's Theorem for the universe as a corollary.
- The universe is injective, which is used as a lemma in the indiscreteness theorem.

This is also briefly reported as a blog post with links to an older version.

- Using Yoneda rather than J to present Martin-Löf's identity type.
- Continuity of Godel's system T functionals via effectful forcing.
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation.
- Univalent logic.
- A small type of propositions a la Voevodsky in Agda. This uses Type:Type in only one module.
- This uses rewriting instead.
- This lives with the fact that the type of propositions is large, and also discusses a large propositional truncation a la Voevodsky and its relation to the small one (if it exists).
- This uses rewriting only to make propositional truncations a la Voevodsky small. Everything else retains its native universe level.

- Agda discussion about propositional truncation, function extensionality, and turning any factorization via the propositional truncation of the domain of a function into a judgmental one. It includes the fact that the interval is the propositional truncation of the booleans, which gives the germ of the idea for the factorization.
- Generalizations of Hedberg's Theorem.
- The empty type has a constant endomap (the identity function). Any type that has a given point has a constant endomap (that maps everything to that point). If every type has a constant endomap, then every type has decidable equality, which implies WLPO and other constructive taboos.
- Dummett disjunction in Martin-Löf Type Theory.

**Email**: m.escardo@bham.ac.uk**
office**: 140 **Directions: **Look for building Y9 in the yellow zone of
the Edgbaston
campus map. This is
about 1 minute walking time from the train station. Turn left when you
exit the station, and walk for about 30 meters. Our building is the
right-hand one of two red-brick twin buildings facing each other.

Last modified: Monday July 1 11:46:55 UTC 2024