camccann
Reputation
520
Top tag
Next privilege 1,000 Rep.
Create new tags
 Sep 24 awarded Autobiographer Jul 31 comment If an inequality is true for all natural numbers, is it necessarily true for all real numbers inbetween? ...except for 0. Which is excluded from some definitions of the natural numbers for murky reasons, but the question seems to assume it's included. (i.e., equating the positive reals with the ones "between the naturals") Jul 21 awarded Yearling May 17 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 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.