Timeline for Adjoining an arrow to a CCC
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 15, 2013 at 1:21 | vote | accept | tsctsc | ||
| Jul 15, 2013 at 1:21 | comment | added | tsctsc | I'm starting to read that part. Thanks! | |
| Jul 14, 2013 at 22:54 | comment | added | Todd Trimble | Okay, I now see what you're referring to. Courtesy of Google books, I'm looking now at page 57, the first paragraph of section 5. It seems they really botched the first description badly. My advice would be to ignore that bit you copied into 1., and read on. You can see from subsequent text that they really mean for the inclusion of $A$ into $A[x]$ to preserve ccc structure strictly. You will see the "linguistic" construction of $A[x]$, and the conceptual Kleisli construction which is the basis for their functional completeness, and which I think you will find pretty. | |
| Jul 14, 2013 at 22:26 | comment | added | tsctsc | How does the construction 1 can have such functor $i$? When they define the construction of a free cartesian closed category over a graph, they add new objects for products, exponentials, and terminal. How can you have $i(A^B) = i(A)^{i(B)}$? | |
| Jul 14, 2013 at 21:35 | history | answered | Todd Trimble | CC BY-SA 3.0 |