Open fredrik-bakke opened 9 months ago
Fibrations will be very nice to have, for instance if we want to make our extensionality proofs even more slick. We should follow the example of the 1lab on this front.
Feel free to edit the main comment btw!
I think we should try to make more concrete goals that clearly focus the efforts of the person working on them. Goals of the form "formalize the theory of ..." are not attainable. An example of a concrete goal would be "Show that right adjoints preserve limits", or "Prove Beck's monadicity theorem". Notice how different those sound than "formalize category theory".
Btw this issue seems well organized and does try to focus the efforts of a contributor. So I don’t want to change this issue. But I wouldn’t like to see many future issues of the form “Formalize the theory of…” because in general I don’t think they’re so inspiring
I think we should try to make more concrete goals that clearly focus the efforts of the person working on them. Goals of the form "formalize the theory of ..." are not attainable. An example of a concrete goal would be "Show that right adjoints preserve limits", or "Prove Beck's monadicity theorem". Notice how different those sound than "formalize category theory".
Please do! I posted this issue in hopes of getting help shaping more concrete goals. I'm not planning to implement everything in this issue myself, but I'll see if I can phrase some more concrete goals as well. I feel somewhat inspired to do fibrations, so I'll try to do that soon. But otherwise, everything is up for grabs, including developing the issue body.
Awesome! I think fibrations will be really nice to have
This issue outlines formalization goals for the
category-theory
module.Formalization targets
The following list outlines missing formalizations that should be part of any standard library on category theory:
It would also be nice to have