Certainly a proposition is a type, which as such partakes in judgements. But it’s a type of the obtaining of a state of affairs. There’s a proposition as type, what it means to be inhabited, and the judgement as to it’s being inhabited.
As a type, a proposition has at most one element, or in other words any two elements are identified.
A subterminal object, a monomorphism to the terminal object, in the slice topos, $\mathbf{H}/W$ is a subobject of $W$. So if $W$ is a set of worlds, then a proposition is a subset of worlds.
True is an abstract proposition, a name for the unit type $\mathbf{1}$ (HoTT book, p. 41). So when we say ‘$P$ is true’, this is to state an identity of types. In the context of propositional extensionality, ‘$P$ is true’ means $P$= True: Type, and so by the univalence axiom $P \simeq \mathbf{1}$. False is the abstract proposition $\mathbf{0}$.
‘Everything John says is true’, $\prod_{P: Prop} (says(John, P) \to P = True)$.
If the type of apples on my tables has one or no members, do I call it a proposition? No, since it needn’t have been so. In fact I could have a time-dependent or place-dependent type, ‘apples on my table(t)’. Only if the type is forced to be subsingleton at all times do we say ‘proposition’. Is the flag flying today?
There may be subtle variations behind such judgements.
Prime which are the difference between the squares of two primes.
Pairs of primes whose squares differ by 5.
The latter looks like it could depend on $n:N$, with varying cardinalities. Once you come to see in a situation that there’s a most one, does judgement of propositional status change.
Truncation: $\|A\|$ for a type $A$.
Implication into a prop: $[A, P]$, in particular $\neg A$.
$\prod_{x:A} P(x)$ for propositions, $P(x)$ (subsumes latter).
dependent proposition at a value, $P(a)$, dependent relation at tuple, etc..
$Id_A(a, b)$ for a set $A$, and two elements.
What elements can we generate for $\neg P$?
Last revised on November 17, 2020 at 02:52:25. See the history of this page for a list of all contributions to it.