220 reputation
19
bio website beroal.livejournal.com
location
age
visits member for 5 years, 2 months
seen Oct 9 '12 at 21:58

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