## 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: May 13 2021 at 23:16 UTC