"Healthy people cost less.
Educated people contribute more.
Housed people are more stable.

...in a healthy society there are no "undeserving".
There are just people."

Since we're on the subject, I'm curious if there's a resource that explains the practical difference between using the Bishop style (equivalence with Fin) and the Kuratowski style (list/tree quotient) for finite sets. Donnacha Kidney covers this topic in his master's thesis, but his approach is somewhat one-sided—he reduces the Kuratowski style to the Bishop style. For decidable types, the two approaches seem to be completely equivalent.

I’m trying to figure out the best way to define FinInj and FinSur, as well as how to build a metatheory on top of them for things that Simpson's framework relates to, such as the Schanuel topos and nominal algorithms. I suspect Bishop is more convenient for some things and Kuratowski for others.

Today, during an IEEE standards meeting, one of the participants had to stop participating and then run to a bomb shelter because of an undeclared war against Iran.

This is obscenely bad. I'd just like to make that clear. People like me are focusing on creating wonderful technical communications solutions, all open source, and participating everywhere we can.

This horrific damage is all because of the United States government.

As a resident of the State of California, I am so sorry.

In 2013 Aaron Swartz committed suicide for facing 35 years in prison for mass downloading scientific articles.

13 years later, Meta is almost getting away with an infraction orders of magnitude larger.

The law didn't change.

https://torrentfreak.com/uploading-pirated-books-via-bittorrent-qualifies-as-fair-use-meta/

If a Klein bottle could wear pants, would it be like this or like this?

#mathstodon #math #maths #shitpost