18,231 reputation
344103
bio website andrej.com
location Ljubljana
age 43
visits member for 5 years, 1 month
seen 1 hour ago
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.

Dec
10
comment How to generate $n$ FP32 rationals s.t. no two distinct k-el. subsets have same sum?
Where are these matrices coming from? Are you generating them so fast you can't even afford to calculate an MD5 hash for each one of them?
Dec
10
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
Ah yes, the usual terminological confusion. I have to choose between two evils. If I say "intuitionistic" someone will think I am saying "Brouwerian" (which assumes continuity and the fan principle), but if I say "constructive" people will think I am saying "Bishop style" (which assumes dependent choice). I am talking about a very general phenomenon which works in pure intuitionistic logic. This suffices for arguments about pullbacks, but of course we could add any axioms which are valid in an lccc extending topological spaces (such as countable choice).
Dec
9
awarded  Nice Answer
Dec
8
comment Topological retraction vs categorical retraction
I see. Under that reading you indeed have a counter-example, but that reading is completely unreasonable. If that's what the OP asked, then he should be told that's the wrong thing to ask.
Dec
8
comment Topological retraction vs categorical retraction
@MarcHoyois: that's completely irrelevant. Of course $A$ need not be a subspace of $X$, there's no way to make something into a subspace if it isn't (this is a case of set theory doing harm). The answer I give is the best possible: there is a canonical subspace $A'$ which is homeomorphic to $A$. Moreover, the pair of arrows $(r,f)$ is isomorphic to the pair of arrows $(f \circ r, \mathsf{incl}_{\mathsf{im}(f)})$ in the relevant category (whose objects are pairs of arrows $A \to X$ and $X \to A$ and morphisms are the evident ones).
Dec
8
comment Topological retraction vs categorical retraction
And if $A$ is a meridian, then there is a topological retraction of the torus onto it, so your example still doesn't work. Let $S^1$ be the unit circle in $\mathbb{C}$. Then we take $X = S^1 \times S^1$ and $A = S^1 \times \{1\}$. A topological retraction $r : X \to A$ is just $r(z,w) = (z,1)$.
Dec
8
comment Topological retraction vs categorical retraction
Do you really mean "null-homotopic", or did you mean "meridian" (or "longitude")? the way I read this a "null-homotopic circle on a torus" is a very small circle which obviously is not a retract of the torus. That's what I am complaining about.
Dec
8
answered Topological retraction vs categorical retraction
Dec
8
comment Topological retraction vs categorical retraction
This doesn't work as you have to provide $r : X \to A$ as well.
Dec
8
comment Topological retraction vs categorical retraction
I am typing up the answer if you can wait for 2 minutes...
Dec
8
comment Topological retraction vs categorical retraction
It follows that $\iota$ is injective!
Dec
8
comment Topological retraction vs categorical retraction
I fixed the first definition so that it makes sense.
Dec
8
revised Topological retraction vs categorical retraction
added 32 characters in body
Dec
7
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
Sure. Modulo a technical difference between types and sets (which is irrelevant in mathematical practice), the internal language of a topos is (intutionistic) Zermelo's bounded set theory (no axiom of replacement, all quantifiers must be explicitly bounded by a set). So no matter how complicated the objects of the topos are, in the internal language they are sets (or types, to be more precise).
Dec
6
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
@PeterLeFanuLumsdaine: yes, thanks! I've been joining paths too much lately...
Dec
5
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
Continuity is very much an appropriate notion for constructive analysis, and is in fact unavoidable. It's just that you need to approach the step "function" a bit more carefully, as it is not a function defined everywhere. It is defined on $(-\infty, 0] \cup [0, \infty)$, which is a bit like the real line with a "space-time anomaly" at $0$, so when the Enterprise flies through it special things happen – for example a bit in Data's memory suddenly goes from 0 to 1.
Dec
5
answered Formal languages with non-unique interpretations of terms
Dec
4
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
You used excluded middle when you assumed that $f$ is defined everywhere on $\mathbb{R}$, because for that to be true you need $\forall x \in \mathbb{R} . x < 0 \lor x \geq 0$. That's excluded middle. And no, you cannot implement a program for calculating $f$. Floating points are not reals. A real $x$ is represented on a computer as a function which takes $k \in \mathbb{N}$ as input and produces a rational number $p/q$ which is within $2^{-k}$ from $x$. How would you implement your $f$ with this representation of reals?
Dec
4
comment Is the defining bijection for a pullback of topological spaces a homeomorphism?
It would be good to know why I deserved a -1 for my answer. My answer is homotopic to Tom's.
Dec
4
revised Is the defining bijection for a pullback of topological spaces a homeomorphism?
added 1776 characters in body