Pinned toot

Remember: TheAspiringHacker is no longer the username of my GitHub and GitLab accounts!

Pinned toot

As a corollary, if I ever toot anything political, please don't assume that the people whom I follow or who follow me agree with me.

Pinned toot

Disclaimer: In case it isn’t obvious, I do not necessarily share political beliefs with the people whom I follow or boost.

"Point-free" comes from topology, where one does math without mentioning the points of spaces. Did the idea that types are spaces and their inhabitants points exist before HoTT?

If I have:

q : a = b
r : c = d
s : a = c
t : b = d

Can I inhabit q = r?

Nope, I'm still not done with the proof. I don't think I can make a square...? Cubical Agda is so confusing.

I"m almost done with my Agda proof. I just need to figure out how to make a square...

When using Agda, when I create helper functions, do I just call them "lemma," 'lemma2," etc? Those aren't descriptive names, but the real meaning is in the types.

This is so ANNOYING! The propositional equality defined in Agda's standard library is DIFFERENT from the one in the cubical library! And, when the cubical library reproved everything, it swapped the left and right sides in the definition of associativity! Argh!

TAH boosted
TAH boosted
TAH boosted

Arend is a new programming language by JetBrains that supports Cubical Type Theory!

@hydraz @mdallastella Okay, I went to @epicmorphism's instance and saw the Keionbot, but when I went to its instance, I got an error. I think that the instance shut down?

@hydraz I remember that you followed the K-On bot and it followed you back. Do you know what happened?


Nooo! All my boosts of the K-On bot are gone! 😭

Show more
Functional Café is an instance for people interested in functional programming and languages.