Zulip Chat Archive
Stream: general
Topic: Category instance for set
ZHAO Jinxiang (Aug 13 2022 at 11:26):
Is there any thing for Category of sets in mathlib?
ZHAO Jinxiang (Aug 13 2022 at 11:29):
Okay, I found it. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/category.20of.20sets/near/207020182
Kevin Buzzard (Aug 13 2022 at 11:37):
The category of sets is Type which does have a category structure in mathlib
Yaël Dillies (Aug 13 2022 at 11:45):
docs#category_theory.concrete_category.types
Kevin Buzzard (Aug 13 2022 at 11:47):
The mathematical differences between sets and types vanish the moment you start thinking categorically
ZHAO Jinxiang (Aug 13 2022 at 11:50):
Yaël Dillies said:
I found category_theory.types. What the difference with category_theory.concrete_category.types?
Yaël Dillies (Aug 13 2022 at 11:51):
One is the category structure. The other is the concrete category structure (that is the category structure + a functor to Type, namely the identity).
Last updated: Dec 20 2023 at 11:08 UTC