@dougmerritt I've got « and » as Option-\ and Option-Shift-« already (this is ABC -extended). They're the standard Slovenian quotes.
At any rate, it's easy to customize the file, just edit it (and make sure you save it in UTF-8).
I have improved the LaTeX input method for MacOS for typing ℂ𝒪𝕆λ Mαth symbols. MacOS is incredibly finicky about installing it. I wrote up instructions for Sequoia 15.7.4. If anyone tries it, especially on a different version of MacOS, please let me know how it went (here or via an issue) so […]
I am a legendary influencer, second level! https://gitranks.com/profile/andrejbauer
@aspiwack.bsky.social It looks like the bridge with Bluesky is working. Amazing, it's almost like the 1990's internet is back.
@aspiwack.bsky.social What are you referring to? Is there a reference I can look up?
With apologies for the delay, the recordings of the talks at the Types and Topology Workshop in celebration of @MartinEscardo's 60th birthday (https://tdejong.com/mhe60) are now on YouTube (where available) 📺
https://www.youtube.com/@mhe60/videos (also linked from the workshop webpage)
Many […]
@MartinEscardo I have come to a somewhat bleaker realization. In oral exams, the students find it hard to repeat upon request the last sentence they uttered.
I warn them this is something I do in oral exams. I tell them I am going to do this, and that I'll do it both when what they said was […]
@MartinEscardo It's -10°C and 30cm of snow here and nobody even for a moment thought of closing schools. How much snow do you have?
@MartinEscardo I was hoping you'd say "modalities" 🙂
@MartinEscardo How would you quantify the amount of information or constructivity?
As a suitable goal, you should get it down to 42 seconds.
@MartinEscardo Have a student generate a little executable that outputs the dependency graph. Then you can do it for real with a work-stealing queue.
@de_Jong_Tom Make the best of it: "I am sorry but I don't know what email you're talking about. My university disposes of email after 90 days to preserve disk space."
@highergeometer Yeah, this kind of trickery usually doesn't work so well constructively because one needs complements or set difference somewhere, and those won't work as expected constructively.
Kuratowski-finiteness (the initial ∨-semilattice) works well in many cases, but as is usual for […]
@highergeometer Which definition is that? What construction are you referring to?
P. S. The finite subset of S form the initial ∨-semilattice generated by S.
I said too much, both in terms of content and length.
https://www.typetheoryforall.com/episodes/constructivism-and-computational-content
@dpiponi In my circles people know the difference thanks do Donald Knuth.
A plant with lots of roots growing on top of a bar of soap.
@soaproot @MartinEscardo Here is your new profile picture, courtesy of AI.
Before you plug in your new Timex/Sinclair 1000, please take a moment to think about this exciting new adventure. We want to assure you that:
1. You will enjoy computing.
2. You will find it easy as well as enjoyable.
3. You shouldn’t be afraid of the […]
[Original post on mathstodon.xyz]
A new generation has arrived. The other day a freshmen showed me a 10k lines of code in a single file, written by him and an LLM in a week. It uses machine learning to find small boolean formulas that match a given truth table. A freshman. 10000 lines of code in main.py. It works. Oh yeah, and […]
How long does it take to get used to MacOS Tahoe's ugly design? Right now I am rather unhappy.
@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 […]
RE: 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 […]
@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.
