Hey types dot users!
I've been working on solutions to the HoTT book with @vdash and @ionchy for a few months now on a shared overleaf. I know there might be a few other people interested here, so I'm making it public. The view link is in my profile, and if you want an edit link too shoot me a DM and I'll give you one (and if this becomes more popular, I might share it publicly too).
We're only to chapter 6 but I'm confident we can get through the book together!
Oh, it seems that search only returns my own posts. I think that this makes it kinda difficult to find discussions to join, although I guess there are technical challenges for it, it would require storing all posts from all servers or something. I wonder if there is any way to make federated search work.
Delete Chrome. Now.
Google is using its exceptionally powerful position to make *the browser itself* analyze your browsing behavior and serve that on a plate in the form of "cohorts" to anyone interested.
They are transforming Chrome into a "browsing-history-passport" - right now.
If you care about your intellectual freedom even a little bit, you must put Chrome out of your life as soon as possible. Support others doing the same.
non type related, gender reveal parties
For the longest time I thought that gender reveal parties were about trans people coming out and revealing their gender (while trying to cause as many causalities as possible). I was extremely disappointed when I realized that it was about revealing the assigned at birth gender of fetuses.
I am interested in PL/Type theory, especially dependent types and constructive logic.
I am new to mastodon and I do not use it often.
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.