bio  website  andrej.com 

location  Ljubljana  
age  43  
visits  member for  4 years, 10 months 
seen  yesterday  
stats  profile views  6,072 
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/schroedermlq04.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 higherdimensional conditions (which one might expect). So we do have examples where an infinite amount of higherdimensional 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 notiPhone. 
Aug 5 
awarded  Nice Question 