@highergeometer@mathstodon.xyz
Post #1558696
2026-04-22 03:52 UTC
I have a hankering to completely rewrite Makkai's anafunctor paper as internal categories in a well-pointed class category, rather than how it's currently specified, which is essentially using some kind of dependent types machinery.
Replies (2)
-
@highergeometer@mathstodon.xyz 2026-04-22 03:53
It would be a lot less symbol-heavy, that's for sure, but more diagrams.
-
@antoinechambertloir@mathstodon.xyz 2026-04-22 06:23
@highergeometer what's in this paper? (What's an anafunctor?)