Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 19 of 19
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?
Hmm, why isn’t that link to this subsection of extensional type theory not working?
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.
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?
Yep.
OK, so I began propositional extensionality.
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?
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.
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.
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.
So should full univalence really have quote marks to indicate the names of types?
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.
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.
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$?
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.
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?
By “generally” I meant “if one is notating anything at all”, i.e. “if one is using Tarski universes”.
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$.
Oh, yes, $pi$ and $\pi$ should be the same. Not sure if that is a typo or a disagreement in terminology between two editors.
1 to 19 of 19