Zulip Chat Archive

Stream: new members

Topic: Nested categories on the same type


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:40):

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

view this post on Zulip Aaron Anderson (Aug 11 2020 at 00:40):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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: May 13 2021 at 23:16 UTC