Zulip Chat Archive
Stream: general
Topic: constructive image
Kenny Lau (Mar 27 2018 at 17:20):
Maybe we should define the image of a map f:X->Y to be X quotient by the relation that x~y iff f(x)=f(y)
Kenny Lau (Mar 27 2018 at 17:21):
is this how it is done in HoTT?
jmc (Mar 27 2018 at 17:32):
That is usually called the coimage, I think: https://en.wikipedia.org/wiki/Coimage
Kenny Lau (Mar 27 2018 at 17:45):
hmm, I've never heard of coimage.
Kenny Lau (Mar 27 2018 at 17:45):
I think using this instead of the usual image will make things more constructive
jmc (Mar 27 2018 at 17:56):
O.o... you are heading down the constructive path? It seems that happens to every one who starts doing formal proofs...
jmc (Mar 27 2018 at 17:57):
Anyway, even in classical maths you need the isomorphism theorem to tell you that coimage = image
jmc (Mar 27 2018 at 17:58):
In certain settings that theorem might fail
jmc (Mar 27 2018 at 17:59):
E.g. in topology: you will get the same set, but the quotient topology on the coimage may be finer then the subset topology on the image
Kenny Lau (Mar 27 2018 at 18:05):
@jmc "you are heading down the constructive path?"
Kenny Lau (Mar 27 2018 at 18:05):
I've been walking in this path for some time
jmc (Mar 27 2018 at 18:06):
Ok, never mind (^; I am wandering back and forth between constructive and classical maths as well
Patrick Massot (Mar 27 2018 at 19:09):
Kenny, you should search for coimage on this Zulip forum
Patrick Massot (Mar 27 2018 at 19:10):
(usable search is part of the reason why we switched from Gitter to Zulip)
Patrick Massot (Mar 27 2018 at 19:10):
You should also stop this constructive madness but this is another story
Kenny Lau (Mar 27 2018 at 19:15):
lol
Kenny Lau (Mar 27 2018 at 19:19):
@Patrick Massot I searched it and saw you crap-talking about constructivism :P
Last updated: Dec 20 2023 at 11:08 UTC