Zulip Chat Archive

Stream: new members

Topic: Nested categories on the same type


Aaron Anderson (Aug 11 2020 at 00:37):

I'm looking at the category theory library for the first time today, and I'm wondering if there's any smooth way of dealing with multiple categories on the same type of objects?

Scott Morrison (Aug 11 2020 at 00:39):

Use type synonyms, just as in any situation that you want multiple instances on the same type.

Scott Morrison (Aug 11 2020 at 00:40):

Although your subject line says "nested", which I can't guess the meaning of.

Aaron Anderson (Aug 11 2020 at 00:40):

Sorry, I was going to follow that up, and didn't expect such a quick response

Aaron Anderson (Aug 11 2020 at 00:42):

Essentially what I mean is that the different categories will be subcategories of one another, but if I'm using type synonyms, faithful functors will take care of that

Aaron Anderson (Aug 11 2020 at 00:43):

(I want to create a category of bundled first-order homomorphisms and a category of bundled first-order embeddings, and also elementary homomorphisms and elementary embeddings)

Aaron Anderson (Aug 11 2020 at 00:59):

So probably if I come up with better names for these things, and define the inclusion functor, the following code will be good?

def hom_cat (L : Language.{u}) : Type (u + 1) := bundled (Structure L)

def embed_cat (L : Language.{u}) : Type (u + 1) := bundled (Structure L)

instance hom_cat.bundled_hom (L : Language.{u}) : bundled_hom (first_order_hom L) := sorry

instance embed_cat.bundled_hom (L : Language.{u}) : bundled_hom (first_order_embedding L) := sorry

Last updated: Dec 20 2023 at 11:08 UTC