Martin Escardo

Professor at the University of Birmingham, UK.
I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more.

See my meta-blog:
https://cs.bham.ac.uk/~mhe/blog.html

Public Key

npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4

NIP-05 Address

MartinEscardo@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqs9ce6luatpc5hjcr4gmvu36tp6ge2khmy68s9ykncs7g60uql43jspz4mhxue69uhhyetvv9ujuerfw36x7tnsw43q8xecn5

Publishing to

relay.ditto.pub

Author Public Key

npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4

Show more details

Last Notes

2026-03-26 06:47:03 UTC

I have a calculator that is correct 80% of the time. But don't worry, every time I use it, I check the results myself.

2026-02-05 19:43:13 UTC

- reply

Continued.
And one more thing.
When going somewhere by car or by bike, it is counter-productive to try to be fast.
It won't make a significant net difference in terms of time. Do the computations yourself.
It will just add to your, and other people's. stress.

2026-02-05 19:31:27 UTC

- reply

Continued.
This is why three+ years ago I decided to start commuting by bike. But I needed an ebike because there is a rather steep hill when I come back home.
I only chose this option because only 11% of my commute is by road competing with cars. The rest is in two (connected) canals.
And there is a big plus! Going by bike takes a predictable 19-22min, Whereas going by car takes an unpredictable 40-60min, plus time to find car parking space, and then walk to my office. Equally horrible on the way back home.
My self-imposed rules, in my bike commute are (1) be mindful of people walking in the canal, (2) thank them when they make space for me, (3) don't get upset with cyclists who are slower or faster than me - after all, I deliberately chose to commute by bike to get rid of the car-driving stress. So getting upset is not in the menu.
As a bonus, the bike ride in the canal is beautiful nature, so that I enjoy the commute rather than cursing it.

2026-02-04 23:35:26 UTC

- reply

@nprofile…qvyx Road rage is a phenomenon, indeed. But that is not the phenomenon I described (or intended to describe).

2026-02-01 22:31:22 UTC

- reply

@nprofile…lfhd I haven't. Do you recommend it?
@nprofile…4hp5

2026-02-01 21:58:37 UTC

- reply

@nprofile…4hp5 Small world. 🙂

2026-02-01 16:28:34 UTC

- reply

@nprofile…twjf Yeah, A is stronger than B if A implies B. So false is the strongest proposition.

2026-01-30 19:51:36 UTC

Controversial claim.
Constructive mathematics is not about computation.
It is about better (or maybe just natural?) mathematical intuitions.

2026-01-30 19:13:59 UTC

- reply

@nprofile…s7d2
I don't understand the question.
@nprofile…z2n3 @nprofile…4hp5

2026-01-30 18:05:01 UTC

- reply

@nprofile…z2n3 Answering your question.
Sketch of recursive definition:
(1) Prove that the type I gave is well-founded.
(In fact, in constructive mathematics, and in particular in TypeTopology, the definitions of ω² is precisely what I gave as an alternative, via the lexicographic order.)
(2) Then use well-founded recursion on that well-ordered type using (1).
In practice, this means defining the next value of Ackerman assuming that you have all previous values available. Here we don't need all of them, just the "previous" one, which is available under the assumption.
In TypeTopology we have all the necessary machinery to do this, and I am tempted to do this myself as a nice example in the `gist` folder, but right now I don't have time to indulge myself in such nice exercises.
(However, if anybody listening here would like to contribute a `gist` about this in TypeTopology, and then report back here, this would be very welcome.)
@nprofile…4hp5 @nprofile…s7d2

2026-01-28 11:46:16 UTC

- reply

@nprofile…pw0n @nprofile…xuzd @nprofile…l3hr
I do something similar in TypeTopology (in Agda). My casts/coercions are all called ι (with a synonym [_]), defined by a typeclass.
I use this not only for casts/coercions but also for "canonical maps".

2026-01-27 21:46:11 UTC

- reply

@nprofile…2p65
For the record, I disagree.
@nprofile…xdkd

2026-01-27 20:33:30 UTC

- reply

@nprofile…ldyp writes "Are you implying that judgemental equality is about syntactic terms?"
When you do mathematics inside type theory, there are no theorems than mention judgmental equality. There can't be.
There are only metatheorems about it. Judgmental equality is needed only to define the well formed types and terms.
Andrej also writes "Existential reflection seems clearer: if a theorey proves an existential statement, then there is a term witnessing the statement. That's just the well-known existence property."
Not quite. The existence property holds in the *empty* context only.
Anyway, I shouldn't have started this thread, and I regret I did.

2026-01-27 19:24:58 UTC

- reply

