19,495 reputation
448113
bio website andrej.com
location Ljubljana
age 44
visits member for 5 years, 10 months
seen 8 hours ago
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 non-empty $\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 non-empty $\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 "quasi-inverses as per section 2.4"? The type of quasi-inverses (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...