bio | website | PaulTaylor.EU |
---|---|---|
location | London, UK | |
age | ||
visits | member for | 4 years, 3 months |
seen | yesterday | |
stats | profile views | 1,402 |
I am an independent researcher in the foundations of mathematics and computation, using the techniques of category theory and type theory. I wrote a book called Practical Foundations of Mathematics (CUP 1999). My main work now is Abstract Stone Duality, which seeks to axiomatise computable general topology directly, without any recourse to set theory. I am also the author of a TeX package for drawing categorical diagrams.
Mar 27 |
comment |
Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
If you look up the $\sqrt{}$ symbol in Cajori's book, you will see that it is not derived from an r. Somewhere on MO there is a fuller account of this. |
Mar 20 |
comment |
The most unexpected and/or the least natural category theory theorem?
The first proof that coproducts are derivable from the now standard axioms for an elementary topos was given by Christian Mikkelsen in 1976 in his PhD thesis under the supervision of Anders Kock in Aarhus. I forget the details but they are indeed simpler than the construction that one would obtain by unwinding Bob Pare's theorem that the contravariant powerset functor is monadic. |
Mar 2 |
comment |
Varieties where every algebra is free
Saying that the Kleisli and Eilenberg-Moore categories are equivalent is a good way of formalising the question, but what appears to be missing from it is the monad. (Actually, that suggests that some abstract category theory could be brought to bear on the question.) |
Feb 6 |
comment |
Reference request: “unoriented composition” in generalized categories
I would suggest that you describe your structure more precisely and then maybe ask the "categories" list whether anybody has seen an animal like it before, rather than asking for a list of all animals. There are models of linear logic where the morphisms don't really have sources and targets. |
Feb 6 |
comment |
Euler's mathematics in terms of modern theories?
I am of the view that the "punctiform continuum that we are used to in the post-Cantor era" was vandalism on his part and hope to see the end of his "era". So I would like to hear more of how Euler saw the continuum prior to this damage. I would also like to see the answers to your question, but the Thought Police have moved in again. |
Feb 6 |
comment |
Euler's mathematics in terms of modern theories?
"He apparently didn't think of a line segment as a point set." Sounds good, please tell us more. |
Feb 5 |
revised |
Coequalizers in the category of algebras of the double power locale monad
added 2112 characters in body |
Feb 5 |
revised |
Coequalizers in the category of algebras of the double power locale monad
added 250 characters in body |
Feb 3 |
revised |
Cartesian closed category
gave the counterexample as requested |
Feb 2 |
answered | Cartesian closed category |
Jan 30 |
answered | Coequalizers in the category of algebras of the double power locale monad |
Jan 30 |
comment |
Coequalizers in the category of algebras of the double power locale monad
As the "Related" sidebar suggests, this question is about the same topic. |
Dec 21 |
awarded | Yearling |
Dec 7 |
comment |
What's a nice argument that shows the volume of the unit ball in $\mathbb R^n$ approaches 0?
One can get the exact result with school calculus, so surely the challenge is to avoid using even that and it is a pity that you refer to "the unit ball of $\ell_1^n$". We could equivalently consider the principal $2^n$-ant of the ball, whose tangent hyperplane normal to the body diagonal has equation $\sum x_i=\sqrt{n}$. This meets each axis at distance $\sqrt{n}$ and has volume $n^{n/2}/n ! $. |
Nov 27 |
revised |
Well founded induction attributed to Noether
replied to Joel on which rule is preferable |
Nov 26 |
revised |
Well founded induction attributed to Noether
commented on the history |
Nov 24 |
comment |
Well founded induction attributed to Noether
Anyway, the point of the question was whether Noether (whom I always thought of as an algebraist) identified this as a general principle of logic. |
Nov 24 |
comment |
Well founded induction attributed to Noether
As a constructivist, I insist that any well founded relation is necessarily irreflexive, whilst I write $\subset$ and not $\subseteq$ for (reflexive) inclusion of sets etc. |
Nov 24 |
revised |
Well founded induction attributed to Noether
added missing quantification of $y$ |
Nov 24 |
awarded | Student |