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 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

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 3rd 2012
   • (edited Sep 3rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexat _[[axiom of choice]]_ into the section _[In dependent type theory](http://ncatlab.org/nlab/show/axiom+of+choice#InDependentTypeTheory)_ 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 $B \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?

   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 $B \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?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 4th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe thing appearing on the right-hand side of a turnstyle $\vdash$ must always be a [[judgment]]. If we left off the $:true$ then we would have a type or a proposition, not a judgment. A proposition $P$ gives rise to a judgment "$P$ is true" which apparently someone has notated here as "$P: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 "$P$ true". Another, probably even better, option would be to say that there is a term $t$ such that $...\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 $B\to A$ and giving a section of its (-1)-truncation.

   The thing appearing on the right-hand side of a turnstyle $\vdash$ must always be a judgment. If we left off the $:true$ then we would have a type or a proposition, not a judgment. A proposition $P$ gives rise to a judgment “$P$ is true” which apparently someone has notated here as “$P: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 “$P$ true”. Another, probably even better, option would be to say that there is a term $t$ such that $...\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 $B\to A$ and giving a section of its (-1)-truncation.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 4th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexOkay, 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. ?

   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.

   ?

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 4th 2012
   • (edited Sep 4th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, but maybe I misunderstood what you were saying. You are actually disagreeing with calling > $$\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?

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

   $$\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?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 4th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> 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:A$ an element $y:B$ together with an element $z:C(x,y)$, then there is a function $f$ assigning to each $x:A$ an element $f(x):B$, and also another function $g$ assigning to each $x:A$ an element $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.

   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:A$ an element $y:B$ together with an element $z:C(x,y)$, then there is a function $f$ assigning to each $x:A$ an element $f(x):B$, and also another function $g$ assigning to each $x:A$ an element $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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 4th 2012
   • (edited Sep 4th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOh, I see. I assumed (without checking) that _you_ put [that paragraph](http://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory#AxiomOfChoice) 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeSep 4th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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](http://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html)) . 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 $n$Lab entry knows it, too.

   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 $n$Lab entry knows it, too.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 4th 2012
   • (edited Sep 4th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAfter editing it I see that what now is remark 2 [here](http://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory#AxiomOfChoice) 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.

   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.