algebra hierarchy

Stream: mathlib4

[Frederic Paugam]

@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]

@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]

Of course.

[Kevin Buzzard]

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