Impact
~8k
people reached
- 0 posts edited
- 0 helpful flags
- 60 votes cast
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 |