direct limits and bundled homs

Stream: maths

[Yury G. Kudryashov]

I'd like to rewrite algebra/direct_limit using bundled homs. Is there somebody already working on it?

[Yury G. Kudryashov]

Should I reuse some definitions from category_theory/?

[Yury G. Kudryashov]

For me this is a part of the quest "get rid of is_ring_hom"

[Scott Morrison]

So... this stuff is already pretty duplicated.

[Scott Morrison]

I've never stopped to look very hard, but you might look at the algebra/category/*/limits.lean and algebra/category/*/colimits.lean files.

[Scott Morrison]

What is missing the categorical setup is anything about filtered limits