Pinned toot

Pinned toot

Tengen Toppa Gurren Lagann opening is 👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌👌

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

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

RT @JarrettB@twitter.com

real type theory hours who up

Who is best girl in #K_ON? (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 #HoTT, 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.

https://github.com/ocaml-ppx/ppx_deriving_yojson/blob/cadb5f653d4c2a94bc9e601c02dac75698cd5b97/src/ppx_deriving_yojson.cppo.ml#L131 Anime reference in ppx_deriving_yojson???

K-ON!, romance Show more

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

My new blog post: https://theaspiringhacker.gitlab.io/posts/agda-matrix.lagda.html

#Agda 2.6.0 and the standard library version 1.0 was released today!

Yay, I implemented type-safe matrix multiplication in #Agda!

Please criticize my proof code: https://gist.github.com/TheAspiringHacker/1e15b0edd3a1f302ab8fbc4021505731

I might be wrong here, but are the definitions of left and right congruences swapped? 🤔

Joined Jul 2018