[quotation continued from the previous post]
"This transition is the result of extensive reflection and many discussions with all concerned parties. We were forced to begin this work in 2024 following ACM's decision to raise SIGs contributions from $10K to $25K— a move that would have spelled the end for SIGLOG. While ACM reverted this rise in November 2025, the situation remains uncertain. Previously, the $10K SIGLOG contribution was offset by $10K in income from the ACM Digital Library; however, this revenue is not guaranteed at this stage. You may also recall a questionnaire we organized in June 2025, where we asked for your opinion on going independent or joining SIGPLAN (which was the only alternative at the time). We sent an email to approximately 750 people and received 318 responses, of which 79% preferred independence and 16% favored joining SIGPLAN.
Given the significance of this shift, the LICS Steering Committee self-imposed a two-thirds majority threshold for this decision to be enacted. This self-imposed requirement has been met."

2026-01-27 19:24:24 UTC

I got this message from LICS:
"At the end of December 2025, the LICS Steering Committee decided that LICS 2026 will not be sponsored by ACM nor IEEE. In particular, the proceedings of LICS 2026 will be published by LIPIcs. LICS 2026 will be a part of the FLoC 2026 meeting; of the ten main conferences at this meeting, nine will be run independently, while one will be sponsored by the IEEE.
The main reasons for this decision are:
- Organizing the conference independently is more efficient and avoids the surcharge currently applied to all conference costs by ACM/IEEE.
- LIPIcs offers high-quality, open-access publishing with a transparent and sustainable cost structure.
- Independence ensures that the organization of our community remains in our hands, rather than being determined by external forces that we can neither control nor influence.
We have decided to reevaluate our decision after FLoC 2026 because we wish to fully understand the implications of this change on the organization of future FLoCs, which we consider a major asset to the community. A final decision will be taken after FLoC 2026.
[continued in the next post]

2026-01-26 22:20:50 UTC

- reply

@nprofile…xdkd Can I "favourite" some parts of your message but not others?
🙂

2026-01-26 22:07:49 UTC

- reply

@nprofile…xdkd For now, I will only say that the fact that a particular model validates equality reflection doesn't justify it universally.
I still think that equality reflection confuses language and metalanguage.

2026-01-26 20:51:34 UTC

- reply

@nprofile…gy4l
Universal-quantification reflection:
If something can be metaproved proved for all (syntactical) **terms** (rather than elements) of a type, then it can be proved for the universal statement for elements of that type, by a metarule saying so.

2026-01-26 20:36:16 UTC

I don't want to pollute a well-intentioned thread in my feed.
So I say this here in a new thread.
1. Equality reflection, in MLTT, confuses language and meta language.
2. It also makes type checking undecidable, which is worse.
But the real problem is (1), not (2).
Consider, e.g., universal-quantification reflection. Nobody in their sane mind would do that. Or existential-quantification reflection.
Using (2) as the reason for disregarding equality reflection is wrong.
The real reason for considering equality reflection an abomination is (1), not (2).

2026-01-24 19:10:03 UTC

- reply

@nprofile…lfhd I lose it everyday for the same reason, as probably do you. 😞

2026-01-24 18:45:22 UTC

Mistake. I've just read the news.

2026-01-21 09:03:38 UTC

- reply

@nprofile…4hp5 writes "though he may be tired of talking about it."
🙂
Lean is better for classical mathematics, both because of its large mathlib and its community.
Agda is better for other things, in my case (constructive) homotopy type theory.
You can define tactics in Agda, but generally people prefer to write terms.
Then there is Rocq, which is good for both, and does have tactics.
Agda is based on Martin-Löf type theory, Rocq on the Calculus of Inductive Constructions, and Lean on something similar to Rocq (you would have to check the literature for precise details).
I hope this helps. Other people can say more.
@nprofile…jrcx

2026-01-20 18:25:40 UTC

- reply

@nprofile…xhtk Is there a general theorem behind this?

2026-01-20 18:17:38 UTC

- reply

@nprofile…r0xq I couldn't agree more with you.

2026-01-16 22:55:43 UTC

- reply

@nprofile…st9f I've just asked ChatGPT to summarize your post.
It said: "If they were good for you, shareholders would hate them."
🙂

2026-01-16 22:11:47 UTC

Luckily there isn't a Noble prize in mathematics.

2026-01-16 20:40:49 UTC

- reply

@nprofile…g0zc But, isn't it, to a large extent, regarding what history records?

2026-01-14 23:06:51 UTC

- reply

@nprofile…qvyx Nice. And when was that, for the record?

2026-01-14 22:53:25 UTC

This is a new application of AI:
"West Midlands police chief apologises after AI error"
Before we used to blame computers. Now there is a new culprit.

2026-01-14 21:35:19 UTC

How many of you listening here can claim that their very first computer program was written in punched cards?
The very first computer program I wrote was in the programming language Algol in a B6700 computer, typed in punched cards (one card per line).
You punched the cards, then you put them in a pigeonhole, and the next day you would collect the printout with the result of the compilation and running the program.
So you'd better make sure you got everything right the first time, as otherwise you would need to wait for 24hrs to try again.
This was in 1982, in my second last year of high school (at Colégio Anchieta in Porto Alegre, Brazil).
The B6700 computer belonged to UFRGS (Universidade Federal do Rio Grande do Sul), and somehow our school was allowed to use it. In fact, the teacher of that course was a person from UFRGS working at the CPD (Centro de Processamento de Dados).
The B6700 computer was well ahead of its time, already in the early 1970's. Search it!
You will see that it had features that only recently current CPU's are trying to catch-up with regarding security.

