Replying to
@jer_gib@functional.cafe i remember reading the blog, it is totally awesome
looking forward to the book
Remote
Dan Frumin
@dif@mathstodon.xyz
mastodon 4.7.2logic-adjacent ~ groningen
i post about logic, arts, and culture
66 Followers
85 Following
35 Posts
Joined September 11, 2025
pronouns:
he/him
Here is an ``interesting'' question I have in type theory, and it has to do with Leibniz equality.
In type theory, we can formalize a version of Leibniz equality principle on sets as a type
```
Leq(A, a, b) ≡ ∏ (P : A → hProp), P a = P b
```
where `A : hSet`. I.e. two things are equal if no proposition can distinguish them. Thus we 'explain' equality in an hSet in terms of hProp-predicates.
In case `A : hSet`, the defined Leibniz equality coincides with the usual equality. Since both types in this case are propositions, it is easy to show the logical bi-implication.
What I am interested in is if this generalizes to higher type? Suppose `A : n-Type`, and we define
```
Leq_n(A, a, b) ≡ ∏ (P : A → (n-1)-Type), P a = P b
```
what can we say in relation to the actual equality? We can still have a logical bi-implication, but I am not sure if the types are going to be isomorphic. Can anyone (dis)prove me?
Replying to
@hcschuetz@mastodon.social @johncarlosbaez@mathstodon.xyz I am also not a native English speaker, but I read the article and the second point was made somewhat implicitly: he says that Turing test was a test for consciousness (but not anymore). This is debatable position in philosophy of mind.
As for the first point about Claude being conscious, I think he cleverly avoids it altogether, and coaxes it in his typical humor: "Could a being capable of perpetrating such a thought really be unconscious?"
In fact, I found the whole article very funny, but it is clear that Dawkins is not a philosopher of mind (just like most of the people talking about AI)
pet in de hand
fiets aan de kant
wij staan stil in dit land
One of my favourite harpists is the brilliant Lavinia Meijer. And she is out with a new album, full of her own arrangements
Please check it out if you like baroque music or just harp music:
- https://open.spotify.com/album/6t5pw5WCiQlpmo0aIkejXk
- https://classical.music.apple.com/us/album/1860263402
Replying to
@de_Jong_Tom@mathstodon.xyz @nmvdw@mathstodon.xyz that's okay, i will just read the slides and play your voice in my head
Does anyone remember [Darcs](https://darcs.net/)? It was genuinely a nice interesting system, but seems completely dead now
Since there are a lot of type theory folks here, maybe someone can help me out
Does anyone know a good overview/reference of how to make gradual typing (somewhat) sound without destroying performance?
Replying to
@rysiek@mstdn.social you are so right, the joke ig nobles conference is definitely more serious than NeurIPS. that is totally true and makes sense
Replying to
@moses_izumi@fe.disroot.org @0xabad1dea@infosec.exchange @nina_kali_nina@tech.lgbt it's literally the name of the thing
Salman Rushdie on Voltaire's Candide: spotting a fresh eye patch, it looks like they are going to make the whole series
https://www.youtube.com/watch?v=wgk5gXEEV9U
How to make a better pen/pencil clip by using springs
Why doesn't this exist everywhere?
Replying to
@de_Jong_Tom@mathstodon.xyz @nmvdw@mathstodon.xyz is there a recording, sir? i missed the live stream
Replying to
@beep@follow.ethanmarcotte.com I think I can meaningfully separate my everyday usage of "Deepseek" from the "machine of death and war"
Niels W Gade: Violin Concerto in D minor, Op. 56 (the "W" stands for "Winner"): https://www.youtube.com/watch?v=lecOb2MKYl8
Danish music is extremely underrated.
Replying to
@fl yeah curious to see what the results are, but if all they need to do is use word processing and web apps, then it shouldn't be a terrible transition
it's not like windows is an easy to use system
The dreams are coming true: France is ushering a new age of Linux. Could 2027 finally be the year of Linux on Desktop? (probably not)
https://www.zdnet.com/article/france-leaves-windows-for-linux-desktop/
Replying to on dice.camp
@StefanEJones@dice.camp Love the comic, will you share the prompt that you used?
Replying to
@emilymbender@dair-community.social @alex@dair-community.social have you guys tried the latest Claude model for programming and auto-formalization? it is pretty cool
An interesting survey from the Kyiv International Institute of Sociology on the attitude of Ukrainian people towards different ethnicities and nationalities.
The respondents were asked to rate different ethnicities on the scale from 1 to 10, where 1 means "I'd treat them like my family" and 7 means "I'd not allow them to enter the country"
In a true Eastern European fashion, no group has managed to get an average score below 2 (which means "I'd treat them as closed friends"). The results are in the screenshot, and the rows are as follows, from the most friendly to the least friendly: Ukrainian-speaking Ukrainians, Russian-speaking Ukrainians, Jewish citizens of Ukraine, Canadians, Germans, Poles, French, Americans, Belorussian citizens of Ukraine, Romanians, Russian citizens of Ukraine, Africans, Roma, Belorussians, and, in the very end Ukrainian and Russian citizens of Russia
Compared to a similar study in 2022, Americans fell down the list for the obvious reasons, and all the bickering with Poland is probably responsible for the Poles scoring this low
source: https://www.kiis.com.ua/?lang=ukr&cat=reports&id=1603&page=1
Replying to
Maxim Vengerov plays Tchaikovsky's Violin Concerto with Tokyo Philharmonic, 1993: https://www.youtube.com/watch?v=Ydg64SXfOJI
This guy should have more subscribers on his channel!
Maxim Vengerov plays Tchaikovsky Violin Concerto (1993)
Replying to
@johncarlosbaez@mathstodon.xyz @ClimateJenny@biodiversity.social Glad that I am safe from this curse, since I am not a Noble prize winner
Replying to
@andrejbauer there used to be a time on the internet, where having a well-designed and well-maintained website was at least a signal of serious intent. now it is so easy and quick to make a web 2.0 flashy website that it has an opposite effect to me
Replying to
@johncarlosbaez@mathstodon.xyz @ClimateJenny@biodiversity.social what can i say, the guy has his way with words
Does anyone have experience with self-hosted Git? I am currently using Gitea but it updates so fast (including security fixes) that I cannot keep up with it..
I am considering going back to just using cgit (which is annoying to configure). Does anyone have any pointers?