@highergeometer @jameshanson I am not sure what you're after. A proof of Lawvere's theorem in a very weak system, or a type theory that possess non-trival instance of Lawvere's theorem?

@highergeometer Lawvere's fixed point theorem is a favorite of mine. Did you know Lawvere in his original paper did not present any non-trivial examples of it? He used it in the contra-positive form only "If f : B → B has no fixed points then e : A → B^A is not a surjection".

When I looked for […]

@MartinEscardo Yes, but with less Agda.

@MartinEscardo I teach mappings by first saying that they are "rules", i.e., λ-abstractions, except we write them using x ↦ ...

A bit later, when we discuss definitions, I explain definite descriptions "the unique x ∈ A such that φ(x)", written using Russell's notation ι(x ∈ A). φ(x). Still a […]

@highergeometer We have a slightly better measure, namely a graph of all the entries in mathlib, with edges the references between them.

@pschwahn @highergeometer Wikipedia links U₁(1) to U(1), so I guess they're the same thing.

@highergeometer Why did they have to call it "electromagnetism" when all the time it was just a connection on a U₁(1) bundle?

I've updated the accounting page on our wiki with actual numbers about where money is and where it's going: https://wiki.mathstodon.xyz/finance

@MartinEscardo
> To give a trivial example, if you hover over link in Firefox, you see its url, and this is not available in Safari.

Use "View → Hide/Show status bar" to enable Status bar, then when you hover on a link the URL appears at the bottom.

[Spoilers!]

@highergeometer Let C = {-1,0,1}^ℕ be the ternary Cantor space and D = {-1, 0, 1} the Davey space. Define f : C → D by

f(α) := if ∃ n . f α = 0 then 0 else (limsup_n α(n)).

In words; if α contains a 0 then f(α) = 0, otherwise if α attains 1 infinitely often then f(α) = 1 […]

@highergeometer Who first detached received meaning from concepts such as number, bigness, and quantity? Who was the first formalist?

It wasn't Euclid, for he defines a point is that which has no parts. (Is that an irreducible closed set?)

It wasn't Russell, although he came close to it […]

@dougmerritt @MartinEscardo Actually, nonstandard analysis is not what physicists need. They use nilpotent infinitesimals, which are not available in nonstandard analysis.

It is the synthetic differential geometry, as developed by Dobus, Kock, Lawvere and others, that does the job.

@MartinEscardo I would venture to say that mathematicians naturally do make the distinction, but the intuition is defeated by formal education, when they're told that "existence is ∃". The problem isn't even what ∃ is – but simply that they're taught *only one* notion of formal existence.

P.S […]

@MartinEscardo I prefer to call (2) "abstract eistence".

In practice, mathematicans operate with the distinction between concrete and abstract existence, but they're never thought the distinction formally because they're told first-order logic is The One True Way.

This situation is akin to […]

@MartinEscardo I am happy to see that Cécilia Pradic (whose obviously reads these posts but I cannot find the username) has put some real thought into questions about the Myhill Isomorphism theorem and its genralizations: https://arxiv.org/abs/2507.05028

The verdict: it doesn't generalize much […]