@jonmsterling This could be a good MSc student project, and I have some hints to give to them.

@jonmsterling Here is me breaking the promise (which is fine, because I explicitly didn't promise to keep the promise).

I wrote "I've added the following questions to the TypeTopology file".

In fact, after thinking a little but about this this evening, I am pretty sure that, in general, free […]

@jonmsterling

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.

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

@jonmsterling I ended up proving a stronger result:

Every lifting algebra is free if and only if the topos is boolean.

This also has a simpler proof, which in particular doesn't use Higgs Involution Theorem […]

It is perhaps worth discussing why we are discussing this.

Jon wanted to justify, in his arxiv paper, why something he did was more complicated than perhaps other people would expect.

He justified this with a cautious conjecture.

One can never be sure, in mathematics, until things are proved […]

@jonmsterling I wrote "3. G ≃ (principle of excluded middle).

[...]

I particularly like (3)! Isn't it funny?"

The fact that G ≃ (principle of excluded middle) isn't surprising after all.

Anders Kock proved, as you mention in your paper, that if a lifting algebra is free, then it is freely […]

@dpiponi I don't think the UK is the worst in this respect. Think of e.g. Italy, but also other European countries.

@dpiponi 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.

@skewray writes "My wife just purchased an iPhone 17. When she is in the house and I am listening to music with my desktop and headphones, I can hear her iPhone microphone in the right headphone channel"

Funnily enough, something very similar happened to me two days ago.

I connected my […]

Actually, (iii) was an oversight.

@de_Jong_Tom Developed this in TypeTopology:

https://cs.bham.ac.uk/~mhe/TypeTopology/DomainTheory.Lifting.LiftingDcpo.html

So in principle we just need to put things together.

@jonmsterling

@jonmsterling

By the way, there is also a question, labelled by the prefix "TODO", which I find very interesting and for which I would like to know an answer.

I hesitate to call this a conjecture, because I am in two minds.

At some point I thought I could prove that my results are tight.

But […]

@andrejbauer writes "If anyone knows of (non-trivial) examples of Lawvere's fixed point theorem, I'd be interested to know about them."

I have quite a few here:
https://martinescardo.github.io/TypeTopology/Various.LawvereFPT.html

@highergeometer @jameshanson

@andrejbauer Something similar to this?

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

Even later:

"Loosely speaking, a mapping from one set, S, into another, T, is a "rule" (whatever that may mean) that associates with each element in S a unique element t in T."

This is followed by a formal definition in set theory as a set of pairs, only to be followed by

"This definition […]