2026-01-13 21:40:34 UTC

Idle thought. If, as in the UK, your "biological sex" is that registered at birth, then there is a related concept of biological father, that registered at birth, even if a DNA test proves this otherwise.
In the same vein, in another thread, @nprofile…xhtk introduced the concept of biological name, which I love.
In the UK you can rectify your biological father and your biological name, but not your biological sex. I wonder what rationale the supreme court is applying.

2026-01-12 20:22:45 UTC

It is interesting see that Plato is now considered to be woke in a country that shall not be named.
When I just discussed this with my wife, she said she never knew that Plato was well ahead of his time.

2026-01-11 22:48:08 UTC

- reply

@nprofile…azwq The answer is somewhere in this thread already from yesterday, but here it goes again:
"M-q (translated from <escape> q) runs the command
prog-fill-reindent-defun (found in agda2-mode-map), which is an
interactive native-comp-function in ‘prog-mode.el’.
It is bound to M-q.
(prog-fill-reindent-defun &optional ARGUMENT)
Inferred type: (function (&optional t) t)
Refill or reindent the paragraph or defun that contains point.
If the point is in a string or a comment, fill the paragraph that
contains point or follows point.
Otherwise, reindent the function definition that contains point
or follows point.
Probably introduced at or before Emacs version 30.1.
[back]"
As you can see, it has to do with the Agda mode.
**However**, if I start a fresh emacs without Agda, I get this after your key sequence:
"M-q (translated from <escape> q) runs the command
prog-fill-reindent-defun (found in lisp-interaction-mode-map), which
is an interactive native-comp-function in ‘prog-mode.el’.
It is bound to M-q.
(prog-fill-reindent-defun &optional ARGUMENT)
Inferred type: (function (&optional t) t)
Refill or reindent the paragraph or defun that contains point.
If the point is in a string or a comment, fill the paragraph that
contains point or follows point.
Otherwise, reindent the function definition that contains point
or follows point.
Probably introduced at or before Emacs version 30.1."
And I have this after the very end of my "~/.emacs":
(global-set-key "\M-q" 'fill-paragraph)
But it doesn't work.

2026-01-10 20:36:09 UTC

Esc-q stopped working for me in emacs to justify paragraphs. Google search doesn't work for me (it does find related things, which don't apply to me). Any ideas?

2026-01-09 23:05:00 UTC

- reply

@nprofile…4hp5 Isn't this an instance of the fact that ideas tend to be discovered simultaneously by many people at about the same time, but some particular people push them further?
(For example, this happened regarding Darwin with evolution. But even the piano was invented twice at the same time independently, as an improvement or modification of previously existing keyboard instruments.)

2026-01-09 08:50:30 UTC

- reply

@nprofile…ldyp In our garden I've just measured 15cm.
This is what the amber warning says:
https://weather.metoffice.gov.uk/warnings-and-advice/uk-warnings/gcqdjh2qs#1ae0aefe-a04c-4569-83a8-10f40cb1c0dd
The railways were closed last night until the afternoon. In the airport "reduced runway operations have resumed".
There is almost no car traffic in the roads close to our house, and usually at this time there are a lot of cars taking people to our and/or schools.
We had an "Education away Day" in our department today, but it was cancelled.
I think the amount of snow is similar to when you came for the UniMath School in 2019.
The thing is that there isn't infrastructure to cope with the snow, even more after snow has become "rare", as in the words of the Head Master I quoted above.

2025-12-31 13:08:44 UTC

- reply

@nprofile…63jn One possible way to understand this is that you are working in an arbitrary mathematical universe, where in some universes excluded middle holds, and it others it doesn't (and yet others, it doesn't hold or fail). Such universes can be (elementary, or Grothendieck, or ∞-) toposes.
This is like when you are working with an arbitrary group - it may or may not be abelian. Or when you are working with a geometry, which may or may not satisfy the parallel postulate.
I discussed this point of view in this blog post a few years ago:
https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/

2025-12-30 23:59:54 UTC

I am 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.

2025-12-26 18:48:39 UTC

- reply

@nprofile…356e Can it cope with TypeTopology or agda-unimath?
I think I was meaning to have my *favourite* proof assistant to deal with this. And you can guess what my favourite proof assistant is. 🙂

2025-12-26 18:38:10 UTC

Wish for the new year: let proof assistants have flags for specifying precisely which type theory we want to work with.
There are many (dependent) type theories.
But some of us want to work with particular ones, for mathematical purposes of various kinds.
Wouldn't it be nice if we could control which type theory we want to work with, for
whichever purpose we have in mind?
I would love my favourite proof assistant to support the type theory I have in mind.

2025-12-24 18:46:33 UTC

