bio  website  andrej.com 

location  Ljubljana  
age  44  
visits  member for  5 years, 10 months 
seen  8 hours ago  
stats  profile views  7,808 
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.
2d

reviewed  Close Relationship between $N_{A/K}$ and the reduced norm $\text{nr}_{A/k}$? 
2d

reviewed  Close A compact Alexandrov space with curvature bounded below has curvature bouneded above? 
2d

reviewed  Close Properties of Coefficients of Order Polynomials 
2d

reviewed  Leave Open What are the restrictions in the ramification behavior of a Galois extension of number fields imposed by the Galois group of the extension? 
2d

reviewed  Close Avoiding the range of a bivariate integer function or Diophantine function 
2d

reviewed  Close “Graph Individualization”[ reference request] 
2d

reviewed  Leave Open Defining Global Choice in terms of strong limit cardinals over $ZF$ 
Aug
27 
awarded  Stellar Question 
Aug
20 
comment 
Quotients of powers of the Sierpinski space
You probably know this, but it might be worth mentioning that every $T_0$space is a subspace of a power of Sierpinski space. Hmm, is every space a quotient of a $T_0$space? If so, then we can "fix" your question by pointing out that every space is a subquotient of a power of Sierpinski space. 
Aug
20 
comment 
Defining equivalence of equivalences without assuming extensionality
I do not undestand your comment about "shape". 
Aug
19 
revised 
Is every nonempty $\Delta_0$ set provably the range of some primitive recursive function?
Ok, I was wrong, sorry. Just fixing LaTeX spacing now. 
Aug
19 
revised 
Is every nonempty $\Delta_0$ set provably the range of some primitive recursive function?
Remove wrong usage of "provably", fix LaTeX 
Aug
19 
comment 
Defining equivalence of equivalences without assuming extensionality
I wonder if my last comment makes any sense. If $f_1$ is an equivalence and is homotopic to $f_2$ then surely $f_2$ is an equivalence. 
Aug
19 
comment 
Defining equivalence of equivalences without assuming extensionality
You should also specify that the homotopy between $f_1$ and $f_2$ takes $\mathsf{isequiv}(f_1)$ to $\mathsf{isequiv}(f_1)$, whatever that means. 
Aug
19 
answered  Defining equivalence of equivalences without assuming extensionality 
Aug
19 
comment 
Defining equivalence of equivalences without assuming extensionality
What do you mean "quasiinverses as per section 2.4"? The type of quasiinverses (2.4.5) is not equivalent to the type of equivalences (2.4.11) and should not be used as a substitute. 
Aug
16 
comment 
What's a good introduction to category theory for someone doing analysis?
Probably something that has examples from analysis would be more motivating. 
Jul
30 
comment 
Detecting positive endomaps of the formal reals
How do you extend the map $f$ from reals to the locale of reals? Or this something that Erik does? 
Jul
21 
comment 
Elementary treatment of elementary functions in constructive math
Ok, looking at your example, this isn't really about constructive mathematics. You just want us to do the nasty details for you. You would have exactly the same kind of problem if you replaced "constructive" with "numeric" or "explicit" everywhere. As my professor of analysis said "you do it in the sweat of your face" (that's a Slovene expression). 
Jul
21 
comment 
Elementary treatment of elementary functions in constructive math
Since we seem to be using Cauchy reals it would be a good idea to have countable (or dependent) choice. Otherwise the Cauchy reals are not even Cauchy complete... 