Qais Hamarneh (Jul 27 2019 at 19:09):
I have a functor
(F : Type u ⥤ Type u) using the category types as defined in
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
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