Zulip Chat Archive

Stream: mathlib4

Topic: algebra hierarchy


Frederic Paugam (May 18 2021 at 11:51):

@Mario Carneiro Thank you for subscribing me to this list. Sorry for this newbie question: does you algebra hierarchy start with the notion of a category? I would find it pedagogically quite comfortable, since this notion is quite useful (isn't it ;-) in algebra.

Scott Morrison (May 18 2021 at 11:56):

@Frederic Paugam, we certainly have categories, but no, they are not at the base of the algebra hierarchy. It would be unnecessarily cumbersome, specialising to the single object case everywhere.

Frederic Paugam (May 18 2021 at 14:54):

Of course.

Kevin Buzzard (May 18 2021 at 16:43):

@Frederic Paugam A slightly stripped-down version of the algebra heirarchy in Lean 3 is in this gist.


Last updated: Dec 20 2023 at 11:08 UTC