# nLab propositions as some types

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

(0,1)-category

(0,1)-topos

# Contents

## Idea

One paradigm of dependent type theory is propositions as some types, in which propositions are identified with particular types, but not all types are regarded as propositions. Generally, the propositions are the “types with at most one term”, i.e. the h-propositions or subsingletons, and the paradigm can thus also be called propositions as subsingletons. This contrasts with the propositions as types paradigm, where all types are regarded as propositions.

Propositions as some types is the paradigm usually used in the internal logic of categories such as toposes. In this case, the type-theoretic operations on types either restrict to the propositions to give logical operations (for conjunction, implication, and the universal quantifier), or have to be “reflected” therein (for disjunction and the existential quantifier). The reflector operation is called a bracket type. The law of double negation in classical mathematics similarly has to be restricted to propositions, unlike the case in the propositions as types paradigm - where the law of double negation is represented by a global choice operator.

Furthermore, most structures traditionally involving predicates or relations are defined as proposition-valued type families in this restricted sense, where each type of the type family has at most one term. For instance, setoids or Bishop sets are usually defined to have an equivalence relation in the propositions as some types paradigm, rather than a pseudo-equivalence relation as typical in the propositions as types paradigm.

Dependent type theory support various foundations of mathematics via the propositions as some types interpretation of dependent type theory.

On the other hand, if one only has a Tarski type of all propositions for higher-order logic, then propositions and subsingletons are not the same thing, and one is following the philosophy of propositions as codes for subsingletons, similar to set theory with the axiom schema of separation.

### Propositions as subsingletons in set theory

There is an analogue of the “propositions as some types” in set theory, called propositions as subsingletons. Instead of working in the external logic, one interprets certain set-theoretic operations as representing the predicate logic:

Compare with propositions as sets, which is the BHK interpretation of the internal logic of a set theory via set-theoretic operations on sets.

Last revised on February 23, 2024 at 22:46:08. See the history of this page for a list of all contributions to it.