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.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 7th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIn one of the [Bernays lectures](https://github.com/vladimirias/2014_Paul_Bernays_Lectures) Voevodsky cites Boole and continues: >“If instead of the proposition, “The sun shines,” we say, “It is true that the sun shines,” we then speak not directly of things, but of a proposition concerning things […] Every primary proposition may thus give rise to a secondary proposition, viz., to that secondary proposition which asserts its truth, or declares its falsehood.” (loc.cit., p. 38) >The equivalence of these two forms is known in type theory as propositional extensionality: P <=> ( P = True ). >It is the simplest particular case of the Univalence Axiom. The only reference we have on nLab to ''propositional extensionality" is in [extensional type theory](extensional+type+theory#propositional_extensionality), a different sense I take it. So is the idea that univalence for propositions means there is an equivalence between $Equiv(P, True)$ and $Id_{Prop}(P, True)$. These types are in turn propositions, so equivalence is logical equivalence here. Then Univalence says that $P$ is logically equivalent to True if and only if $P =$ True, and one rewrites '$P$ is logically equivalent to True' simply as $P$. Is it worth having something about this on nLab?

   In one of the Bernays lectures Voevodsky cites Boole and continues:

   “If instead of the proposition, “The sun shines,” we say, “It is true that the sun shines,” we then speak not directly of things, but of a proposition concerning things […] Every primary proposition may thus give rise to a secondary proposition, viz., to that secondary proposition which asserts its truth, or declares its falsehood.” (loc.cit., p. 38)

   The equivalence of these two forms is known in type theory as propositional extensionality: P <=> ( P = True ).

   It is the simplest particular case of the Univalence Axiom.

   The only reference we have on nLab to ”propositional extensionality” is in extensional type theory, a different sense I take it.

   So is the idea that univalence for propositions means there is an equivalence between $Equiv(P, True)$ and $Id_{Prop}(P, True)$. These types are in turn propositions, so equivalence is logical equivalence here.

   Then Univalence says that $P$ is logically equivalent to True if and only if $P =$ True, and one rewrites ’$P$ is logically equivalent to True’ simply as $P$.

   Is it worth having something about this on nLab?

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 7th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexHmm, why isn't that link to [this subsection](http://ncatlab.org/nlab/show/extensional+type+theory#propositional_extensionality) of [[extensional type theory]] not working?

   Hmm, why isn’t that link to this subsection of extensional type theory not working?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJan 7th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think there's a missing step or specialization there; propositonal extensionality really says that $(P=Q) \simeq (P\leftrightarrow Q)$. We can specialize to $Q=True$ as you're saying, but it's not obvious to me that that case implies the general one.

   I think there’s a missing step or specialization there; propositonal extensionality really says that $(P=Q) \simeq (P\leftrightarrow Q)$. We can specialize to $Q=True$ as you’re saying, but it’s not obvious to me that that case implies the general one.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 7th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI wouldn't have thought it generalized either. I guess Voevodsky was just using the Boole quote as an amusing anticipation of Univalence. But anyway, is this stably enough phrased material to go into nLab, univalence for pairs of props is propositional extensionality?

   I wouldn’t have thought it generalized either. I guess Voevodsky was just using the Boole quote as an amusing anticipation of Univalence.

   But anyway, is this stably enough phrased material to go into nLab, univalence for pairs of props is propositional extensionality?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 7th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYep.

   Yep.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 8th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOK, so I began [[propositional extensionality]].

   OK, so I began propositional extensionality.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJan 8th 2015
   • (edited Jan 8th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSo Boole speaks about the secondary proposition $(Q = true)$, or does he speak about $(Q \Leftrightarrow true)$, or does it not make a difference for Boole? What I am wondering is: I see how Bool may be seen to speak about one or both sides of the equivalence $(Q = true) \simeq (Q\Leftrightarrow true)$, but propositional extensionality concerns the equivalence sign in the middle, doesn't it, i.e. the subtle superficial difference between the left and the right sides. Is this really something that Boole considers in that quote given in the entry? Maybe in some other quote?

   So Boole speaks about the secondary proposition $(Q = true)$, or does he speak about $(Q \Leftrightarrow true)$, or does it not make a difference for Boole?

   What I am wondering is: I see how Bool may be seen to speak about one or both sides of the equivalence $(Q = true) \simeq (Q\Leftrightarrow true)$, but propositional extensionality concerns the equivalence sign in the middle, doesn’t it, i.e. the subtle superficial difference between the left and the right sides. Is this really something that Boole considers in that quote given in the entry? Maybe in some other quote?

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 8th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see your point. As mentioned in #1 this was taken from v v. I guess the idea is that plain $Q$ is the same thing as $(Q \Leftrightarrow true)$ and that's the primary proposition, and that 'it is true that $Q$' is $(Q = true)$ or $Id_{Prop}(Q = true)$, the secondary proposition. Ideally we'd have Boole saying along the lines of [Tarski's](http://en.wikipedia.org/wiki/Semantic_theory_of_truth) >material adequacy condition, also known as Convention T, holds that any viable theory of truth must entail, for every sentence P of a language, a sentence of the form (T): >(1) 'P' is true if, and only if, P.

   I see your point. As mentioned in #1 this was taken from v v.

   I guess the idea is that plain $Q$ is the same thing as $(Q \Leftrightarrow true)$ and that’s the primary proposition, and that ’it is true that $Q$’ is $(Q = true)$ or $Id_{Prop}(Q = true)$, the secondary proposition.

   Ideally we’d have Boole saying along the lines of Tarski’s

   material adequacy condition, also known as Convention T, holds that any viable theory of truth must entail, for every sentence P of a language, a sentence of the form (T):

   (1) ’P’ is true if, and only if, P.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeJan 8th 2015
   • (edited Jan 8th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOh, right, I get it: thanks for the quotation marks in the last line! :-) Namely, $'P'$ is of course the _name_ of $P$, i.e. is the term in the universe the fiber over which is $P$, $$ \array{ P &\longrightarrow& \widetilde Prop \\ \downarrow && \downarrow \\ \ast &\stackrel{'P'}{\longrightarrow}& Prop } $$ and so the left hand of our equivalence is more precisely written as $('P'='true')$ which is really the identity type of the universe. On the other hand, on the right we are speaking about the actual propositions, types, of course, not just their names. Thanks, I'll edit the entry a bit now to reflect this.

   Oh, right, I get it: thanks for the quotation marks in the last line! :-)

   Namely, $'P'$ is of course the name of $P$, i.e. is the term in the universe the fiber over which is $P$,

   $$\array{ P &\longrightarrow& \widetilde Prop \\ \downarrow && \downarrow \\ \ast &\stackrel{'P'}{\longrightarrow}& Prop }$$

   and so the left hand of our equivalence is more precisely written as

   $('P'='true')$

   which is really the identity type of the universe. On the other hand, on the right we are speaking about the actual propositions, types, of course, not just their names.

   Thanks, I’ll edit the entry a bit now to reflect this.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2015
    • (edited Jan 8th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, I have expanded a bit at _[[propositional extensionality]]_. Also added a reference that I found for the HoTT statement, although there must be more canonical references. I don't however see it discussed in the HoTT book, apart from a brief remark in the introduction.

    Okay, I have expanded a bit at propositional extensionality. Also added a reference that I found for the HoTT statement, although there must be more canonical references. I don’t however see it discussed in the HoTT book, apart from a brief remark in the introduction.

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSo should full univalence really have quote marks to indicate the names of types?

    So should full univalence really have quote marks to indicate the names of types?

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexIt's often left implicit. In Coq it's implicit, as far as I am aware. But it helped me here to see what was meant. Blame it on me being slow.

    It’s often left implicit. In Coq it’s implicit, as far as I am aware. But it helped me here to see what was meant. Blame it on me being slow.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIn type theory, rather than notating the quote marks, one generally notates instead their inverse by the name $El$ ("elements of"), and its presence or absense is referred to as "Tarski-style" or "Russell-style" universes.

    In type theory, rather than notating the quote marks, one generally notates instead their inverse by the name $El$ (“elements of”), and its presence or absense is referred to as “Tarski-style” or “Russell-style” universes.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI knew I should get round to understanding that. In the Tarski universe section [[type of types]] are the two instances of 'pi' supposed to be $\pi$ or $\Pi$?

    I knew I should get round to understanding that. In the Tarski universe section type of types are the two instances of ’pi’ supposed to be $\pi$ or $\Pi$?

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI think they were intentionally written as "$pi$" to indicate that it is an operation on terms of type $U$, as distinguished from the operation $\Pi$ on actual types.

    I think they were intentionally written as “$pi$” to indicate that it is an operation on terms of type $U$, as distinguished from the operation $\Pi$ on actual types.

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexActually I checked the type theory code linked to at [[univalence]] etc., and that does leave the distinction implicit. I think the "generally" in #13 means "in more generality one should" and not "it is general practice that". Right?

    Actually I checked the type theory code linked to at univalence etc., and that does leave the distinction implicit. I think the “generally” in #13 means “in more generality one should” and not “it is general practice that”. Right?

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexBy "generally" I meant "if one is notating anything at all", i.e. "if one is using Tarski universes".

    By “generally” I meant “if one is notating anything at all”, i.e. “if one is using Tarski universes”.

18. • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 10th 2015
    • (edited Jan 10th 2015)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #15, but why does it then go on to say $Id_{U'}(\pi'(el(a),el(b)),el(\pi(a,b)))$? That suggests $\pi$ is being used as the within universe version of $\Pi$.

    Re #15, but why does it then go on to say $Id_{U'}(\pi'(el(a),el(b)),el(\pi(a,b)))$? That suggests $\pi$ is being used as the within universe version of $\Pi$.

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOh, yes, $pi$ and $\pi$ should be the same. Not sure if that is a typo or a disagreement in terminology between two editors.

    Oh, yes, $pi$ and $\pi$ should be the same. Not sure if that is a typo or a disagreement in terminology between two editors.