Concrete categories (after port?)

Stream: maths

[Yury G. Kudryashov]

What do you think about the following idea?

• Redo bundled homs as in #2202.
• Restrict concrete categories to bundled categories with BundledHom morphisms.

I'm very far from being expert in category theory, so I don't know, e.g., if we have, e.g., general constructions about categories with instances saying that they produce concrete categories under some assumptions.

[Kevin Buzzard]

One day we'll prove a theorem saying that all abelian categories are concrete, but I think it would be a quite unwise instance :-)

[Yury G. Kudryashov]

Another way is the opposite one: don't use Bundled.α as coercion to Type _.

[Yury G. Kudryashov]

And don't assume that instances available for X are available for toSort (TopCat.of X).

[Yury G. Kudryashov]

Where toSort is a generic coercion for bundled categories.

[Matthew Ballard]

I _very_ briefly played around with changing the CoeFun instance to flow through BundledHom https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20Algebra.2ECategory.2ERing.2EBasic.20!4.233901/near/357677164 but things seemed more pleasant.

[Adam Topaz]

I think all morphisms in bundled categories need to be single-field structures, similar to how docs4#CategoryTheory.Sheaf.Hom is defined which adds a layer of separation from natural transformations.