categorical subobjects

Stream: maths

[Johan Commelin]

Why is docs#category_theory.subobject.map a functor instead of a regular function between lattices? @Bhavik Mehta @Scott Morrison

[Bhavik Mehta]

I believe there are legitimate use cases for both - iirc there's a function to convert from the functor to a (monotone) function. It's nice to define it this way because the functorial properties for most of the functions on lattices can be deduced immediately from functors in the over category, and there are times you want to compose the functor with other functors which aren't just on lattices

[Johan Commelin]

Ok, that makes sense.