Timeline for Dependent sum/product and the base-change functor adjunctions
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 14, 2023 at 7:11 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 1 character in body
|
| May 12, 2023 at 16:12 | vote | accept | Bartosz Milewski | ||
| May 11, 2023 at 21:21 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 56 characters in body
|
| May 11, 2023 at 19:39 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 23 characters in body
|
| May 11, 2023 at 19:38 | comment | added | Andrej Bauer | Yes, the type-theoretic sum and product are both adjoint to $p_A$, so that's actually the only pullback you care about. However, in sets every $f : X \to Y$ is isomorphic to some such $p_A$, so at least there considering products and sums adjoint to $p_A^*$ is not really less general than considering products and sums adjoint to $f^*$ for a general $f$. | |
| May 11, 2023 at 17:26 | comment | added | Bartosz Milewski | @AndrejBauer: So am I to understand that the type-theoretic dependent sum/product is just a special case of $f = \sigma = p_A$? BTW, thanks for the link to your notes. It looks like a real treasure trove of information linking math to programming. | |
| May 11, 2023 at 16:24 | comment | added | Andrej Bauer | I spelled out the set-theoretic interpretation using display maps. You can read about the (more reasonable) set-theoretic interpretation in terms of families in my notes, linked to in the answer. | |
| May 11, 2023 at 16:23 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 1809 characters in body
|
| May 11, 2023 at 15:31 | comment | added | varkor | @BartoszMilewski: you can view $\iota$ here as the projection function $\pi_1$ from a pullback. The empty context can be interpreted as a singleton set. | |
| May 11, 2023 at 10:52 | comment | added | Bartosz Milewski | I guess my problem is that I'm used to thinking of types as bona fide sets and terms as functions (closures). Bigger context means bigger set (a product of more sets). But your $\iota$ or my $f$ is not a function, is it? And an empty context (terminal object) is not a singleton? | |
| May 11, 2023 at 6:48 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
edited body
|
| May 10, 2023 at 21:38 | history | answered | Andrej Bauer | CC BY-SA 4.0 |