Zulip Chat Archive

Stream: general

Topic: constructive image


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Mar 27 2018 at 17:21):

is this how it is done in HoTT?

view this post on Zulip jmc (Mar 27 2018 at 17:32):

That is usually called the coimage, I think: https://en.wikipedia.org/wiki/Coimage

view this post on Zulip Kenny Lau (Mar 27 2018 at 17:45):

hmm, I've never heard of coimage.

view this post on Zulip Kenny Lau (Mar 27 2018 at 17:45):

I think using this instead of the usual image will make things more constructive

view this post on Zulip 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...

view this post on Zulip jmc (Mar 27 2018 at 17:57):

Anyway, even in classical maths you need the isomorphism theorem to tell you that coimage = image

view this post on Zulip jmc (Mar 27 2018 at 17:58):

In certain settings that theorem might fail

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 27 2018 at 18:05):

@jmc "you are heading down the constructive path?"

view this post on Zulip Kenny Lau (Mar 27 2018 at 18:05):

I've been walking in this path for some time

view this post on Zulip jmc (Mar 27 2018 at 18:06):

Ok, never mind (^; I am wandering back and forth between constructive and classical maths as well

view this post on Zulip Patrick Massot (Mar 27 2018 at 19:09):

Kenny, you should search for coimage on this Zulip forum

view this post on Zulip Patrick Massot (Mar 27 2018 at 19:10):

(usable search is part of the reason why we switched from Gitter to Zulip)

view this post on Zulip Patrick Massot (Mar 27 2018 at 19:10):

You should also stop this constructive madness but this is another story

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:15):

lol

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:19):

@Patrick Massot I searched it and saw you crap-talking about constructivism :P


Last updated: May 18 2021 at 16:25 UTC