## Not signed in

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

## Site Tag Cloud

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

• 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)$ 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$.

• 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) \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.

• 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)$, 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?

• 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 $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.

• 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'$ 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.

• 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 $El$ (“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 “$pi$” to indicate that it is an operation on terms of type $U$, 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'}(\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, $pi$ and $\pi$ should be the same. Not sure if that is a typo or a disagreement in terminology between two editors.