Timeline for What are the equational laws for zero types?
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2011 at 10:27 | comment | added | Ohad Kammar | regarding edit 2: Left adjoints preserve colimits. If the category is Cartesian closed, then $(-)\times C$ is left adjoint to $(-)^C$ so $(A+B)\times C$ is the sum $A\times C + B\times C$. | |
| Jul 28, 2011 at 7:31 | history | edited | Neel Krishnaswami | CC BY-SA 3.0 |
added 304 characters in body
|
| Jul 4, 2011 at 14:04 | vote | accept | Ohad Kammar | ||
| Jul 3, 2011 at 21:24 | vote | accept | Ohad Kammar | ||
| Jul 4, 2011 at 14:04 | |||||
| Jul 3, 2011 at 21:24 | comment | added | Ohad Kammar | Aha! Thanks for that proof! And for the patience, too! | |
| Jul 3, 2011 at 14:35 | history | edited | Neel Krishnaswami | CC BY-SA 3.0 |
added explanation of equality of elements of 0 type
|
| Jul 1, 2011 at 17:03 | comment | added | Ohad Kammar | I don't follow. The distributivity amounts to $initial : 0 \to A\times 0$ having an inverse. Why does that imply that $0$ is subterminal? | |
| Jul 1, 2011 at 16:36 | comment | added | Neel Krishnaswami | Yes: the fact that the STLC with sums needs a distributive bi-CCC ($(X \times A) + (X \times B) \simeq X \times (A+B)$) to interpret it, and the uniqueness for the 0 type comes as the nullary version of that. (Try to write down the interpretation of the elimination rule for sums, and you'll see it.) | |
| Jul 1, 2011 at 16:14 | comment | added | Ohad Kammar | Regarding 1: I think of a zero type as an initial object. Initial objects may have multiple arrows into them, but can only have one arrow out of them. In other words, I don't immediately see any reason why being bi-CCC implies 0 to be subterminal. Is there one? | |
| Jul 1, 2011 at 16:01 | history | answered | Neel Krishnaswami | CC BY-SA 3.0 |