meta user
network profile
| bio | website | |
|---|---|---|
| location | trapped in an IO monad, send help | |
| age | 30 | |
| visits | member for | 2 years, 9 months |
| seen | yesterday | |
| stats | profile views | 55 |
camccann :: (Coffee a) => [a] -> IO Software
Entia non sunt multiplicanda praeter necessitatem.
|
1d |
comment |
Is “cofunctor” an accepted term for contravariant functors? I think "covariant" is the outlier here, and is using the co- prefix differently. "Contrafunctor" appears to be a contraction of "contravariant functor" and isn't used by mathematicians that I'm aware of. At any rate, there isn't necessarily a tidy duality here, because to make sense of arrows being "flipped" requires a context establishing a preferred direction for arrows, which a functor in full generality doesn't have. |
|
May 7 |
comment |
A natural example in category theory Does the requirement given include the case where $Y$ is $X$ and the morphism $X \to Y$ is the identity, or must they be distinct? |
|
May 6 |
awarded | Caucus |
|
Apr 30 |
comment |
distribution of categorical product (conjunction) over coproduct (disjunction) The canonical morphism is so named because it follows directly from the definitions of the product and coproduct, so it doesn't really tell you anything about its inverse (which may not exist). |
|
Apr 30 |
comment |
distribution of categorical product (conjunction) over coproduct (disjunction) Dually, $(A \times B) + C \to (A + C \times B + C)$ always exists as well. Going in the other direction is where things get trickier. |
|
Apr 30 |
comment |
distribution of categorical product (conjunction) over coproduct (disjunction) @JoshuaTaylor: If you're working in an intuitionistic setting, quite a few tools along these lines already exist in the context of typed lambda calculi--e.g., the proof in your question can be read off directly as a lambda term whose type is the formula being proved, and a program that can convert it to use only function composition and application exists (and is used largely to entertain other programmers). |
|
Apr 30 |
comment |
distribution of categorical product (conjunction) over coproduct (disjunction) @JoshuaTaylor: The definition of a monoidal closed category includes that currying is a bijection, so it isn't actually necessary to derive that. I believe it's also possible to derive both directions using only the eval arrow and without relying on the product projections. This is all pretty easy to reconstruct in a cartesian closed category, though. |
|
Apr 30 |
awarded | Editor |
|
Apr 30 |
revised |
distribution of categorical product (conjunction) over coproduct (disjunction) added 501 characters in body |
|
Apr 30 |
answered | distribution of categorical product (conjunction) over coproduct (disjunction) |
|
Apr 25 |
comment |
Given a functor between categories, how to denote a morphism between particular objects of that category @smartcaveman: Morphisms can be just about anything depending on the category. There's no reason in general for a mapping from one object to another to have anything to do with the morphisms of the category they live in. |
|
Apr 25 |
comment |
Given a functor between categories, how to denote a morphism between particular objects of that category @smartcaveman: So in general, you're talking about relating a functor between two categories with morphisms in a third category that contains all the objects of the other two? |
|
Apr 25 |
comment |
Given a functor between categories, how to denote a morphism between particular objects of that category @smartcaveman: So in that case, $C_1$ and $C_2$ are distinct categories whose objects are also categories, right? |
|
Apr 22 |
answered | evaluate the lambda expression call by value |
|
Apr 2 |
comment |
Why should the taxpayer pay the mathematician? Who are you to say what will always and forever remain useless? People might once have said the same about number theory, yet today it's hard to think of any mathematics more directly useful, needing not even a detour via physics or engineering. |
|
Apr 1 |
comment |
Why is propositional logic not Turing complete? @Hypercube: I mean circuits where an input to a gate can logically depend on its own output. For example, flip-flops implement simple memory cells using feedback loops. |
|
Apr 1 |
answered | Why is propositional logic not Turing complete? |
|
Jan 7 |
comment |
Natural numbers as types. A 0-tuple or record with no fields, i.e. an empty product type, are also common ways to describe the unit type. And of course an uninhabited type is 0. |
|
Dec 28 |
comment |
What is the practical difference between a differential and a derivative? In the version of that joke I originally heard, the second "problem" had the faucet already running and making a mess, which the mathematician reduces to a solved problem by (of course) setting the trash on fire. |
|
Dec 28 |
comment |
A new imaginary number? $x^c = -x$ Hm. Seems to me you only lose that rule about exponents half the time--if you preserve parity of the number of c exponents it should work, I think? Note that introducing an extra factor of 1^c would always suffice. You still end up with x^2c == x^2, of course, which seems peculiar. It's sort of a hypernegative unit, that constructs the inverse of two hyperoperations down, like -1 does one hyperoperation down. Unfortunately, multiplying by c doesn't give you the predecessor operation... |
