Amélia Liao @amy@types.pl
Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).
I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️
Joined Jan 2022
Pinned toot
Every boolean in the Agda codebase can actually be one of True, False, or An internal error has occurred. Please report this as a bug.
herculean, heroic, other h-adjectives that mean of daunting size and commanding respect for having been undertaken
after yesterday's scare i'm back on the grind. today: getting the annotated printing PR mergeable and merging @totbwf's herculean rewrite of everything co/limit for the 1lab
We're going home now that she's been doing better for a couple hours
doctor seems to think it's just dietary which is gonna be really "funny" when her bp is 21 over 16 again
I'm doing some anxiety scrolling and wow. [gestures at everything], huh?
Had to accompany my mum to the hospital so pretty-printing can take the L on this one
(She's stable)
Not gonna look at my github notifs on Sunday
Amélia Liao
boosted
CVE-2023-21036 / acropalypse is absolutely bonkers.
Apparently for 5+ years the cropping / editing tools for screenshots on Google Pixel phones was only overwriting the start of the screenshot PNG file, but not truncating.
All screenshots shared for the past 5+ years might have data recoverable from them. Demo available at https://acropalypse.app/
Google still hasn't communicated anything on this.
(h/t ItsSimonTime on Musk's site)
Agda developer me and Agda user me are sometimes at odds in funny ways
Agda developer me: Not using the provided built-in modules is unsupported
Agda user me: [doesn't use those, code breaks literally every other commit]
Why do I do this to myself?
i even did a thing yesterday! a minor refactor, but a thing nonetheless!
two(?) days in a row now i slept through the entire day and woke up in the morning!
Based path induction is such a funny term to me, now. If you point it out it's implicitly a compliment, like "hey, based path induction! 😎"
Amélia Liao
boosted
Category theory is sometimes taught to computer scientists in a way that makes the most simplifying aspects of category theoretic thinking look like they are making things much harder. An example is the idea of "preserving XX up to isomorphism".
Taking products for example, we are often a bit sloppy about the difference between products as a chosen structure and as a property. Part of the reason for this sloppiness is that conventional mathematical foundations do a bit of violence to the view of products-as-property, so we need to switch between the viewpoints more often than we would ideally do.
Anyway, the point of my example is that if we tell students "This functor preserves products up to isomorphism”, what *we* mean is that “you just have to check that the image of any product cone under the functor is also a product cone" (which is usually easy and non-gnarly to check).
But because of our sloppiness, many students (and professionals!) will think we mean something like “We take it for granted that there are distinguished product cones on either side of the functor; what we want you to do is construct an explicit isomorphism between any cone in the image of a distinguished product cone with the corresponding distinguished product cone on the right side."
I'll paypal you five dollars if you can find these constraints documented anywhere in the cabal-install documentation
I Love to find out that cabal-install will just silently add constraints to your build plan and then fucking attribute them to you. I love it when my build tool gaslights me!!!
Though the question is whether this would be worse than using valid-hole-fits in the Agda repo 🤔🤔🤔🤔
Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).
I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️
Joined Jan 2022
