## Stream: general

### Topic: image factorization to functor

#### Qais Hamarneh (Jul 27 2019 at 19:09):

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 (Jul 27 2019 at 19:40):

@Qais Hamarneh Why would it be true?

#### Johan Commelin (Jul 27 2019 at 19:41):

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

#### Qais Hamarneh (Jul 27 2019 at 20:11):

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

Last updated: May 12 2021 at 23:13 UTC