Timeline for Does the "coproduct-elimination transform" have an accepted name, and where can I learn more about it?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 26, 2020 at 2:36 | comment | added | Ptharien's Flame | This transformation is also related, by way of propositions-as-types/Curry-Howard, to the DeMorgan laws of propositional logics, and for similar reasons to “continuation passing”. | |
| Jul 25, 2020 at 14:18 | comment | added | Paul Taylor | $D Y$ above should of course have been $T Y$. Also, Kock wrote $[X\pitchfork Y]$ for the internal hom more recognisably called $[X\to Y]$. | |
| Jul 25, 2020 at 13:19 | comment | added | Paul Taylor | That is the version of "strength" that is commonly seen in the CS literature, especially since Eugenio Moggi's work. Kock investigated other forms, of which I suspect the original one was that the action of the functor on hom-sets $T:C(X,Y)\to D(T X,D Y)$ extends to internal homs $[X\to Y]\to[T X\to T Y]$ or $Y^X\to (T Y)^{(T X)}$. Kock did this for monoidal-closed categories; it's hardly worth mentioning for CCCs. His webpage is users-math.au.dk/kock | |
| Jul 25, 2020 at 10:07 | comment | added | goblin GONE | @PaulTaylor, honestly I don't quite see the connection with functorial strengths. As I understand it, a strength allows you to take something outside a functor's arguments, and put it inside the arguments. Like so: $X \times FY \rightarrow F(X \times Y)$. But I can't really see the connection to what I'm asking.... | |
| Jul 25, 2020 at 8:43 | comment | added | Paul Taylor | This looks like one of the many manifestations of "strength" of a functor, which was first investigated by Anders Kock. As for a name, strong/strength are words that have been vastly over-used already. Look up Kock's work, but just describe your construction as what it does - don't give it a confusing name. | |
| Jul 25, 2020 at 5:46 | history | edited | goblin GONE | CC BY-SA 4.0 |
added 70 characters in body
|
| Jul 25, 2020 at 3:42 | history | edited | goblin GONE | CC BY-SA 4.0 |
added 426 characters in body
|
| Jul 25, 2020 at 3:25 | history | edited | goblin GONE | CC BY-SA 4.0 |
deleted 111 characters in body
|
| Jul 25, 2020 at 1:58 | history | asked | goblin GONE | CC BY-SA 4.0 |