Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 7 of 7
See this page for the formulation of my problem.
Please help to find explicit formulas for exponential object, exponential transpose, and evaluation.
I am a category theory novice and have a trouble with this problem. I can’t make these formulas to coincide:
;
.
Solving this problem is a step toward proving that Fcd and Rld are cartesian closed categories. It is very important. Please help.
Your second equation doesn’t make sense.
Let’s start again. For , let be the exponential transpose (or currying) of , and let be the evaluation map. The assignment is to be a bijection
whose inverse takes to . The first equation says the composite
is an identity. The equation that says the composite
is the identity is . You should use this instead of your second equation.
Try seeing if you can establish these equations. But let me say that the cartesian closed structure on (products, exponentials, exponential transpose, evaluation map) is inherited from the cartesian closed structure of the larger category of directed graphs, where a directed graph consists of a triple . Here the category of directed graphs may be identified with the category of functors ; this is a presheaf category, where there is a well-known description of the cartesian closed structure. (If you don’t like this, then try the description given in Berci’s answer. But maybe my observation will become useful to you later, when the objects of study become more complicated.)
From Awodey’s book it follows that .
But this formula does not make sense when and are edges of a digraph, because edges are not functions.
Please help me to understand where my error is.
See also this question about my error.
Victor, I have written some things out here which gives some concrete details on what you wanted from #1, from a point of view I was hinting at in #2.
Your “here” link requires a password.
Sorry; I created the link straight out of finishing my edits. Try here instead.
1 to 7 of 7