- reply

@nprofile…8eua writes "We give the notes letter names. [...] A,B,C,D,E,F,G"
Thanks for the nice thread.
I think I've already said this here a few years ago. I find it very difficult to get used to use "A,B,C,D,E,F,G" automatically without thinking. I grew up playing musical instruments with "do, re, mi, fa, sol, la, si" corresponding to "C,D,E,F,G,A,B".
Question. I know the origins of the two notational systems. But why does one start with "A/la" and the other with "do/C"?
You kind of mention this in (5/n).
But when did this actually occur?

2025-12-23 18:14:17 UTC

- reply

@nprofile…n7dy writes " "We give you the wrong answer faster than any other system"
This works pretty well here, too. 🙂

2025-12-22 15:15:32 UTC

Some people here get upset when I wonder about things people wondered about before me themselves.
Rather than getting upset and giving a speech, please give the references in a polite an educative way.
More importantly, give the conclusions, rather than just saying "lots of people thought about this, including myself, and published papers about this".
It is not like I am trying to invade your territory.
Science, including mathematics, is a social process, not an unsocial one.

2025-12-21 17:23:36 UTC

TypeTopology is not a library (although it can be used as such, I guess).
It is primarily a blackboard to write papers intended for publication.
So far ~25 publications have arisen from TypeTopology, and you can see them here:
https://github.com/martinescardo/TypeTopology?tab=readme-ov-file#publications-resulting-from-typetopology
But perhaps a repository that collects (un)publications can be considered as a library in a more traditional sense? If so, then in a rather modest sense, because a collection of just 25 publications can't be considered to be a library.

2025-12-20 10:54:42 UTC

- reply

@nprofile…rrqe This is a bug.
I've just used it to produce a wrong proof of the fact that Bool is a set, without Hedberg and without encode-decode.
```
{-# OPTIONS --safe --without-K #-}
module gist.test where
[... imports ...]
wrong-proof₀ : (x : Bool)
(p : x ＝ x)
→ p ＝ refl
wrong-proof₀ false refl = refl
wrong-proof₀ true refl = refl
wrong-proof₁ : is-set Bool
wrong-proof₁ {x} {y} p refl = wrong-proof₀ x p
```

2025-12-20 00:38:48 UTC

- reply

@nprofile…ddsj writes "less plausibly based is the totality checker"
Indeed!

2025-12-19 23:14:54 UTC

As somebody who tends to do mathematical work and publish it in mathematical venues, I think that saying that something has been "proved in Agda" or "proved in Rocq" or "proved in Lean", or what-you-have, is rather unsettling.
I get the impression that people are using supposedly formal systems to do informal (rigorous) mathematics (as always before proof assistants).
This is not bad, because I am a firm believer of informal, rigorous mathematics, but it is bad because a proof assistant can't be used as a parameter of "ultimate correctness".
Most people using a proof assistant don't have the faintest idea of what the formal rules are.
And do the designers and implementers always know that their formal rules correspond to formal systems that are both understood by logicians, **and**, more importantly, correspond to what mathematicians have in mind when they are doing their rigorous mathematics?
The idea that proof assistants give legitimacy to mathematics developed within them is uncertain to me.
I do use proof assistants and I love them as my blackboards, and I gain more confidence from them than from the people who referee my papers, but I don't think "a proof that passed the proof assistant check" is guaranteed to be a proof.
And, of course, I am **not** talking about software bugs. I am talking about what happens before any bugs take place.
And for there to be a bug, we need to know the precise specification of what we intended, which is what I think is missing here, in all proof assistants discussed above.
Yes, Rocq is based on the calculus of inductive constructions. Yes, Agda is based on MLTT. Etc. But "based" doesn't mean anything precise.

2025-12-18 19:30:02 UTC

This happened to me in the past, but I don't remember how I fixed it.
My mouse on my Mac Mini still moves but it can't click. So, in particular, I am writing from a MacBook Air, because my Mac Mini is stuck.
The solutions on the web say to restart it, which is bad enough, but I can't even do that: I can't use my mouse to click the menus to do that. I can't use my mouse to go to the terminal in front of me to do "sudo reboot". Etc.
I guess I can ssh to the Mac Mini from the MacBook Air I am using, and then do "sudo reboot".
Is there a better way?

2025-12-15 17:53:49 UTC

- reply

@nprofile…qm54 I did miss a lot of lectures when I was a student because I was in the library instead. Do you know what your students are doing when they are not attending lectures? I don't. Some of them are doing nothing. Some of them are ahead of us. We don't know which.

2025-12-15 17:21:50 UTC

- reply

@nprofile…pwph Adding to your experience, last week I bought a book online as a Christmas present. I was at home when it was delivered, but instead the deliverer decided to put it "behind the willy bin" (in their words) and when I collected it in the morning it was completely soaked because of the rain.

2025-12-15 17:16:31 UTC

- reply

@nprofile…qm54 Don't blame the students. They are just learning, like we all here did once. They are trying hard. At least some of them are.

