# nLab propositional extensionality

Contents

### Context

#### Type theory

= + +

/-/
,
of / of
introduction rule for for hom-tensor adjunction
( of) ( of)
into into
( of) ( of)
, ,
higher
/-//
/
, () ,
(, ) /
(absence of) (absence of)

homotopy levels

semantics

#### Universes

Disambiguation: This should not be confused with propositional extensionality in extensional type theory.

# Contents

### Idea

In formal logic propositional extensionality holds when any two propositions $P$ and $Q$ are identified, $P = Q$, precisely if they imply each other, $(P \leftrightarrow Q)$ (hence if they are logically equivalent $(P \simeq Q)$), i.e.

$(P=Q) \simeq (P\leftrightarrow Q) \,.$

## Properties

### In type theory and Relation to univalence

In type theory the expression $(P=Q)$ is the identity type $Id_{Prop}(P,Q)$ of the universe of propositions (or of the whole universe of types, under propositions as types), with $P$ and $Q$ substituted. One might more precisely write $('P'='Q')$ here, with the quotation marks indicating that this is the name of the proposition, namely a term of the universe type, rather than the proposition/type itself.

On the other hand, the expression $(P \leftrightarrow Q)$ in homotopy type theory is the type of equivalences $(P \simeq Q)$ between the two propositions, hence the subtype of the function type $(P \to Q)$ on those terms that, in particular, have a homotopy inverse.

Hence propositional extensionality in type theory is the statement that

$('P' = 'Q') \simeq (P \simeq Q) \,.$

In homotopy type theory, the assertion of this equivalence is a special case of the univalence axiom which asserts this equivalence for all types $P$,$Q$, not necessarily propositions, with the identity type of the full universe of types on the left.

## History

Specializing to the case where one of the propositions is ‘true’, George Boole can be thought to be talking about propositional extensionality when he writes (Boole 1853, p. 53):

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, viz., of the proposition “The sun shines.” And, therefore, the proposition in which we thus speak is a secondary one. Every primary proposition may thus give rise to a secondary proposition, viz., to that secondary proposition which asserts its truth, or declares its falsehood.

Later this became Alfred Tarski‘s material adequacy condition, also known as Convention T:

any viable theory of truth must entail, for every sentence $P$ of a language, a sentence of the form:

$'P'$ is true if, and only if, $P$.

This may be regarded as the above equivalence of propositional extensiomnaly for the case that $Q \coloneqq$ true:

$('P' = 'true') \simeq (P \simeq true) \,.$
• George Boole, An Investigation of the Laws of Thought, (1853) (retyped pdf)