I am delighted to announce that my colleagues Paul Blain Levy and Anupam Das have both been promoted to full professor. Well done and well deserved!

1/ I call a type X *totally separated* if whenever p(x)=p(y) for all p:X → 𝟚, then x=y, where 𝟚 is the type with two points 0 and 1. (This corresponds to a notion in topology with the same name, which I won't discuss here.)

This is a "boolean Leibniz principle". Two things that satisfy the same boolean-valued properties are equal. (This arises in my investigation of compact/searchable types, which I won't discuss here.)

I will work in HoTT/UF in this discussion (without using univalence, but using propositional truncation implicitly).

Any type X has a totally separated reflection, namely the image of the evaluation map X → ((X → 𝟚) → 𝟚). (It is the definition of image that requires propositional truncation to be available.)

One question I had is what is the totally separated reflection of Ω, the type of propositions (types with at most one element) more explicitly/concretely.

This same question was asked to me by a participant of MFPS'2026 (or was it 7WFTop?).

So here is an answer for you (I don't remember who you were, but thanks for the question) in the next post of this thread.

On Monday at MFPS I gave a talk "An inductive-recursive universe of searchable ordinals", which I am very proud of.

https://martinescardo.github.io/.talks/mfps2026.pdf

This is still unpublished, I guess because I am unable to break the umbilical cord and I want to know more about it.

In any case, I am quite proud of this work, as I said.

Which is also available at TypeTopology.

I invite you to look at it.

When I was young, I learned, and was taught, how to make the computer to work efficiently and correctly, in my computer science degree.

Now it is the opposite. Do brute-force search using giant farms of computers, using a huge amount of energy and water, and get results that are not guaranteed to be correct any more.

And I was discussing with a colleague this morning that my 2001 laptop ran faster than my current top-range computer for everyday tasks. Of course, it had a much worse CPU and much less ram. And of course the software for things we still do *now* was much faster *then*.

I still have that laptop from that time running Ubuntu 4.10 from 2004 in my personal museum of computers. You would be amazed how responsive the system is for everything we do every day with a computer. I recently tested it with my son, because he was curious to see how things were then.

So we are using more powerful hardware for getting a poorer experience.

The new computers are much better for some things, such as running Agda. But, for everything else I happen to do, they were just as fast, because people programmed them in a more efficient way (they had to - there was no other way).

The Google search AI just gave me a mathematical claim which I believe is wrong, and it attributes it to me!

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.

I'll be spending a few days in the other side of the Atlantic Ocean, where "other" refers to my usual coordinate system, and where, luckily, it is not in the untolerable side.