2025-12-13 23:15:13 UTC

- reply

@nprofile…5ug2 Is it?

2025-12-13 22:07:33 UTC

I learned (as many of you also probably did) the following expression from Tom Hales, which I love:
"Conjectural conjecture".
I often have conjectural conjectures, and less often actual conjectures.

2025-12-13 19:32:45 UTC

- reply

@nprofile…mdgu writes "I've been thinking that at some point in the past while, maybe a decade or so, mailing list norms have changed, because I do think that getting off-list replies has increased"
Maybe. But in this particular case, I suspect this happened because the authors wanted to report what they are thinking about, rather than what is categorically know (which is explicitly what I asked about in the mailing list).
But let me say one more thing. People in the categories lists are getting old, and so interacting less, and the new people are using different means of communication, including, e.g., this (namely mastodon), Zulip and discord (and more). So this also makes a difference.

2025-12-13 18:10:14 UTC

- reply

I wrote "I've just written to the Categories mailing list to ask whether this is known to any (1-)topos theorist".
Nobody answered in the list, but I was contacted by André Joyal and Jérémie Marquès because it turns out they are thinking about similar things. An interesting discussion followed!
@nprofile…rrqe

2025-12-12 21:39:24 UTC

- reply

I wrote "Not all algebras of the partial-map classifier (aka lifting) monad are free."
I've just written to the Categories mailing list to ask whether this is known to any (1-)topos theorist, and, moreover, whether any example other than the one I gave above is known.
I am curious to know what the old category theorists know about this. Not that I am young - of course I am officially not young any more.
@nprofile…rrqe

2025-12-12 18:58:13 UTC

- reply

Continued rant, but also solutions asked for, regarding Microsoft crap software and infrastructure.
... And I can say more, including the fact that some of my collaborators (in universities other than mine who also sadly use Microsoft) suddenly lost all invitations when they declined *just one* invitation in an open-ended series.
(Seriously, why are companies and universities using such crap service, and paying a lot for it? End of parenthetical rant.)
In any case, does anybody know how to solve **all** the above problems?
I already waste a lot of time with email and calendar handling.
I don't want to waste even more time, as I am doing now, meta-handling the email and calendar problem.
2/2

2025-12-12 18:56:30 UTC

