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
Wholesome YuiAzu wedding doujin: https://dynasty-scans.com/chapters/yui_and_azusas_love_song
(Content warning that there are inappropriate doujins on the site. This one is totally appropriate, though.)
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? 🤔