CategoryTheory.Functor.essImage: `Set` defeq abuse

Stream: mathlib4

[Yury G. Kudryashov]

We define docs#CategoryTheory.Functor.essImage as a set, then use it as a predicate (e.g., by using dot notation). Should we resolve it one way or another? Note: I never used this part of the library, so I have no opinion on which way is better.

[Yury G. Kudryashov]

I found this while trying to turn Set into a one-field structure (not yet sure if this is a good change, let's not discuss it here anyway).

[Adam Topaz]

I think we want it to be a set

[Adam Topaz]

We want to be able to say things of the form "This object is an element of the essential image" using Membership notation, for instance.

[Adam Topaz]

I guess the real question is whether we want docs#CategoryTheory.FullSubcategory to take a set or a predicate

[Matthew Ballard]

I would lean predicate. That’s how I think of things in real life

[Adam Topaz]

you mean for the full subcat?

[Adam Topaz]

I'm the other way -- I think of it as being associated to a (sub)set of objects.

[Matthew Ballard]

Yeah, I would go predicate everywhere but don’t have strong opinion

[Joël Riou]

In a near future, when I start PRing notions of triangulated subcategories, I will have to manipulate some "sets" of objects in a category. For example, I will introduce a typeclass Set.RespectsIso {C : Type*} {Category C] (S : Set C) : Prop. Then, I would prefer if we do not change sets into predicates.