# Andrej Bauer

 12,511 Reputation 4246 views

## Registered User

 Name Andrej Bauer Member for 3 years Seen 7 hours ago Website Location Ljubljana Age 42
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.
 9h comment In what rigorous sense are Sperner’s Lemma and the Brouwer Fixed Point Theorem equivalent?In this particular case a general topos would work to show that they are not equivalent. But in general, when discussing equivalence of statements $A$ and $B$, we have to do it in a context where not both of them are provable (or refutable), lest they are "lost in the background theory". The idea is to a fragment of mathematics that is just strong enough to express the statements. See François's answer, where he identifies the relevant weak logical setting for Spenne'r Lemma and Brouwer's fixed point theorem. 1d accepted Lawvere’s fixed point theorem and the Recursion Theorem 1d comment Lawvere’s fixed point theorem and the Recursion TheoremA special case of Lavwere's fixed point theorem is a special case of Recursion theorem. 2d revised Lawvere’s fixed point theorem and the Recursion Theoremadded 213 characters in body 2d revised Lawvere’s fixed point theorem and the Recursion Theoremadded 86 characters in body; deleted 1 characters in body; deleted 4 characters in body 2d comment Lawvere’s fixed point theorem and the Recursion TheoremThat's an answer for logicians, yes. Are we all logicians here? I can be. 2d answered Lawvere’s fixed point theorem and the Recursion Theorem May19 comment Importance of separability vs. second-countabilityAnd this would be Paul Taylor: paultaylor.eu The photo is a bit blurry, but that's how I percieve Paul most of the time anyway. May19 comment Importance of separability vs. second-countabilityOvertness is exactly as complicated as compactness. nLab has a bit written about it: ncatlab.org/nlab/show/overt+space May19 comment Importance of separability vs. second-countabilityThis might not be the right decade to make this comment, but separability seems to be just the poor man's version of overtness, something Paul Taylor has been pointing out. If this is indeed the case, then separability would indeed be a suboptimal notion. May15 comment On the large cardinals foundations of categories@Michal: It is a joke of course, but what you seem to worry about is how many jokes it is. Well, the thing to notice is that it is a sequence, not a series. May15 comment On the large cardinals foundations of categories@Asaf: perhaps this may help. The universes are typically taken to be such that $\mathcal{U}_i$ is an element of $\mathcal{U}_{i+1}$. Cummulativity means that $\mathcal{U}_i$ is also a subtype (subset in your parlance) of $\mathcal{U}_{i+1}$. So we can obviously distinguish them because each contains something that another does not. May15 comment On the large cardinals foundations of categories@Asaf: the notion of a universe in type theory is quite flexible. It's good if the universe is closed under many operations, perhaps so many that it forms a small model of type theory, but it doesn't have to. Actually, I am not sure what you're getting at. What does "distinguish between them" mean? May14 comment On the large cardinals foundations of categoriesThe nice embedding is guaranteed by universe cummulativity. By the way, the entire Coq standard library fits into three or four universes. May14 answered On the large cardinals foundations of categories May9 awarded ● Good Answer May9 comment A question in category theoryThe modern version is: tell me who your Facebook friends are and I will tell you not only who you are, but also how you use your credit cards. May9 comment A question in category theoryLet's be honest here: category theorists are their own friends, which is why the slogan works. May9 comment Is rigour just a ritual that most mathematicians wish to get rid of if they could? We are not machines. Not. Damn you Freud! May9 comment Is rigour just a ritual that most mathematicians wish to get rid of if they could? This answer hit the nail on its head. We are machines, we trust other people, and prefer to hear what ideas they have than why they think those ideas might be true. May9 awarded ● Nice Answer May8 revised Is rigour just a ritual that most mathematicians wish to get rid of if they could? added 240 characters in body; deleted 6 characters in body May8 revised Is rigour just a ritual that most mathematicians wish to get rid of if they could? added 208 characters in body; added 39 characters in body May8 answered Is rigour just a ritual that most mathematicians wish to get rid of if they could? May7 awarded ● Nice Answer May6 comment Definition of subobject classifier in presheavesSteve says the first edition has a rather unfortunate number of typos. May6 revised Definition of subobject classifier in presheavesedited title May6 answered Definition of subobject classifier in presheaves May5 answered Useful tricks in experimental mathematics Apr28 comment Is there any nontrivial monad on the category of graphs?I think this proves I am very smart. Had I been doing things randomly, at least some of these would be actual examples. It takes a special talent to produce four plausibly-sounding non-examples. Apr26 comment Can nonstandard analysis be used to prove results in constructive or computable analysis?Sam says he is going to give an answer in "due time", whatever that means. Apr26 comment Can nonstandard analysis be used to prove results in constructive or computable analysis?It think Sam Sanders is the expert on this question, I'll alert him to its existence. Apr25 comment Connection between codata and greatest fixed pointsI don't know what they mean. When I wrote my PhD dissertation I meant "greatest fixed-point in the complete lattice of partial equivalence relations on a partial combinatory algebra". So I did apply Tarski's theorem to a complete lattice. But I do not know how to do it just for sets. Apr25 comment A Model where Dedekind Reals and Cauchy Reals are DifferentWell, I'd be delighted to see a difference between Cauchy and Dedekind reals which originates from making classical mathematics so weak that even excluded middle cannot rescue the coincidence of reals. Apr24 awarded ● Nice Answer Apr24 comment A Model where Dedekind Reals and Cauchy Reals are DifferentI'll let the expert in the room figure out how many powersets I consumed :-) Apr24 comment A Model where Dedekind Reals and Cauchy Reals are DifferentWhat is this "background"? The meta-matheamtical level which I am using to answer the question, or the formal system of which we are considering the models? I was taking about meta-mathematical level, which in my answer is something that suffices to build categories of sheaves. In any case, the original question does not specify any formal system or anything like that. Therefore, the answers should not focus on formal system. They should explain the ideas, either through topological considerations (continuous vs. locally constant), or computability considerations (am looking forward to). Apr24 comment A Model where Dedekind Reals and Cauchy Reals are DifferentI am not particularly amused when a "background theory" is imposed on an informal argument which I make. It is the logicians' wishful thinking that informal mathematics stands on formal mathematics. But since you raised the issue, possible backgrounds for my answer could be ZFC, IZF, ETCS, IHOL, BZ, or HOTT. Take your pick. Apr24 answered Can Inequivalent Topologies Have Same Sheaves/Cohomology? Apr24 answered A Model where Dedekind Reals and Cauchy Reals are Different Apr23 comment Connection between codata and greatest fixed pointsActually, I think the cool and correct way to do codata is to use set theory with antifoundation. See Barwise's book "Vicious Circles", books.google.si/… Apr22 comment Connection between codata and greatest fixed pointsWell, if you only care abut the carrier sets, you could look at greatest fixed points, I suppose. I will write another answer. Apr22 answered Connection between codata and greatest fixed points Apr19 revised Is there any nontrivial monad on the category of graphs?deleted 252 characters in body Apr18 comment Is there any nontrivial monad on the category of graphs?But surely, there are billions and billions of them. Apr18 comment Is there any nontrivial monad on the category of graphs?Ugh, maybe I should just delete the answer. Apr18 revised Is there any nontrivial monad on the category of graphs?added 70 characters in body Apr18 comment Is there any nontrivial monad on the category of graphs?Oops, that would be a comonad then. Thanks! Apr18 answered Is there any nontrivial monad on the category of graphs? Apr14 comment Does “induction” for a functor algebra imply it is initial?@Bruce Westbury: no.