Notices by Martin Escardo (martinescardo@mathstodon.xyz)

I've already got rid, for some years, of

* Twitter (when it was Twitter)
* Facebook (although only recently I deleted the account).
* WhatsApp (account still to be deleted, I use Signal instead, with my immediate family, and even with my old parents).
* Dropbox (I use pCloud instead).

I still need to get rid of Google and Amazon. The latter is quite easy. The former less so, because I have an Android phone and I don't want an iPhone either. And many accounts linked to google.

Oh, and there is github too.

How can I get rid of all American tech in my life, personal and academic?

I feel like a voluntary slave of tech companies.

@julesh My final year UG project was a type system for Prolog. At that time, in the late 1980's, I didn't know about dependent types.

The world was much better, or at least less worse, when the internet didn't exist. I lived to witness this.

@julesh And who is going to maintain the code for 10-20 years in that case? The category theorists?

I joined the categories mailing list 30+ years ago. At some point it was very active. It isn't any more. But it still exists and still runs, and somebody maintains the archives (and I have all emails from then on in a private folder).

@johncarlosbaez writes

"(I would like to talk about even more advanced stuff, but there's little audience for that here.)"

Or almost anywhere?

Of course, there are specialized communication forums for that. But what I like here is that we can reach more people than in the specialized forums.

The ultimate specialized forum is a long 1-1 email thread with somebody you can relate to researchwise.

I like all levels of (non-)specialization for communication, discussion and dissemination. Including this one.

@johncarlosbaez

Try to get the Bluesky people here. Perhaps by pointing to interesting threads by yourself and by other people.

I, for myself, am not going to join anything run/funded by billionaires, even if they have genuinely good intentions (in their own wishful inner thoughts).

So, in particular, there is no way I will join Bluesky. I was vaccinated first as a late joiner to Facebook and then as a very late joiner to Twitter (two years before it became X). I am not in any of them any longer.

It's not that I am politically against Bluesky. It is simply that I completely lost any motivation to join anything like that.

And I forgot to mention the defunct Google+ in the above discussion.

I simply don't want to invest any amount of energy joining anything that will either fail on its own or that else I will like to leave when it becomes "successful".

We'd better learn how to make things work here.

And notice that part of the reason things "don't work here" (as you would like) is that everybody is disappointed with how things went in all the other (research) social media they were part of since the early 1990's.

@johncarlosbaez says

"I'm extremely happy with the Category Theory Community Server."

Sure. I am also happy with other Zulip servers, and other Discord servers.

I am just waiting for Zulip and Discord to go the same downfall.

Actually, one of the Discord servers I am in was formerly a Slack server. But then we were told we would have to pay if we wanted to preserve our posts for more than three months. And then we left.

Negative axioms can be postulated without loss of canonicity.

In this thread I want to explain a 3-page research note Coquand, Danielsson, Norell, Xu and myself wrote with the above title, back in 2013 with revisions and additions in 2017:

http://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf

There are many reasons people may (or may not) be interested in constructive mathematics.

* One is philosophical. For me, it is hard to agree (or even disagree) with the philosophical justifications, but this thread is not about this.

* Another one is that mathematical objects of interest, such as toposes, are intrinsically intuitionistic in nature, even when they are developed in a classical meta-theory. It is this that I find very persuasive, and this is a purely mathematical view independent of philosophical considerations, but this thread is not about this either.

* Yet another one, related to the first, but founded on a firm mathematical basis instead, is that "constructive proofs compute". I also find this persuasive.

I usually write things here based on the second bullet point, but this thread is about the third one.

1/

Martin-Löf type theory (MLTT) is a minimal foundation for mathematics, which is at the same time a programming language.

(E.g. Agda is based on MLTT.)

Compared to classical (non-constructive) mathematics, it lacks the principle of excluded middle.

Compared to Brouwer's intuitionism, it lacks continuity and bar-induction principles.

Compared to (the internal language of) topos theory, it lacks impredicativity and has a different treatment of the existential quantifier.

Compared to Homotopy Type Theory (HoTT), it lacks the univalence axiom and higher-inductive types.

The above mathematical theories can be accommodated in MLTT by simply postulating the required "missing" axioms (excluded middle, choice, propositional resizing, propositional truncations, univalence etc.)

2/

@highergeometer

Call it x, and then it is compressed to one character.

So I tried to be open-minded, as always, and had some goes at ChatGPT in the last few months.

To find something I wanted to buy. To write a Haskell program. To write an Agda proof. To have my VPN ignore ssh connections in MacOS. To write a recommendation letter. To improve my prose. And much more.

All I managed to achieve was to waste time.

There wasn't a single thing that made me think "Oh, yeah, this is great! I am adopting it."

But, who knows. Maybe there are some kinds of jobs that ChatGPT can do better than people. I am sorry for those people, if they exist.

Before two years ago, I used to commute to work by car.

Some days I did go by bicycle, but very few days, because there is a steep 0.7 mile hill to get back home. The 3.3 miles along the canal were fine. Each day is 8 miles in total.

Then two years ago, I decided to get an e-bike. I got it with the UK's Cycle to Work scheme that allows you to make tax deductions via so-called Salary Sacrifice, so that I paid about 60% of the price.

I was wondering, given my previous track record of using a bike to commute, whether I would really use it, or I was just making a toy purchase.

Well, it turned out that I commuted by bike every day since then, and, the few times (like 5) that I had to go by car or public transport for one reason or another, I found this very painful and time consuming.

By car or public transport it takes between 40 and 60 minutes at peak time, but by bike it takes 20 minutes, and often less.

So far I have done 3480 miles by e-bike in two years, which amounts to 5600km, mainly by just commuting to work.

Not only does this take less time, but it is much more pleasant to ride 2 x 3.3 miles every day along the canal, seeing only nature, than face roads and cars and buses, with everybody angry with each other.

(And also not paying for fuel or parking paid for the e-bike in less than a year.)

We have reached a point where more money is spent to "educate" (or "train") machines than to educate kids.

Of course, the mastodon veterans are explaining this again and again (and I am propagating this here), but this is not enough.

I am not sure using the same symbol for "boost" (here) and "retweet" (elsewhere) helps. We should not use the same symbol with different meanings.

We know this here as mathematicians.