image factorization to functor

Stream: general

[Qais Hamarneh]

I have a functor (F : Type u ⥤ Type u) using the category types as defined in
mathlib.category_theory.types.lean
and a function (f: A → F.obj A .
I would like to define the image_factorization of this function on (S : set A) as a : S → F.obj S .
However, I am not able to “convince” lean that (f s ∈ F.obj S).
I tried both subsets and subtypes and it didn’t work.

[Johan Commelin]

@Qais Hamarneh Why would it be true?

[Johan Commelin]

You need some compatibility between f and the functor F, right?

[Qais Hamarneh]

Actually @Johan Commelin , you're right, it might not hold up. Forget about it.