Timeline for $\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 31, 2018 at 15:12 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
the forthcoming paper forthcame
|
| Jul 13, 2013 at 21:43 | history | edited | Mike Shulman | CC BY-SA 3.0 |
added 989 characters in body
|
| Jul 13, 2013 at 20:41 | comment | added | Mike Shulman | As for the forthcoming paper, you may have to wait until it forthcomes. (-: | |
| Jul 13, 2013 at 20:40 | comment | added | Mike Shulman | Not all type formers with $\eta$ can be formulated as left adjoints. Dependent products with $\eta$ are right adjoints. Universe types certainly aren't any sort of adjoint. The natural numbers type has a left universal property, so you can probably describe it as a left adjoint to something-or-other, but not in the same way as $\Sigma$s and identities. | |
| Jul 12, 2013 at 16:41 | vote | accept | Paolo Capriotti | ||
| Jul 12, 2013 at 16:38 | comment | added | Paolo Capriotti | My question is whether this idea of "structured section" + "pullback-stability" can be formulated as a general pattern. For example, for type formers with $\eta$, it's: left adjoint + Beck-Chevalley. Is there a way to get ahold of this forthcoming paper? | |
| Jul 11, 2013 at 12:58 | history | answered | Mike Shulman | CC BY-SA 3.0 |