## 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

lol

#### 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