@maxsnew@types.pl

Max S. New ⚜️ @maxsnew@types.pl · May 28, 2026

Replying to @koronkebitch@types.pl

@koronkebitch@types.pl congratulations 👏

2

0

Max S. New ⚜️ @maxsnew@types.pl · May 11, 2026

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

15

4

2

0

Max S. New ⚜️ @maxsnew@types.pl · May 08, 2026

Replying to @mc@mathstodon.xyz

@mc@mathstodon.xyz @JacquesC2@types.pl Universal Element of a presheaf is an element such that composition with it is an equivalence: https://github.com/agda/cubical/blob/7a4fbe151cc7185b5b782f8257976753317ed176/Cubical/Categories/Presheaf/Representable.agda#L84 PshHom is a natural transformation of presheaves (defined in a way that is universe polymorphic: https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Morphism/Alt.agda#L87) PshIso is a PshHom that is pointwise an isomorphism (https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Morphism/Alt.agda#L275) Note that isomorphism and equivalence are equivalent. The Yoneda lemma says that an element P x can be uniquely extended to a PshHom (C [-, x]) P that sends the identity to the specified element. We call this operation "yoRec". Then UniversalElement is just saying that the resulting PshHom you get from the element is a PshIso. This equivalence is proven here: https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Representable/More.agda#L156

3

0

Max S. New ⚜️ @maxsnew@types.pl · May 08, 2026

Replying to @mc@mathstodon.xyz

@mc@mathstodon.xyz @JacquesC2@types.pl Maybe that's the difference between PshIso and UniversalElements in our formulation?

1

0

Max S. New ⚜️ @maxsnew@types.pl · May 07, 2026

Replying to @mc@mathstodon.xyz

@mc@mathstodon.xyz @JacquesC2@types.pl I wouldn't take any notes you find in there as particularly definitive, they're just some thoughts that I put down at some point and likely outdated. Our approach is to encode all universal properties as representable functors (and displayed versions of this). This is motivated by wanting to have one single definition of universal property out of which concrete instances would be special cases so that we could get for free many of the reasoning principles you want out of a universal property. I don't think this is particularly radical approach but compared to textbooks we try very hard to adhere to the DRY principle and formulate things in as much generality as possible. So for instance we prefer to avoid defining functors by hand when they have a universal property (https://github.com/um-catlab/cubical-categorical-logic/blob/main/Cubical/Categories/FunctorComprehension/Base.agda) which gets you things like functoriality of products, exponentials "for free". We also use displayed categories heavily because it's just much more natural way to handle indexing in dependent type theory. We have started integrating them further into the core of the library. For example, I'm sure no sane textbook defines the binary product of categories as a total category of a weakened category (https://github.com/agda/cubical/blob/master/Cubical/Categories/Instances/BinProduct.agda#L23) We also have some fun defining the universal property of free constructions to produce a global section of a displayed category and then derive the more typical universal property from that (https://github.com/agda/cubical/blob/7a4fbe151cc7185b5b782f8257976753317ed176/Cubical/Categories/Instances/Free/Category/Quiver.agda#L122) There's also some more strange stuff that is pretty experimental in there. We define bifunctors in an unusual that helps us to produce nicer compositional definitions of things like the exponential. There's a whole sub-module of large and locally small categories that we haven't adopted yet but helps us handle some very universe-polymorphic stuff better. And there's probably like 3 different definitions of presheaf and 5 different definitions of natural transformation of (displayed) presheaves that all have weird tradeoffs that we haven't totally settled yet. (btw what's the difference between representable functors and universal arrows? Aren't they the same thing?)

13

2

1

0

Max S. New ⚜️ @maxsnew@types.pl · May 07, 2026

Replying to @mc@mathstodon.xyz

@mc@mathstodon.xyz @JacquesC2@types.pl Honestly this library is not documented for use by people outside of my lab rn. When we upstream stuff to cubical we clean things up and document them more

4

1

0

Max S. New ⚜️ @maxsnew@types.pl · May 03, 2026

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

5

4

0

Max S. New ⚜️ @maxsnew@types.pl · May 01, 2026

Replying to @markusde@mathstodon.xyz

@markusde yea I can do it myself in a spreadsheet, but I would prefer if the students could see the calculation

0

1

0

Max S. New ⚜️ @maxsnew@types.pl · May 01, 2026

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

1

4

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 30, 2026

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

8

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 30, 2026

Replying to @emilyriehl@mathstodon.xyz

@emilyriehl There's a typo: the representative who introduced the Fair Representation Act's name is Donald Beyer not Boyer

2

1

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 30, 2026

Replying to @emilyriehl@mathstodon.xyz

@emilyriehl

Voters in each district submit ballots ranking all the candidates, like in an instant runoff voting election. If some candidate exceeds the threshold for election, earning say 40% of the vote, the excess votes are reallocated to other candidates in proportion to voters' choices.

Does this mean that voters who voted for the plurality candidate have more influence because their vote counts both towards the election of their top priority as well as to their lower priority votes?

1

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 30, 2026

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

www.nsf.gov

Award Details - NSF Award Search

Find award details and explore award abstracts and publications.

86

22

4

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 29, 2026

Replying to @ohad@mathstodon.xyz

@ohad I'd be surprised if there's no earlier reference. There's a cool way to view Yoneda/CoYoneda in these terms btw that I think I've posted here before. CoYoneda says that every presheaf is a canonical quotient of a free algebra, and Yoneda says that every presheaf is a canonical sub-coalgebra of a cofree coalgebra.

4

0

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 29, 2026

Replying to @ohad@mathstodon.xyz

@ohad I originally learned this from Dima's work. I may have a Good Use of this in future manuscript but it remains to be seen

