Timeline for Dependent sum/product and the base-change functor adjunctions
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 14, 2023 at 11:44 | comment | added | varkor | are multiple ways to represent a single term. Working over a slice is one way to capture the dependency structure, but it is not necessary to do so. Dependency can be captured instead by working in the original category, and identifying dependencies by projecting out of pullbacks. (I feel this comment is probably not very clear, and I really need more space to make it clear.) Perhaps this is a conversation that could be had elsewhere, without MO's limitations, though. (2/2) | |
| May 14, 2023 at 11:36 | comment | added | varkor | To be honest, I think that it is difficult to have this sort of technical discussion in the comments section of MO, and the character limit is going to make it easy to cause undue confusion. Since Andrej Bauer's answer has clarified OP's question, it also doesn't seem so worthwhile to modify mine further; it may be simpler to delete my answer. My general impression, though, is that we are interpreting the semantics of a term in a dependent type theory differently: since categories with finite limits have a lot of redundancy in a certain sense (as some morphisms determine others), there (1/2) | |
| May 14, 2023 at 9:49 | comment | added | daniel gratzer | I'm having some trouble type-checking this comment. I assumed $A$ was a type in context $\Gamma$, in which case $\Gamma \vdash t : A$ (and $t$ has type $A$ not $B$ above I think) would need to be formulated in the slice over $\Gamma$. If instead $A$ is closed then this isn't necessary. However, I'm having trouble understanding your comment regarding $s$ which seems distinct from the above? It appears that $s$ is meant to be an element of $B(t)$ where $\Gamma \vdash t : A$ and $A$ is a closed type, is that correct? | |
| May 11, 2023 at 15:33 | history | edited | varkor | CC BY-SA 4.0 |
added 260 characters in body
|
| May 10, 2023 at 14:32 | comment | added | varkor | My understanding is that, if $a : A \vdash B(a)\ \mathrm{type}$, then a term $\Gamma \vdash s : B$ can be represented either as a morphism $\Gamma \to B$ in $\mathscr C$ or as a morphism $\Gamma \to \Gamma \times_A B$ in $\mathscr C/\Gamma$, but the two are equivalent by the universal property of the pullback. I agree with the other points, though. | |
| May 10, 2023 at 14:28 | history | rollback | varkor |
Rollback to Revision 1
|
|
| May 10, 2023 at 14:17 | history | edited | varkor | CC BY-SA 4.0 |
added 287 characters in body; added 8 characters in body
|
| May 10, 2023 at 13:51 | comment | added | daniel gratzer | Note that $t$ should be a morphism in the slice category over $\Gamma$ to represent a term. And, just to put a fine point on it, in the model of type theory in a locally Cartesian closed category, every morphism $f : X \to Y$ is a display map and therefore should be interpreted as a type in $Y$ such that the extension of $Y$ by this type is precisely $X$. The right adjoint $f_*$ then corresponds to taking a dependent product over this type. | |
| May 10, 2023 at 12:55 | history | answered | varkor | CC BY-SA 4.0 |