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 bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex-geometry computable-mathematics computer-science connection constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus 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 history homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal-logic model model-category-theory monoidal monoidal-category-theory morphism motives motivic-cohomology nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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 subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 7th 2015

    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)Equiv(P, True) and Id Prop(P,True)Id_{Prop}(P, True). These types are in turn propositions, so equivalence is logical equivalence here.

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

    Is it worth having something about this on nLab?

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 7th 2015

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

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2015

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

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 7th 2015

    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?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2015

    Yep.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 8th 2015
    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2015
    • (edited Jan 8th 2015)

    So Boole speaks about the secondary proposition (Q=true)(Q = true), or does he speak about (Qtrue)(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)(Qtrue)(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?

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 8th 2015

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

    I guess the idea is that plain QQ is the same thing as (Qtrue)(Q \Leftrightarrow true) and that’s the primary proposition, and that ’it is true that QQ’ is (Q=true)(Q = true) or Id Prop(Q=true)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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2015
    • (edited Jan 8th 2015)

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

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

    P Prop˜ * P Prop \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)('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.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2015
    • (edited Jan 8th 2015)

    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.

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 9th 2015

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

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015

    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.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015

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

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 9th 2015

    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?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2015

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

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015

    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?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2015

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

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 10th 2015
    • (edited Jan 10th 2015)

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

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2015

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