beroal
Reputation
230
Next privilege 250 Rep.
 Jul 2 awarded Curious Feb 3 awarded Yearling Aug 8 awarded Popular Question Jun 21 awarded Popular Question Jul 21 comment Why is it so difficult to write complete (computer verifiable) proofs? “These linear scripts are unreadable unless replayed step-by-step in the proof assistant.” +1. Elementary tactics killed readability in Coq. Not to mention that you must learn dozens (hundreds?) little tactics. Lambda-calculus is shorter. However, advanced tactics, like “ring”, are useful. Sep 16 comment Do Arbib and Manes describe just concrete categories? @Qiaochu Yuan: Thanks, I did not know that. I have removed “ct.”. Sep 16 revised Do Arbib and Manes describe just concrete categories? “ct.” has been removed Sep 13 asked Do Arbib and Manes describe just concrete categories? Aug 28 comment What is the theory of polynomials? @Todd Trimble: BTW, Emil's answer would be great if I could understand it. :) Aug 28 comment What is the theory of polynomials? @Todd Trimble: Not so slightly. Emil does not mention any adjunction, and I do not mention atomic=positive diagrams and associative algebras. I posted my answer because I could not follow Emil's answer because of a couple of unfamiliar terms. (Never heard of atomic=positive diagrams before. Now I see they are probably related to $\eta(R)$, though do not see how until I find the precise definition.) And I gave the reference. It is always good to know your predecessors and not to reinvent the wheel. :) Aug 28 revised What is the theory of polynomials? added 10 characters in body Aug 27 awarded Teacher Aug 27 answered What is the theory of polynomials? Jul 16 comment a “self-dual” adjunction @Finn Lawler: Thanks, that is exactly what I was looking for. The power-object functor is a particular case of contravariant exponential functors. Contravariant exponential functors lead to the continuation monad. I will probably stick to MacLane's term. Jul 16 comment a “self-dual” adjunction @Finn Lawler: $I$ is a morphism between categories, i.e. a functor. Jul 14 asked a “self-dual” adjunction May 24 comment Writing “Semi-Formal” Proofs “He seemed skeptical that anyone would actually prefer symbols to English.” I prefer symbols to English. You are not alone. I write proofs for myself with Fitch diagrams. For myself because it is hard to post pictures on forums and IMHO not so many people understand that notation anyway. Feb 19 comment Why is a topology made up of 'open' sets? @Vectornaut: There is a short answer by @Mike Benfield, which goes in parallel with mine. It seems that this point of view is not popular. If you have any further info, especially rigorously developed, I will be glad to hear that. Feb 19 comment Why is a topology made up of 'open' sets? @Vectornaut: Your definition of a continuous map is a nice formalization of informal “a map without breaks” or “a map which preserves infinitesimal distances”. a touches A ↔ a is infinitely close to A. Infinitesimal distance between points does not make sense, so we need to replace one of the points with a set. That was crucial. I went the same way, but directly from the Kuratowski's axioms. a touches A ↔ $a\in cl(A)$. Thank you very much for the references because I did not know even where to start my search or what name it is called. I wonder why point-set topology is not derived this way. Feb 19 awarded Critic