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 […]

How much of what we do in "theory" is fashion, among academics, and how much of it will survive the test of time?

Of course we can't tell. - the test of time involves fashion, too.

Any volunteer to formalize the following in TypeTopology?

In the file linked below [1], I show, in Agda (together with lots of discussions in mathematical vernacular), that there is an algebra of the lifting (aka partial-map classifier) monad that is not always free.

This is for the lifting […]

If you want to just use the *theorems* of a paper, you don't need to read it very carefully, assuming that you trust the proofs based on third-party assessment.

But if you want to use the *ideas* of the paper, instead, then you do.

I am reading a paper whose author I deeply respect, but whose proofs are written in a confused way, aiming for economy of exposition rather than clarity and motivation.

There is no mistake in the paper, but it is so hard to decipher things that would be much easier with a clearer exposition […]

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 […]

I love this in the preface to the 2nd edition of a successful book:

"One could accuse me of overkill at this point, probably rightfully so. The fact of the matter is that Sylow's theorem is important, that each proof illustrates a different aspect of group theory and, above all, that I love […]

The amount of heavy and constant rain is unbelievable today, since 6:30am when I woke up until 9pm now, still going on.

People here have been discussing exact real number computation recently.

Here are the lecture notes for a talk I gave at Fun in the Afternoon in 2011, with Haskell code computing arithmetic operations, trigonometric functions, definite integrals and more […]

RE: odon.xyz/@egbertrijke/115528036589916180" class="hover:underline text-blue-600 dark:text-sky-400 no-card-link" target="_blank" rel="noopener" data-link="bsky">https://mathstodon.xyz/@egbertrijke/115528036589916180

Congratulations to @egbertrijke on the publication of his textbook on homotopy type theory and univalent mathematics!

For many of us classically trained mathematicians, learning univalent mathematics and type theory meant adapting to […]

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 […]

Perhaps funny story. Today I met with one of my collaborators regarding a paper we are writing, where all but two theorems are formalized in TypeTopology.

We discussed how to formalize one of them.

In the end, we concluded that the opposite of what the alleged theorem says is true. 🙂

The […]

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

I've used `bash` forever (first on Linux and then on MacOS).

I've also used symbolic links forever.

But never did I realize, until yesterday, Friday, that if you do

$ cd <some directory which is a symlink>

$ ls ..

then you don't get a listing of the files from the directory you started from […]

As some of you know, from time to time I write expository threads here and elsewhere.

An index to all (?) of them is here:

https://martinescardo.github.io/blog.html

In this thread, I'd like to (re)advertise my MGS'2019 lecture notes "Introduction to Univalent Foundations of Mathematics with Agda"

https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents

In the lengthy Introduction, I explain how univalent foundations differ […]

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 […]

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 […]

I have been postponing, for about three months, to try to prove something "I know is true"s, either on paper or in Agda in TypeTopology.

Or, rather, my schedule is against me.

I have recorded 5 starting points on paper (or actually on my tablet in handwritten notes) where I start thinking […]

Peter Freyd said that "Perhaps the purpose of categorical algebra is to show that which is trivial is trivially trivial".

In my experience, however, mathematics is non-trivially trivial.

Including category theory and everything else.

Progress. Less is more.

I meet with Paulo Oliva weekly, online (and very occasionally in person) to work on game theory and more generally the selection monad, since 2007 (Skype, Google meet, Zoom, or whatever is available when we meet).

Today's meeting (without a plan in advance) amounted to […]

First year student: I don't understand this notation (there is a lot of information I have to reconstruct by myself, and I don't know where to start with).

Later years' student using a proof assistant: Damn, the notation requires me to write down so much obvious information.

It is good to rediscover things. I keep rediscovering things all the time. This doesn't disappoint me. It rather tells me I am on the right track.

Today we had an internet outage at home and I ended up in a chat to try to get this sorted. I was sure that this was not a chatbox when (1) I was first put in a queue, and then, more convincingly, (2) one of the answers had a typo.

A lot of students who do genuine work of their own are using AI to "improve" their writing. Particularly, but not only, students whose first language is not the same language as that of their host institution.

The downside is that people will immediately see that this is AI written, and will […]