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.

TAH boosted
Tengen Toppa Gurren Lagann opening is 👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌

https://www.youtube.com/watch?v=5EXFilTUiko
TAH boosted

Who is best girl in ? (I can only have up to four options, so I only put the four original girls. I don't mean to imply that Azusa is the worst.)

According to , types form a groupoid because of the equality type.

Isn't this just an extension of the idea that preorders give rise to a category? Transitivity is composition and reflexivity is identity. An equivalence relation is a preorder with symmetry, where symmetry is the invertibility of the morphisms of a groupoid.

K-ON!, romance Show more

Even though 's standard library's latest release is 1.0, github.com/agda/package-index hasn't been updated. Do people actually use the package manager?

Lesson learned not to post when sleepy... I posted a code example on HN and gave a function a name that didn't make sense. Now, I can't edit my comment.

(I wrote a random function to demonstrate something and called it "add" even though it wasn't about addition.)

2.6.0 and the standard library version 1.0 was released today!

People generally say "Vector space over a field," but since I only need addition and multiplication to do dot product and matrix multiplication, I should just use a commutative semiring, right?

TAH boosted
TAH boosted
TAH boosted

Yay, I implemented type-safe matrix multiplication in !

Yay, I finally finished my proof! The code is really messy, though...

Show more
Functional Café

functional.cafe is an instance for people interested in functional programming and languages.