16,634 reputation
14098
bio website andrej.com
location Ljubljana
age 43
visits member for 4 years, 10 months
seen yesterday
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.

Aug
19
revised In the category of sets epimorphisms are surjective - Constructive Proof?
deleted 14 characters in body
Aug
19
comment In the category of sets epimorphisms are surjective - Constructive Proof?
It is not really different, but I would say that it is less mysterious.
Aug
18
answered In the category of sets epimorphisms are surjective - Constructive Proof?
Aug
13
comment How to define the input of computable function or Turing machine over real numbers
I specifically preempted my comment with "regarding the question..." so as to make it clear I was not discussing complexity (although what I said still stands, except as you note, things get more complicated). Of course complexity is a very interesting issue. Some work has been done in Type Two Effectivity. Essentially, complexity on a space $X$ makes sense when each point of $X$ has compactly many representatives, see e.g. homepages.inf.ed.ac.uk/als/Research/Others/schroeder-mlq04.pdf
Aug
13
comment How to define the input of computable function or Turing machine over real numbers
No, that is not the point. We can implement the reals, but it's a bit trickier than you'd expect. You cannot naively expect to implement equality as a boolean test, for instance, but you can implement inequality as a semidecidable test. So there are some surprises, and that's why people are so confused about computation over the reals.
Aug
13
comment How to define the input of computable function or Turing machine over real numbers
Regarding the question "what representation of reals do we have to choose", please read my answer at cstheory.stackexchange.com/a/16547/705
Aug
11
comment Delooping in homotopy type theory
I agree with you, of course. A major winning point for HoTT is that "$\infty$-groupoid" is just "type", and that equivalence requires no higher-dimensional conditions (which one might expect). So we do have examples where an infinite amount of higher-dimensional structure is dealt with without explicit reference to it.
Aug
11
comment Salvaging Leibnizian formalism?
I think putting some mathematical sense into what physicists do (without trying to change physicists too much) would be of great value.
Aug
11
comment Salvaging Leibnizian formalism?
Ah. Well, anyhow, the derivation is not particularly complicated, I added it to my answer. Why aren't you happy with it?
Aug
11
revised Salvaging Leibnizian formalism?
added 506 characters in body
Aug
11
comment Salvaging Leibnizian formalism?
With regards to the chain rule of derivatives, in Bell's primer it is called "composition rule" and is treated in detail on page 28, end of section 2.1. Or are we talking about two different things? I cannot find any exercises on page 69. I am looking at ISBN 0 521 62401 0 (hardback), printed in 1998.
Aug
11
comment Salvaging Leibnizian formalism?
It is not at all clear to me what you mean by "salvage Leibnizian formalism". SDG keeps all the essentials of it, so it salvages it. If you worry about little details such as "we do not divide but rather cancel on both sides" then yes, SDG does not "salvage" Leibniz's formalism.
Aug
11
comment Salvaging Leibnizian formalism?
Have you read SDG treatments of the chain rule? I don't find them particularly impractical. It's not clear to me what you'd like. SDG recovers all the essential ideas at a price (intuitionistic logic, can't divide by an infinitesimal). Are you looking for a better price, or are you hoping there is free lunch?
Aug
11
answered Salvaging Leibnizian formalism?
Aug
11
comment Delooping in homotopy type theory
I wonder if we should give a HoTT student the task of defining associahedra in type theory. It sounds horrible.
Aug
6
comment Existence of solutions of a polynomial system
@JohnMount: and now that you're on Mathoverflow, make sure statistics and probability are your favorite tags, and help answer some questions!
Aug
5
accepted Existence of solutions of a polynomial system
Aug
5
revised Existence of solutions of a polynomial system
deleted 2 characters in body
Aug
5
comment Existence of solutions of a polynomial system
You should try using it through not-iPhone.
Aug
5
awarded  Nice Question