Post #2636097
2026-05-07 11:58 UTC
@maxsnew@types.pl @mc@mathstodon.xyz Yeah, I should have warned Matteo that your library requires serious archeological skills to peruse on one's own!
Having said that, Matteo definitely has the categorical chops to "get" what you're doing -- more so than me, frankly.
Replies (1)
-
@mc@mathstodon.xyz 2026-05-07 14:20
@JacquesC2@types.pl @maxsnew@types.pl I didn't quite read any Agda but I scavenged a LaTeX note under Notes/ that makes the point that even if there are equivalent definitions for universal objects in category theory, you prefer the representability ones @maxsnew@types.pl Is this takeaway coming from the formalization effort? Also, is it a matter of making a canonical choice for all instances or are there actual benefits when using representability vs universal arrows or 'first-order' universal properties?