@ClarkKent Where do you live?

The obvious proof in classical logic proves something different: if a map has the right cancellation property, then it is not a map for which there exists an element in the codomain such that it is not the image of any element in the domain.

Avoiding double negation is tricky.

@ZhenLin hint: use g = the characteristic function on f(X) and h = the constant map to 1

That uses the law of excluded middle in a very essential way...

how do you figure?

How do you define the characteristic function?

g(y) = 1 for y in f(X), g(y) = 0, for y not in f(X).

You're assuming $y \in \operatorname{im} f \lor y \notin \operatorname{im} f$. :p

You could use the axiom of choice instead of double negation :)

is there some other possibility besides "in" and "not in" a set?

@tb Diaconescu proved that every epimorphism splits in a topos only if it is boolean...

@ClarkKent Oh, just confirming.

Because I am Batman. And I like confirmations!

@ZhenLin hence the :)

@David: We do not know that there is no other possibility. But I think your idea works, suitably modified.

Yes, I know who you are.

The "J" said enough.

@tb Well, see, what I actually want to do is prove it for any elementary topos, not just $\textbf{Set}$. Because it is true, but for stupid reasons...

Hmm, I need to order some food!

@ClarkKent Na, you didn't trick me, I was just trying to confirm. Batman likes security.

@ZhenLin well, you said "set". sets have special properties, the "membership" relationship being one of them.

Holy monkey only the Döner stuff is open!

@David: Fine, I'll rephrase. I want to show that a map is an epimorphism in an elementary topos if and only if it is a surjection in the internal logic of that topos. :p

Oh it is bloody 1:17 AM!

you'd have to define a lot of terms for that to make sense to me

I have writings?

Oh that :-). Thanks.

@David: Well, which is why I simply said "set", because it is just a constructive version of set theory.

@JonasTeuwen somehow the inbox thingie doesn't work for me right now, so I only found out now that I'm a crazy bro... but why?

@ClarkKent Just... messy.

@tb Because I am crazy according to my colleagues because I think about these things. You're a bro because you're cool.

You are crazy and tb is the bro.

Right! Ordered some food.

At 1:24 AM. I'm more a student now than I was when I was a student...!

@JonasTeuwen I see, thanks :)

I first tried to fix the gaps in that paper in Michael's first answer but then I got annoyed because it seemed to miss various points entirely.

Heh, a professor here went back all the way to a 1920's paper by Titchmarsch to understand why his theorem contradiction something 8-).

There's nothing wrong with reading the masters :)

@tb Well, the master was actually the one that was wrong! :D.

His proof seemed okay... But some theorem he used used that.

@ZhenLin well i AM curious, how will you "modify" my idea?

@JonasTeuwen happens occasionally :) But better find out when they're long dead than telling them, I tell ya...

:D.

Well, the idea is to replace $\{ 0, 1 \}$ with the constructive version of "the set of truth values", namely the set of all subsets of $\{ * \}$.

the power set of a singleton, ok

Seeing how they respond me!

@JonasTeuwen I was once shocked to find out that there was a published paper trying to fix a "gap" in a theorem of Banach, notably a theorem I used a whole lot over and over again. The review on MathSciNet even added a few more "fixes". Turns out the author, the referee and the reviewer misread the meaning of "Baire measurability", so the "fixes" were entirely uncalled for. Then I told the author. He was not ... amused.

They don't like set theory.

i would be tempted to call such a thing, simply "2"

@tb He was not amused you telling him or he was not amused with the fact that he was an idiot?

I would be grateful and be very amused as it confirms that I'm an idiot which I knew for a long time already!

@David: Oh no. $2$ is the disjoint union of $\{ * \}$ and $\{ * \}$. That would be akin to asserting that there are only two subsets of $\{ * \}$, a very bold claim.

@JonasTeuwen Probably both. But there's the projection mechanism you know...

Anyone want to help me with a functional equation ?

well, is there a bijection between them?

If I find a "gap" in a proof by Banach I would probably think I had a drink too much.

@David: There is, if and only if logic is classical!

Yes, but was Banach!

Like the coolest Polish dude ever.

Or maybe that was Marcinkiewicz. Interpolate the stars!

@JonasTeuwen well, someone quoted and used a weaker version of Banach's theorem which looked stronger if you misunderstood the meaning of the words.

@ZhenLin, well that confuses me...what other subsets of $\{*\}$ could there be besides $\{*\}$ and {}?

He's joking, right?

