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 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 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 nforum 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 sheaves 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.
    • CommentAuthorUrs
    • CommentTimeSep 3rd 2012
    • (edited Sep 3rd 2012)

    at axiom of choice into the section In dependent type theory I have moved the explicit statement taken from the entry of dependent type theory (see there for what I am talking about in the following).

    One technical question: do we need the

      : true

    at the very end of the formal statement of the theorem?

    One conceptual question: I feel inclined to add the following Remark to that, on how to think about the fact that the axiom of choice is always true in this sense in type theory. But please let me know what you think:

    Heuristically, the reason that the axiom of choice is always true when formulated internally this way in dependent type theory is due to the fact that its assumption thereby is stated in constructive mathematics:

    Stated in informal but internal logic, the axiom of choice says:

    If BAB \to A is a map all whose fibers are inhabited, then there is a section.

    But now if we interpret the assumption clause

    a map all whose fibers are inhabited

    constructively, we have to provide a constructive proof that indeed the fibers are inhabited. But such a constructive proof is a choice of section.

    So constructively and internally the axiom is reduced to “If there is a section then there is a section.” And so indeed this is always true.

    Would you agree that this captures the state of affairs?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2012

    The thing appearing on the right-hand side of a turnstyle \vdash must always be a judgment. If we left off the :true:true then we would have a type or a proposition, not a judgment. A proposition PP gives rise to a judgment “PP is true” which apparently someone has notated here as “P:trueP:true”. I’ve never seen that notation elsewhere – it seems odd since “true” is not a type to which “P” belongs; instead I’ve seen that judgment written as “PP true”. Another, probably even better, option would be to say that there is a term tt such that ...t:P...\vdash t:P.

    Your Remark is probably something that constructivists who believe in calling this “a proof of the axiom of choice” would agree with. But I am not such a constructivist, and I disagree with it. To me, it is perfectly possible to give a constructive proof that the fibers are all inhabited without giving a section. It is the difference between giving a section of BAB\to A and giving a section of its (-1)-truncation.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2012

    Okay, so how would you say in words what is going on in that “type-theoretic proof of the axiom of choice”?

    A map that has a section of its (-1)-truncation also has a section itself.


    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2012
    • (edited Sep 4th 2012)

    Hm, but maybe I misunderstood what you were saying. You are actually disagreeing with calling

    Γ(x:A)(y:B(x))C(x,y)(f:(Πx:A)B(x))(x:A)C(x,apply(f,x))true\Gamma \vdash (\forall x : A) (\exists y : B(x)) C(x, y) \to (\exists f : (\Pi x : A)B(x) )(\forall x : A) C(x, \mathrm{apply}(f, x)) \; \mathrm{true}

    a statement of an axiom of choice, right?

    And there is no (-1)-truncation in this statement, actually, you were just referrring to my use of the word “inhabited”, which, I guess, you would demand to see for something that actually deserves to be called a statement of the axiom of choice. Is that right?

    Finally, while, therefore, my heuristics about proving “if there is a section then there is a section” would therefore not apply to a statement that actually involves a (-1)-truncation, it does capture what the above formal expression actually expresses, right?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2012

    You are actually disagreeing with calling […] a statement of an axiom of choice, right?

    Yes. I would state that theorem as “if there is a function assigning to each x:Ax:A an element y:By:B together with an element z:C(x,y)z:C(x,y), then there is a function ff assigning to each x:Ax:A an element f(x):Bf(x):B, and also another function gg assigning to each x:Ax:A an element g(x):C(x,f(x))g(x):C(x,f(x)). It’s basically the statement that a (dependent) function with two outputs (one dependent on the other) can be broken apart into two (dependent) functions with one ouput each (with the type of the second involving the first). Useful, certainly, but I think calling it “the axiom of choice” is an insult to the deep mathematics surrounding the latter.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2012
    • (edited Sep 4th 2012)

    Oh, I see. I assumed (without checking) that you put that paragraph into the entry Martin-Löf dependent type theory. This has been there for ages. I was staring at it and trying to understand the terminology. That’s where my question above arises from.

    Okay, so then I now remove again the copy of that discussion which I had moved to “axiom of choice” and you please see if you find a minute to do something about the paragraph in the Martin-Löf dependent type theory entry.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2012

    I have googled around a bit:

    the interpretation of that statement as an internal axiom of choice is promoted on this page here:

    • John Bell, The Axiom of choice in type theory, Stanford Encyclopedia of philosophy, 2008 (web) .

    It seems that Bell is referring to some text

    • Tait, 1994

    for that formulation of the axiom of choice, the one that you are objecting to. He calls it the “logical form of the axiom of choice”, abbreviated ACL.

    Well, you may know all this. But eventually we need to make sure that the reader of the nnLab entry knows it, too.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2012
    • (edited Sep 4th 2012)

    After editing it I see that what now is remark 2 here refers to this issue. I didn’t even see that remark before. Somehow I find it a bit vague, because the discussion seems to be mixing the informal question of what deserves to be called the axiom of choice with other formal matters.

    But all right, I leave this the way it is now, need to be doing something else.