I hesitate to ask this here in this forum, but here we go, because google search didn't help me.
(If you want to answer, please read everything else first before answering, because there are many issues, not just one, and I want **all** of them solved, not just one - thanks. Solving just one of them doesn't work for me.)
1. The Outlook app on macOS is not working properly for me. (Don't say: "Don't use it". I have no choice.)
2. For example, yesterday I spent three hours making my calendar for next year (teaching, conferences, research collaborations, and much more). This was from my Mac at home.
3. This morning, to my surprise, and to my disappointment, when I got to my office, these calendar entries were not present in the Outlook app.
4. Even worse, people who were expecting these calendar invitations didn't get them.
5. Much, much worse, for me, is that none of the calendar work I did was reflected in the app or in the web interface.
6. "Luckily", when I got back home, all the work I did on my home Mac **was** in the Outlook calendar. So I synced manually. No effect. So I quit the Outlook app, crying that yesterday's 3hr work would be lost. But then, after a few hours, eventually everything was synced.
7. So I said to myself, I should not use the Outlook app on macOS. I should instead use the web app.
8. So I tried this. Use Outlook from Firefox. Catch. I don't get calendar or email notifications when doing this. No matter how hard I tried to search for solutions for
this on the web, the recipes didn't work,
9. A calendar app that doesn't sync among multiple devices is useless.
10. A calendar that doesn't give timely notifications is useless.
1/
(Character-limit limitation.)

2025-12-07 18:27:14 UTC

- reply

@nprofile…yw5f I just rather enjoy it. Otherwise I wouldn't be doing it.

2025-12-07 18:20:25 UTC

Is it outrageous to say that I don't care about philosophy, and I do constructive mathematics just because I like it, full stop, no other reason needs to be given?

2025-12-03 18:46:28 UTC

- reply

@nprofile…xjm9 writes "I assume the type theory course is more "what's it like to live within type theory" than the meta-theoretical aspects?"
I assume so. It is going to be delivered by Thorsten Altenkirch.
But I don't know for sure, because Thorsten has done a lot of work about the meta-theory of type theory using Agda as the meta-language.
Maybe the local organizers @nprofile…h3ed or @nprofile…kxks , and also colleagues of Thorsten's, have insider information to answer your question more definitively.

2025-12-03 17:35:40 UTC

- reply

@nprofile…cj4s We did the same in Birmingham. 😞

2025-12-02 22:57:01 UTC

The hardest thing in academic life is "context switch". And maybe in other lives here on earth, too.
With a packed week, with teaching, unavoidably admin, my own work, and my work with collaborators, not mentioning family life, not only there is little time for each of these things, but when it comes to switch to the next thing there is a significant overhead involved, trying to remember what happened last time and make progress from that.
And I didn't mention email in the above discussion, which is a killer, in many ways.
If you respond to all emails, there is literally no time to do the above.
If you don't, then you feel guilty, which impairs the normal development of the above.
Initially, email was conceived to make things more efficient.
But my practical conclusion is that email, in a workplace, makes things utterly inefficient, by enabling people to create an endless stream of tasks for everybody else, and fast.

2025-12-02 21:42:37 UTC

- reply

@nprofile…qm54 Bad.

2025-12-02 21:12:33 UTC

I highly recommend the Midlands Graduate School in the Foundations of Computing Science. And so do tell me many previous students, some of whom are now well-established academics, including LICS invited speakers.
The courses for 2026 are:
1. Type theory using Agda
2. Category theory
3. Lambda calculus and combinatory logic.
4. Effects and Call-by-Push-Value.
5. Synthetic Homotopy Theory.
6. Categorical Algebra and Logic.
7. Inductive and coindictuve Reasoning with Isabelle/HOL
(4) is to be delivered by the winner of the 2025 Alonzo Church Award, my colleague Paul Levy.
For more details, see
https://tinyurl.com/MGS-2026

2025-11-26 22:49:19 UTC

- reply

@nprofile…f34w wrote "sorry if you heard something different from what I meant"
Out of context, this can mean many things.
In particular, it can mean a misunderstanding.
So in this interpretation, "sorry" is not about apologizing, but about being polite.
But this is not what @nprofile…aqgj is talking about.
They are talking about apologies, not about the various possible uses of the word "sorry".

2025-11-26 21:05:07 UTC

- reply

@nprofile…rrqe
Speculative question. Is there a nice characterization of the type of
all algebra structures on Ω? We have two "extreme" ones, namely ∃ and ∀.
There must be plenty in between.

2025-11-26 19:59:43 UTC

- reply

One more thing, and I promise that I will stop after this.
Although I don't promise to keep the promise.
I've added the following questions to the TypeTopology file:
"
The above gives *one* example of an algebra which if it's free then excluded middle holds. There must be plenty more. For example, a product of algebras is an algebra. Is a product of free algebras also free? As a second example, the algebras form an exponential ideal. Is the algebra X → A free if the algebra A is?
"
Do you have a feeling, @nprofile…rrqe , regarding what the answers to the above question could be?
https://martinescardo.github.io/TypeTopology/Lifting.AnAlgebraWhichIsNotAlwaysFree.html
Yes, I admit, I am currently obsessed with this topic, and I want to understand the original question to the bottom of it.

2025-11-26 19:01:38 UTC

- reply

@nprofile…ywac
I haven't looked at the link, but may I ask: is its sobrification also CGWH?
In that respect, see e.g. Streicher and Gruenhage's paper "Quotients of countably based spaces are not closed under sobrification".
Luckily Thomas Streicher's web page still exists (wise university) for us to find the paper: https://www2.mathematik.tu-darmstadt.de/~streicher/

2025-11-25 21:22:01 UTC

Please be mindful of mast(h)todon replying etiquette.
When you reply to somebody, please @mention them first, then write your reply, and then afterwards mention @everybodyelse.
Here is one example: https://mathstodon.xyz/deck/@MartinEscardo/115611953893816975
The point is:
(1) Make sure everybody knows who you are replying to.
(2) Make sure everybody in the conversation gets to see your reply.
I am now in a thread I find interesting, but in which people are chaotically replying to messages, to the extent I don't even know whether they are attributing something to me or they are just keeping me in the loop.
So if you are replying to a post with @nprofile…gxzw, @y, @nprofile…mj43 in the loop, and you want to say "blah" to @y, then do
```
@y blah
@nprofile…gxzw @nprofile…mj43
```
This will make everybody, not just me, understand not only what you are talking about but also who you are addressing it to.
Just like in real-life conversations.

2025-11-25 19:15:56 UTC

- reply

@nprofile…5ug2 But is this necessarily the case?
Of course you have to be patient to structure things in the right way. I think I am patient in this respect (although I've made some structuring mistakes).
@nprofile…ddsj @nprofile…rrqe

2025-11-25 19:11:30 UTC

- reply

@nprofile…ddsj
There is an additional advantage for older people like me.
The proof assistant will tell me off when I am wrong, but the piece of paper won't.
🙂
@nprofile…rrqe

2025-11-25 19:02:19 UTC

- reply

@nprofile…rrqe I have something to say about this "early experience".
My "current experience" is that I am lazy to work on paper nowadays.
I don't know whether this is good or bad.
My old-acquired instinct, when thinking about a mathematical problem, is still to get a piece of paper to think about it. This is how I always start.
But when it gets to the point I need to do actual calculations, my newly-acquired instinct is to move to Agda, in particular TypeTopology, as a blackboard.
To repeat, I don't know whether this is good or bad, but it is how things currently work for me.

2025-11-25 10:27:03 UTC

- reply

@nprofile…0t4k @nprofile…rrqe
I would like to have refactorization tools! Is this available somewhere?

2025-11-25 10:07:26 UTC

- reply

@nprofile…rrqe Maybe. But if there was decent written documentation about the interactive mode, this wouldn't have happened. There still isn't, at least not in the Agda manual. 😞

2025-11-25 09:53:02 UTC

- reply

@nprofile…rrqe Back in 2009/2010 I didn't know that holes existed and wrote proofs for one year directly without the interactive mode - until a new PhD student (supervised by somebody else) came from Sweden and enlightened me. 🙂

2025-11-20 22:37:33 UTC

- reply

@nprofile…stct writes "the US is the laughing stock of the world"
What's sadder is that a lot of countries are copying it, to the extent that fewer and fewer people laugh about this.

2025-11-20 21:24:53 UTC

In the last few days, somebody proposed to add something to TypeTopology which was already available in other libraries, with a nice justification for adding it to TypeTopology.
Only for this person to realize that it actually wasn't in any library at all!
In any case, thanks to them, it is now in TypeTopology.
I thought this was a funny story!
Something similar was in other libraries, but not what they added!

2025-11-18 21:20:49 UTC

- reply

@nprofile…5ug2 writes "[...] (I also learned operational domain theory from you, Martin, at that same MGS.)"
Really? Nice. Which year was that? (I can probably compute this by going to the MGS website, as I believe I taught this topic only once at MGS.)

2025-11-18 20:42:15 UTC

My colleague Paul Levy gave a wonderful talk this evening for an internal celebration of his Church Award.
https://siglog.org/winner-of-the-2025-alonzo-church-award/
He gave an amazingly lucid and non-trivial, but highly understandable, talk for a general audience, including not only computer scientists. And it was entertaining, too.
Please join me congratulating him!

2025-11-18 20:35:13 UTC

- reply

@nprofile…juu5 Actually I forgot that this evening we had my colleague's Paul Levy celebration for his Church Award, and I've just got back home after a detour to pick up my son at the piano lesson etc. So another day.
But, for the moment, let me say that we started to think about computability constructively with my former student Cory Knapp
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21
Also we thought about the Kleene-Kreisel continuous functionals constructively with my former student Chuangjie Xu.
https://www.sciencedirect.com/science/article/pii/S0168007216300410
I will report back later. Perhaps I will write a thread about "constructive computability theory".
But your question is something interesting to wonder about, with non-trivial answers.

2025-11-18 10:22:46 UTC

- reply

@nprofile…juu5 Yes, there are. I will give a few this evening.

2025-11-16 20:54:34 UTC

- reply

@nprofile…rrqe I love the results, too, but the formal proofs are written using the opposite of the philosophy of TypeTopology.

2025-11-16 18:16:14 UTC

- reply

@nprofile…356e @nprofile…ral2
In my experience, when a category theorist says "x is just y", they are explaining a simple thing x in harder terms y.
There are usually two interpretations of this:
(1) You dumb person.
(2) You've come across an interesting notion or theorem. Here is how it can be viewed more generally. And you may profit from seeing it more generally.
I don't know what such people mean by "just", but we may just assume that they meant (2) and that they are socially awkward.

2025-11-16 18:10:07 UTC

- reply

@nprofile…5ug2 @nprofile…ral2 It got a bit colder today, so now is the time.

2025-11-15 17:41:39 UTC

- reply

@nprofile…rrqe writes "Writing your name is the hardest problem in CS"
The context, as I understand, is that students submit written work without their names or student id's, which make it impossible to give credit to them.
I have something to say about this. In the past I used to teach a module in which the students had to submit written work as in a piece of paper.
I had the very same problem as you report. No matter how widely we advertised that it is impossible to give credit to a paper without identification, the problem persisted.
So I had a brilliant idea: Question 1. Write your name or university id (worth 1%) .
It worked!
Nowadays we don't have this problem any more, as all submissions are electronic (on Canvas).
But we do have another new problem: "Sorry, I missed the deadline by 1 minute. Here is my submission by email."
OK, so you would think that giving them 5min grace on Canvas would solve the problem. Then they submit 6min late, and again send you an email. The solution is to have firm deadlines, with not even one minute of lateness allowed. If you have hundreds of students, as we do, getting hundreds of emails from students doesn't scale up.

2025-11-10 12:34:58 UTC

- reply

@nprofile…v38n @nprofile…kag9
I have a proof that choice implies excluded middle, similar, bbut not quite the same, here in TypeTopology:
https://martinescardo.github.io/TypeTopology/UF.Choice.html
There is also a version in my MGS'2019 lecture notes:
https://martinescardo.github.io/TypeTopology/UF.Choice.html

2025-11-08 17:43:12 UTC

In a boolean 1-topos, every algebra of the lifting (aka partial-map classifier) monad is a free algebra.
John Sterling asked whether this is the case in *all* toposes.
We show that it isn't.
For example, it fails in Johnstone's topological topos. More generally, we show that it fails in any topos in which the negation of the principle of excluded middle holds. (not (for all p, (p or not p))).
The object Ω of truth values is an algebra in (at least) two ways, with structure map ⨆ = ∃ (exists) or ⨆ = ∀ (for all).
In all toposes, the structure map ⨆ = ∃ exhibits Ω as freely generated by ⊤ : Ω.
In a boolean topos, the structure map ⨆ = ∀ exhibits Ω as freely generated by ⊥ : Ω.
Moreover, the converse is true. If the structure map ⨆ = ∀ exhibits Ω as freely generated by ⊥ : Ω, then the topos is boolean.
We may wonder whether Ω with the structure map ⨆ = ∀ is freely generated by *any* object G of generators.
We show that if this is the case, then
1. G is a subsingleton/proposition/truth value,
2. the double negation of the principle of excluded middle holds, and moreover,
3. G ≃ (principle of excluded middle).
I particularly like (3)! Isn't it funny?
A proof of the above, with a lot of further discussion, is in TypeTopology:
https://martinescardo.github.io/TypeTopology/Lifting.AnAlgebraWhichIsNotAlwaysFree.html
@nprofile…rrqe

2025-11-08 00:16:54 UTC

- reply

@nprofile…jftr
For the record, not once in what I said above did I try to justify the pay scale.
All I said is that at least one person, namely @nprofile…rrqe , gave up the marvellous US pay scale to be here with us. That's all I said.

2025-11-07 22:50:26 UTC

- reply

@nprofile…rrqe And yet here you are.
I suspect that this may be because here you are allowed to think and work on whatever *you* think is important / interesting / relevant?
Whereas is the US, even disregarding the current government, this wouldn't be possible for you?
In any case, anywhere in the world, being an academic means that your pay is the joy and freedom of learning forever, rather than your salary.
Nobody I know, in any country, is an academic for the pay they get.

2025-11-05 18:05:27 UTC

- reply

I wrote: "We haven't formalized this yet, but it is in the making."
Done. By my coauthor.

2025-11-03 20:28:07 UTC

Rhetorical questions, when written down, should not end with a question mark. They should end with a full stop. I practice this preaching.

2025-11-03 16:33:24 UTC

- reply

@nprofile…n7dy
From my perspective, funext is part of the nature of the notion of function.
Functions without funext are not functions (ha, I've just restarted an old flame war - apologies in advance).
I have no view regarding HOAS.
If you have different notions of "function", this is fine. But perhaps they shouldn't be called "functions", to avoid confusion.

2025-11-01 19:21:30 UTC

- reply

@nprofile…juu5 I am not sure what you mean.
Unique existence (in HoTT/UF, which is what I presume you are talking about) is a proposition. So it is just as specified as it is unspecified.
If you truncate a proposition you get the same thing.
Please explain more what you have in mind.

2025-11-01 18:33:27 UTC

- reply

After this, we discuss unique existence in univalent mathematics, in particular in relation to universal properties, with the example of the natural numbers being homotopy initial in the setting of ∞-groupoids (that is, arbitrary types), rather than just sets (that is, types that satisfy the uniqueness of identity principle, or 0-groupoids).
7/

2025-11-01 18:33:05 UTC

- reply

After this we discuss several equivalent notions of equivalence, including half-adjoint equivalence and Joyal equivalence, both of which are conceptually interesting and practically useful.
We then discuss how function extensionality follows from univalence, including many equivalent characterizations of function extensionality, which are again conceptually interesting and useful in practice.
Then we discuss that universes are map classifiers (the literature calls them object classifiers).
6/

2025-11-01 18:32:37 UTC

- reply

At this point, the students should be ready for exercises, and we provide *lots* of them in one section, followed by a section solving them.
We then discuss equivalent formulations of univalence, which are useful for both conceptual reasons and some practical purposes.
And then we proceed to discuss "equivalence induction", similar to "identity type induction", also known as "path induction".
Here there is also a new technical contribution in our notes, by vastly simplifying the approach to obtain equivalence induction from univalence, compared to what people had done before, which should give a more conceptual undertanding of what is going on.
5/

2025-10-31 20:38:58 UTC

In our Advanced Functional Programming module, we secretly teach students dependent type theory and even univalent foundations, without the students knowing we are doing this. Or the people who allow us to teach this module. 🙂
In any case, this has been rather successful in practice with most students, and with some of them choosing to do MSci (or even BSc!) dissertations based on this.

2025-10-31 16:44:17 UTC

- reply

@nprofile…f34w It is not something I am personally involved with. Just watching people battle against each other, sometimes using their authority.

2025-10-30 20:57:28 UTC

All sciences have their internal battles, including mathematics.
And this is healthy, unavoidable, but tiresome, too.
But in Computer Science, people seem to be much more prone to battles, including public battles.
And this manifests itself in damaging ways, in grant applications, in conference paper submissions, in journal paper submissions, and much more.
Could we please stop shooting ourselves in our own foots?