I'm looking to start a project on categories in Lean. I was wondering if anyone could help me out with finding a few of the basic constructions... maybe you know where to look.
I'd like to be able to:
- Create a category given a type for the objects, morphisms, etc. (or some variation of this)
- Create the opposite category
- Product and internal hom of categories
- Isomorphism classes of natural transformations.
- Simplicial C w/ for a category C
- Full subcategory consisting of objects matching a certain condition
- Equalizer and coequilizer of functors.