@David: Well... we don't know there aren't any other subsets.

@anon It is true isn't it?

@tb Yes, but I wonder... Why would someone publish something about a "gap" in a proof of Banach without properly checking what definitions he uses?

(Concretely, if we are working in the topos of sheaves over a topological space $X$, then there are as many subsets of $\{ * \}$ as there are open subsets of $X$.)

@ClarkKent I am not Dutch.

My advisor and some other professors are very cool guys.

Find functions such that $f(x)$ is increasing. $g(x)+f(x)=2x$ and $g(x)=f^{-1}(x)$

@JonasTeuwen Hence the projection. It also helps if the journal is run by your advisor...

@tb :D.

@Jonas: Funny you should mention that. Two of the biggest names in constructivism are Brouwer and Heyting.

@ZhenLin Yes, but I'm in an applied mathematics department :-). "Brouwer... beer?"

@N3buchadnezzar That's easy isn't it?

@N3buchadnezzar Take a linear function, I'd say.

The sad thing about Brouwer is that his best known theorems are quite non-constructive...

@JonasTeuwen I thought so too, but I do not have any proof of it.

$f(x) = x + 2$, then $f^{-1}(x) = x - 2$, so $g(x) + f(x) = x + x - 2 + 2 = 2x$.

@tb Yeah, but he only saw the light after he proved them.

@tb I think I read somewhere that he was unhappy with his theorems even as he proved them...

Re: Banach's error: Are you referring to the error mentioned [here][1] about "not dealing with the endpoint properly"? [1]:math.vanderbilt.edu/~schectex/ccc/addenda/partd.html

@JonasTeuwen: Isn't applied mathematics necessarily quite constructive?

@MichaelGreinecker No, my group is quite pure...

But it contains analysts!

Those people that whine about physicists not being rigorous but have never heard of the CH.

I'm sure there are analysts who whine about other analysts not being rigorous enough... "no hard estimates!"

"That shit is hokum! Too little dimensions!"

@BillDubuque No, it's about automatic continuity of measurable homomorphisms.

You can easily mock the optimization guys: "That shit is trivial! Only finitely many dimensions!".

All functions on the form f(x) = x + b works...

Speaking of constructivism: Erret Bishop was an analyst who complained a lot about the methods of analysts.

Bishop's constructivism is a little different, but still very good.

I would think they were fools, but they are often better at some parts of analysis than I am so I should stfu.

Bishop is a first rate analyst non-constructive and constructive!

But I have pretty much only my advisor and some weird New-Zealand guy to talk to about mathematics here :-).

Bishop... That isn't the guy mocking Newton right? That was a Bishop. Let's see.

Aye, Bishop Berkeley.

@JonasTeuwen Well you know at least the Bishop-Phelps theorem, right?

Yes.

@ZhenLin Yes! That one.

well i'm confused about what you mean by "surjective", then

@tb Many Bishop's in Choquet...

@DavidWheeler It can hit all the monkeys in the bin!

@David: A map $f : X \to Y$ is surjective just if, for all elements $y$ in $Y$, there exists an element $x$ in $X$ such that $f (x) = y$.

@JonasTeuwen But the question remains: did you hit those you didn't miss?

Hah!

Thinking constructively is hard. Especially after years of training in classical logic.

Who knows...

is $\{*\}$ terminal?

Yes, $\{ * \}$ is terminal. Or rather, I am using it as a shorthand for the terminal object.

It turns out that the powerset of the empty set is terminal, so this is reasonable notation.

but we might have "multi-variate" logic?

Yes.

Here is what the constructive proof looks like: i.imgur.com/kenKe.png

It looks absurd to my eyes, but ah well.

Let us assume I have a n-gon, and I want to turn this into a 3dimensional figure by putting several of these together. For a 3gon, this would require 4 triangles, for a square we would need 6. Does these geometrical objects have a specific name?

@N3buchadnezzar Yes.

ok...just trying to "un-wrap" it: it might be that 1 = {true, false, maybe}, or even the unit interval, for example.

Hmm, I'm reading the draft of the thesis of a friend. He writes (out of the blue): "$T_P$ MOAAAAR $T_P$ ! I NEED FIBERS FOR MY BUNDLE!"

Suggest he should use CH more often...

Yea :D.

You want some fibers? I'll give you some fibers!

I wrote, "We ruthlessly exploit this fact to check the other preconditions for flatness."

@N3buchadnezzar They are called holy monkeys.

@JonasTeuwen I clearly need more whiskey.