2

5

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 29, 2026

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

13

12

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 29, 2026

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

11

3

2

1

Max S. New ⚜️ @maxsnew@types.pl · Apr 28, 2026

RE: @dimpase@mathstodon.xyz

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 see something which connects up with something else I know about, and I try to put them together and things develop. I have practically never started oﬀ with any idea of what I’m going to be doing or where it’s going to go. I’m interested in mathematics; I talk, I learn, I discuss and then interesting questions simply emerge. I have never started oﬀ
with a particular goal, except the goal of understanding mathematics.

I'm not allowed to say this but honestly this is what I do in computer science

20

1

3

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 28, 2026

Replying to @jpoiret@types.pl

@jpoiret

I also like having this precise tool for specific applications!

I'm curious to know what specific applications you have in mind.

@jonmsterling @carloangiuli

1

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 25, 2026

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

11

1

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 25, 2026

Replying to @pamorim@mathstodon.xyz

@pamorim That's one way to define it but that requires defining the Cartesian lifts from the start. You can also directly define a displayed category of subgroups as having an object S over a group G being a subgroup and then a displayed morphism over a homomorphism phi : G -> H from S over G to T over H to be a proof that for all s in S. phi(s) in T. Then Cartesian lifts have a universal property in this displayed category. More generally you can define e.g. a displayed category of monomorphisms over any category. I like the perspective of the displayed category first because there's something slightly non-trivial in defining the Cartesian lift: you have to prove that the inverse image phi^*(T) is actually a subgroup not just a subset. And for the general monomorphism case you can define the displayed category of monos even if the category doesn't have the pullbacks you need to define the inverse image

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 25, 2026

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.

13

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 24, 2026

Replying to @jdw@mathstodon.xyz

@jdw It's funny I was going to read Vakil and then it said in the intro that you should also read another book at the same time, such as Gortz-Wedhorn

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 24, 2026

Replying to @burakemir@discuss.systems

@burakemir yea but I already know those

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 24, 2026

Replying to @jdw@mathstodon.xyz

@jdw well based on skimming the intros to some alg geometry books (Gortz-Wedhorn and Vakil) I think I clearly need to at least review some theory of commutative rings/ideals/modules

4

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 24, 2026

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

2

8

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 23, 2026

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. sheaves)? And can we have "synthetic topos theory" by generalizing a dominance from a universe of propositions to a universe of sets?

11

7

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 20, 2026

Replying to @markusde@mathstodon.xyz

@markusde @ionchy yea I'll take 255lb of barbell plates so I can bring back the gym 🐀 posts

3

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 20, 2026

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

6

3

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 17, 2026

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

11

9

1

Max S. New ⚜️ @maxsnew@types.pl · Apr 17, 2026

Replying to @csgordon@discuss.systems

@csgordon @carloangiuli

Yea my own experience was:

Learned touch-typing in an actual high school "keyboarding" class (semi-rural Louisiana public school ~04-05)
Learned emacs out of necessity when I took intro to systems in undergrad and had to use an editor while ssh'd into the lab machines. This was recommended by the course staff and they gave us some links but nothing crazy.

Wild to think that students today have regressed in basic computer skills.

2

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 17, 2026

Replying to @carloangiuli@mathstodon.xyz

@carloangiuli @csgordon Aren't these first-time programmers? Shouldn't we expect them to be unfamiliar with text editors?

3

6

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 16, 2026

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

0

1

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 16, 2026

Love for HoTT is rekindling. HITs are OP

11

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 15, 2026

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.

10

0

Max S. New ⚜️ @maxsnew@types.pl · Apr 15, 2026

Replying to @dif@mathstodon.xyz

@dif no

2

0

Max S. New ⚜️ @maxsnew@types.pl · Mar 20, 2026

Replying to @gallais@mamot.fr

@gallais was wondering who tf that guy was

2

1

0

Max S. New ⚜️ @maxsnew@types.pl · Mar 07, 2026

Replying to @jcoglan@mastodon.social

@jcoglan and in open source LLMs can now automate the process of giving someone else horrible code review to do

1

0

Max S. New ⚜️ @maxsnew@types.pl · Mar 05, 2026

Replying to @markusde@mathstodon.xyz

@markusde co-authored by Claude is "sent from my iPhone" for programmers

19

0

5

0

Max S. New ⚜️ @maxsnew@types.pl · Feb 06, 2026

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 out of it: i.e. when we want to use J. This means that often when you want to *abstract over* a *definitional* equality then you should use the inductive Identity type because a definitional equality will be refl and so the abstraction will reduce to the exact thing you started with. This is not the case for the Path type because you will end up with a transport refl, which doesn't typically reduce.

On the other hand, by nature of being a right adjoint type, the Path type has a definitional eta equality (just like products and functions). This makes it so that a Path in a product type is not just isomorphic to paths between the projections but that this Isomorphism is a *definitional* equality. This is not the case for the inductive Identity type, which doesn't have definitional eta because it's inductive (same for sums/empty). There the Isomorphism between Identity at a product type and pair of identity proofs is not definitional because the round trip will be stuck pattern matching on the original equality.

So we have found that in certain spots in the library it is essential to use inductive equality to avoid large blowup of goals or unnecessary transports when abstracting over things. On the other hand we have at least one spot where it was essential to use Path to get some definitional equalities to hold for structures that contained equality proofs in them.

21

3

2

Max S. New ⚜️ @maxsnew@types.pl · Oct 15, 2025

Replying to @zwarich@hachyderm.io

@zwarich no fucking way. Smash that edit button

1

0

Max S. New ⚜️

Posts

Award Details - NSF Award Search

Remote instance

Media