Nested categories on the same type

Stream: new members

[Aaron Anderson]

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]

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

[Scott Morrison]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

(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]

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