Small Categories vs Large Categories

Stream: new members

[James Squires]

Hello everyone. I'm very new to Lean and I'm learning how to code by doing some simple category proofs. I'm currently doing a proof on the uniqueness of identity morphisms in a category, but I saw that I can use either large or small categories depending on if I want my morphisms to live in separate universes. Is this kind of preference/organization, or will I just learn over time the merits of choosing small or large?

Thank you

[Aaron Liu]

you should probably just use docs#CategoryTheory.Category

[Aaron Liu]

small and large categories I feel is kind of important your proofs should work for both

[James Squires]

Thank you, makes sense!