Help finding some category definitions

Stream: new members

[Dean Young]

Hi Folks! I'm looking to start a project on categories here at the Lean community. 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:
1) Create a category given a type for the objects, morphisms, etc. (or some variation of this)
2) Create the opposite category
3) Product and internal hom of categories
4) Isomorphism classes of natural transformations.
5) Simplicial C w/ for a category C
6) Full subcategory consisting of objects matching a certain condition
7) Equalizer and coequilizer of functors.

[Adam Topaz]

I'm happy to help bu the questions are a bit vague. Let's start with an example for 1 -- what category do you want to construct?

[Adam Topaz]

In general, we have an extensive category theory library as part of mathlib, available in the src/category_theory folder of mathlib.

[Adam Topaz]

All of the constructions you asked for are there in some form.