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

Jul
18
comment How should I be thinking about object classifiers / universal fibrations / universes?
Can we cook up a universe (in some non-trivial category) which classifies everything, including itself? Presumably a model of $\mathtt{Type} : \mathtt{Type}$ will do it, so various domain-theoretic models.
Jul
16
comment opposite category
Are you saying the Vierergruppe acts on 2-cats?
Jul
16
comment How should I be thinking about object classifiers / universal fibrations / universes?
You don't mean the identity to be universal, but rather the thing you call "some sort of universal fibration" in the displayed formula.
Jul
12
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
@ZhenLin: the context in this case should be local, i.e., we require an abstraction so that we can write $\int\int x y \,dx\,dy = \lambda x y \,.\, \frac{1}{4} x^2 y^2$ or some such. For consider the case $x \cdot \int \int x y \, dx \, dy$, what is the answer, and should it be the same as the answer to $x \cdot \int \int z y \, dz \, dy$? You can't resolve the mess until you introduce proper abstractions and bound variables.
Jul
12
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
We could also draw all the diagrams in the other direction...
Jul
12
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
I don't really want to get into a flame war, but when you say that $\frac{dy}{dx}$ refers to the standard part, you're dragging in Robinson's non-standard analysis, which may not be everyone's favorite, especially physicists might prefer nilpotent infinitesimals. Regarding $x$ being the identity function: how about $\int \int x y \, dx \, dy$, do I get two identity functions $x$ and $y$, which magically are not the same? Or are they now projections. If they are projections, perhaps we could use sane notation instead, rather than keep putting kludges on top of kludges. Ok, that's a flame war ;)
Jul
11
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
Persistence, persistence, good arguments, and persistence.
Jul
11
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
I am referring to $\frac{dy}{dx}$ and the fact that it's legal to write $\int x^2 dx = x^3/3 + C$ (which exposes the bound variable $x$), and the fact that ${{\Gamma_{ij}}^{kl}}_{mn}$ means something.
Jul
11
comment What recent programmes to alter highly-entrenched mathematical terminology have succeeded, and under what conditions do they tend to succeed or fail?
Given that we still use 17th century broken notation in analysis, and people actually think the summation conventions are ok, I wouldn't harbor any hopes that things will get better.
Jul
9
answered Is there one binary operation foundational for set theory?
Jul
4
comment Is anyone talking about partial interpretations of theories? (Edited)
Yup, good point by Joel.
Jul
3
comment Is anyone talking about partial interpretations of theories? (Edited)
Sure, in essence you are admitting a lot of constants into the theory, one for each element of $K$, or alternatively a lot of operations -- one scalar multiplication for each element of $K$. In categorical logic this is a natural thing to do.
Jul
3
comment Analogy between variable substitution and the moving lemma
Where in the HoTT book is this?
Jul
2
awarded  Curious
Jun
26
comment Maximum cardinality of a filtered limit of finite sets
Every set is the directed union of its finite subsets.
Jun
26
comment If questions are formalized as ideals of a boolean algebra, what kind of algebra of questions appears from Stone representation theorem?
well, the ideals of a Boolean algebra form a base for the corresponding Stone space. Next, the ideals form an algebraic directed-complete poset, or an algebraic lattice if we admit the trivial ideal. It's not realy clear what you are looking for, but these observations are fairly trivial.
Jun
23
awarded  Nice Answer
Jun
11
revised Morita equivalence for *-algebras
fix latex
Jun
5
comment Pullbacks of $C^*$-algebras
The world wide web is a big place. Does this paper have a URL?
May
28
comment Essential incompleteness via diophantine formulas?
Could the downvoter please explain what the downvote was about?