bio | website | andrej.com |
---|---|---|
location | Ljubljana | |
age | 43 | |
visits | member for | 4 years, 9 months |
seen | 9 hours ago | |
stats | profile views | 5,968 |
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? |