1,625 reputation
616
bio website PaulTaylor.EU
location London, UK
age
visits member for 4 years, 3 months
seen yesterday
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