nLab propositions as some types

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Constructivism, Realizability, Computability

(0,1)(0,1)-Category theory

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 excluded middle and 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 excluded middle and the law of double negation are both 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 Coquand/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.

type, type theory

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

Last revised on August 15, 2024 at 14:12:51. See the history of this page for a list of all contributions to it.