Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorGuiGeek
    • CommentTimeSep 12th 2019

    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 t:Au:B[t/x](t,u):Σ(x:A).B\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.

    • CommentRowNumber2.
    • CommentAuthoratmacen
    • CommentTimeSep 12th 2019
    • (edited Sep 12th 2019)

    I guess they meant

    x:Xa:A(x)x:X(x,a): x:XA(x)\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 XX:

    t:Xa:A(t)(t,a): x:XA(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.

    • CommentRowNumber3.
    • CommentAuthorGuiGeek
    • CommentTimeSep 12th 2019

    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):Σ(n:Nat).Vectn(0,Nil):\Sigma(n:Nat).Vect\,n.

    • CommentRowNumber4.
    • CommentAuthoratmacen
    • CommentTimeSep 12th 2019

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

    Γa:AΓ,x:A,Γt:TΓ,Γ[a/x]t[a/x]:T[a/x]\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, ata \coloneqq t, AXA \coloneqq X, t(x,a)t \coloneqq (x,a), T x:XA(x)T \coloneqq \sum_{x':X}A(x')) we get:

    Γt:XΓ,x:X(x,a): x:XA(x)Γ(t,a[t/x]): x:XA(x)\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 xx need not be free in aa. (And there’s actually no reason for xx to be free in aa when you just immediately substitute, since both tt and aa are provided together. What you really want is for xx to be free in A(x)A(x), of course.)

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeSep 12th 2019

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

    • CommentRowNumber6.
    • CommentAuthoratmacen
    • CommentTimeSep 12th 2019

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

    t:Xx:Xa:A(x)(t,a[t/x]): x:XA(x)\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)A(x) generically, rather than just A(t)A(t) sounds harder, so maybe the rule is still too weak? Oh right, I guess it must be: what if XX is boolbool and A(x)A(x) is {true,false}\{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.

    • CommentRowNumber7.
    • CommentAuthoratmacen
    • CommentTimeSep 12th 2019

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

    • CommentRowNumber8.
    • CommentAuthoratmacen
    • CommentTimeSep 12th 2019
    Re #5: I edited the table include. Fixed?
    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeSep 12th 2019

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