Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorGuiGeek
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: GuiGeek
   Format: MarkdownItexIn the page [[dependent sum type]], the presented "term introduction rule" seems not really dependent, since the typing derivation of the second element is not aware of the first. I would expect $\frac{\vdash t:A\quad \vdash u:B[t/x]}{\vdash (t,u):\Sigma(x:A).B}$ which corresponds to what is presented in the text on positive and negative versions.

   In the page dependent sum type, the presented “term introduction rule” seems not really dependent, since the typing derivation of the second element is not aware of the first. I would expect $\frac{\vdash t:A\quad \vdash u:B[t/x]}{\vdash (t,u):\Sigma(x:A).B}$ which corresponds to what is presented in the text on positive and negative versions.

2. • CommentRowNumber2.
   • CommentAuthoratmacen
   • CommentTimeSep 12th 2019
   • (edited Sep 12th 2019)
   • PermaLink
   Author: atmacen
   Format: MarkdownItexI guess they meant $$\frac{x:X \vdash a:A(x)}{x:X \vdash (x,a) : \sum_{x':X}A(x')}$$ which I think is basically the right idea. But that's not the usual rule either, since it doesn't allow you to construct pairs in the empty context, unless you have a primitive substitution rule. So the usual rule uses an arbitrary term of $X$: $$\frac{t:X \qquad a:A(t)}{(t,a) : \sum_{x:X}A(x)}$$ This is the same as what you wrote, but with different notation.

   I guess they meant

   $$\frac{x:X \vdash a:A(x)}{x:X \vdash (x,a) : \sum_{x':X}A(x')}$$

   which I think is basically the right idea. But that’s not the usual rule either, since it doesn’t allow you to construct pairs in the empty context, unless you have a primitive substitution rule.

   So the usual rule uses an arbitrary term of $X$:

   $$\frac{t:X \qquad a:A(t)}{(t,a) : \sum_{x:X}A(x)}$$

   This is the same as what you wrote, but with different notation.

3. • CommentRowNumber3.
   • CommentAuthorGuiGeek
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: GuiGeek
   Format: MarkdownItexBut what they meant looks wrong to me, since it does not allow to introduce any pair which first element is not a variable, for instance to prove $(0,Nil):\Sigma(n:Nat).Vect\,n$.

   But what they meant looks wrong to me, since it does not allow to introduce any pair which first element is not a variable, for instance to prove $(0,Nil):\Sigma(n:Nat).Vect\,n$.

4. • CommentRowNumber4.
   • CommentAuthoratmacen
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: atmacen
   Format: MarkdownItexRight, that's why you'd need a substitution rule: $$\frac{\Gamma \vdash a\,:\,A \qquad \Gamma,x:A,\Gamma' \vdash t\,:\,T}{\Gamma,\Gamma'[a/x] \vdash t[a/x]\,:\,T[a/x]}$$ So combining this with the variables-only pairing rule ($\Gamma' \coloneqq \cdot$, $a \coloneqq t$, $A \coloneqq X$, $t \coloneqq (x,a)$, $T \coloneqq \sum_{x':X}A(x')$) we get: $$\frac{\Gamma \vdash t\,:\,X \qquad \Gamma,x:X \vdash (x,a)\,:\,\sum_{x':X}A(x')}{\Gamma \vdash (t,a[t/x])\,:\,\sum_{x':X}A(x')}$$ This is sufficiently general, since $x$ need not be free in $a$. (And there's actually no reason for $x$ to be free in $a$ when you just immediately substitute, since both $t$ and $a$ are provided together. What you really want is for $x$ to be free in $A(x)$, of course.)

   Right, that’s why you’d need a substitution rule:

   $$\frac{\Gamma \vdash a\,:\,A \qquad \Gamma,x:A,\Gamma' \vdash t\,:\,T}{\Gamma,\Gamma'[a/x] \vdash t[a/x]\,:\,T[a/x]}$$

   So combining this with the variables-only pairing rule ($\Gamma' \coloneqq \cdot$, $a \coloneqq t$, $A \coloneqq X$, $t \coloneqq (x,a)$, $T \coloneqq \sum_{x':X}A(x')$) we get:

   $$\frac{\Gamma \vdash t\,:\,X \qquad \Gamma,x:X \vdash (x,a)\,:\,\sum_{x':X}A(x')}{\Gamma \vdash (t,a[t/x])\,:\,\sum_{x':X}A(x')}$$

   This is sufficiently general, since $x$ need not be free in $a$. (And there’s actually no reason for $x$ to be free in $a$ when you just immediately substitute, since both $t$ and $a$ are provided together. What you really want is for $x$ to be free in $A(x)$, of course.)

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think we should give the usual rule, as in #2. Anyone who wants to fix it, please do!

   I think we should give the usual rule, as in #2. Anyone who wants to fix it, please do!

6. • CommentRowNumber6.
   • CommentAuthoratmacen
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: atmacen
   Format: MarkdownItexNow I'm not sure anymore. The argument I gave justifies: $$\frac{t:X \qquad x:X \vdash a\,:\,A(x)}{(t,a[t/x])\,:\,\sum_{x':X}A(x')}$$ But having to prove $A(x)$ generically, rather than just $A(t)$ sounds harder, so maybe the rule is still too weak? Oh right, I guess it must be: what if $X$ is $bool$ and $A(x)$ is $\{true \mapsto \top,\;false \mapsto \bot\}$? Yeah OK, it looks like requiring a variable was a red herring; the problem was that the premise isn't depending on a specific term, like GuiGeek originally said.

   Now I’m not sure anymore. The argument I gave justifies:

   $$\frac{t:X \qquad x:X \vdash a\,:\,A(x)}{(t,a[t/x])\,:\,\sum_{x':X}A(x')}$$

   But having to prove $A(x)$ generically, rather than just $A(t)$ sounds harder, so maybe the rule is still too weak? Oh right, I guess it must be: what if $X$ is $bool$ and $A(x)$ is $\{true \mapsto \top,\;false \mapsto \bot\}$?

   Yeah OK, it looks like requiring a variable was a red herring; the problem was that the premise isn’t depending on a specific term, like GuiGeek originally said.

7. • CommentRowNumber7.
   • CommentAuthoratmacen
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: atmacen
   Format: MarkdownItexSo the diagram next to the bad intro rule seems misleading: that $x$ arrow doesn't have to be a context projection.

   So the diagram next to the bad intro rule seems misleading: that $x$ arrow doesn’t have to be a context projection.

8. • CommentRowNumber8.
   • CommentAuthoratmacen
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: atmacen
   Format: TextRe #5: I edited the table include. Fixed?

   Re #5: I edited the table include. Fixed?
9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeSep 12th 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, looks good. Thanks for catching this, GuiGeek, and for fixing it, Matt!

   Yes, looks good. Thanks for catching this, GuiGeek, and for fixing it, Matt!