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
doctor seems to think it's just dietary which is gonna be really "funny" when her bp is 21 over 16 again
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)
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
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 👩🏫✍️