← Feed

Posts

• Post #2538505

  One of the biggest realizations we had about Cubical Agda is that the cubical Path type is not a *replacement* of the inductive Identity type, but instead *complementary* to it. The reason being that they have very different definitional behavior. An intuition for why is that the inductive Identity type is defined by a left adjoint universal property whereas the Path type is defined by a right adjoint universal property. This means that the inductive Identity type works well when we are mapping...

• Post #2531598

  Saying that algebraic effects are an alternative to monads is a bit like saying group presentations are an alternative to groups

• Post #2162175

  Honestly all the stuff about (normal) subgroups and ideals is a lot more palatable now that I am familiar with displayed category theory and see the displayed universal properties there. E.g. the universal property of a quotient by a normal subgroup/ideal is nicely expressed in those terms

• Post #2044539

  Just finished Dune Messiah. I know the series is notorious for eventually being terrible but how far do y'all actually recommend reading?

• Post #1905767

  Never talk about goblins, gremlins, raccoons, trolls, ogres, pigeons, or other animals or creatures unless it is absolutely and unambiguously relevant to the user's query This is real lmao: https://github.com/openai/codex/blob/70ac0f123c4b1869c9069d5b34e367b96c28bfad/codex-rs/models-manager/models.json#L55

• Post #1905766

  Presheaves on C are monadic and comonadic over Families on |C|

• Post #1905765

  most of the time I get stuck on a problem in Aluffi, it shows up in the errata that the question is wrong. I'll take that as encouragement that I understand wtf I'm doing but I should probably look at the errata first to save myself the frustration haha

• Post #1905764

  hm it may actually be impossible to implement my participation grade formula in canvas...

• Post #1840433

  I got the NSF CAREER award y'all: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2540652

• Post #1815123

  The kernel of a group homomorphism phi : G -> H has a universal property in the category of groups: it's the equalizer of phi and the 0 morphism. It also has a universal property in the category of subgroups displayed over the category of groups: it is the cartesian lift along phi of the trivial subgroup { e } of H.

• Post #1768648

  RE: https://mathstodon.xyz/@dimpase/116483887742907549 MINIO: How do you select a problem to study? ATIYAH: I think that presupposes an answer. I don’t think that’s the way I work at all. Some people may sit back and say, “I want to solve this problem” and they sit down and say, “How do I solve this problem?” I don’t. I just move around in the mathematical waters, thinking about things, being curious, interested, talking to people, stirring up ideas; things emerge and I follow them up. Or I se...

• Post #1639319

  I always liked this intuition for open sets (https://math.stackexchange.com/a/31946/281259) which also fits nicely with synthetic topology in the effective topos. It seems like it applies just as well to Locales as spaces. Challenge: how would you generalize this intuition from opens of a space/locale to the sheaves of a Grothendieck topos? Instead of having a notion of which propositions are "open" you have a notion of which...dependent sets are "open" (i.e....

• Post #1639316

  should I re-learn abstract algebra so I can learn algebraic geometry so I can understand any of the examples when I read about sheaves/topos theory

• Post #1471255

  Tornado in Ann Arbor last night! Had to go shelter in the basement at 1:30am but thankfully it didn't hit our side of town. Also thankfully my 2yo almost entirely slept through us carrying her to the basement and back.

• Post #1471253

  Love for HoTT is rekindling. HITs are OP

• Post #1471252

  Got recruiter spam from someone with the incredibly annoying email signature "Co-founder XXX (McKinsey & Harvard Alum)"

• Post #1471251

  The burden of proof is on the skeptics to demonstrate that LLMs *can't* currently slop out verified compilers??

• Post #1471250

  damn all these years later and now I have to use Facebook bc that's where everyone is selling their shit