nLab type of propositions

Redirected from "universe of all propositions".

Context

Universes

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

Contents

Idea

In type theory a type of propositions — typically denoted PropProp or Ω\Omega — corresponds, under categorical semantics, roughly to a subobject classifier.

(To be precise, depending on the type theoretic rules and axioms this may not be quite true: one needs propositional resizing, propositional extensionality, and — in some type theories where “proposition” is not defined as an h-proposition, such as the calculus of constructions — the principle of unique choice.)

Its generalization from propositions to general types is a type universe.

The subtypes of a type AA may typically be identified with the function types into the type of propositions

Sub(A)=Prop AAPropAΩ. Sub(A) \;\; = \;\; Prop_A \;\; \equiv \;\; A \to Prop \;\; \equiv \;\; A \to \Omega \,.

In dependent type theory such a P:APropP \,\colon\, A \to Prop is equivalently an AA-dependent proposition, to be understood as assingning to any term a:Aa \colon A the assertion that “aa is contained in the given subtype”.

Definition

There are many different ways of defining the isProp modality in dependent type theory. Some of them include

isProp(A) x:A y:Ax= Ay\mathrm{isProp}(A) \coloneqq \prod_{x:A} \prod_{y:A} x =_A y
isProp(A) x:A y:AisContr(x= Ay)\mathrm{isProp}(A) \coloneqq \prod_{x:A} \prod_{y:A} \mathrm{isContr}(x =_A y)
isProp(A)AisContr(A)\mathrm{isProp}(A) \coloneqq A \to \mathrm{isContr}(A)

We shall be agnostic about the different definitions of isProp(A)\mathrm{isProp}(A), and just directly use isProp(A)\mathrm{isProp}(A).

The type of all propositions

The type of all propositions Prop\mathrm{Prop} in a dependent type theory could be presented either as a Russell universe or a Tarski universe. The difference between the two is that in the former, every mere proposition in the type theory is literally an element of the type of all propositions, while in the latter, elements of Prop\mathrm{Prop} are only indices of a (-1)-truncated type family El\mathrm{El}; every mere proposition in the type theory is only essentially Prop \mathrm{Prop} -small for weak Tarski universes or judgmentally equal to an El(P)\mathrm{El}(P) for P:PropP:\mathrm{Prop} for strict Tarski universes.

As a strict Tarski universe

As a strict Tarski universe, the type of all propositions is given by the following natural deduction inference rules:

Formation rules for the type of all propositions:

ΓctxΓProptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Prop} \; \mathrm{type}}

Introduction rules for the type of all propositions:

ΓAtypeΓtoProp A:isProp(A)Prop\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toProp}_A:\mathrm{isProp}(A) \to \mathrm{Prop}}

Elimination rules for the type of all propositions:

ΓA:PropΓEl(A)typeΓA:PropΓproptrunc(A):isProp(El(A))\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(\mathrm{El}(A))}

Computation rules for the type of all propositions:

ΓAtypeΓp:isProp(A)ΓEl(toProp A(p))Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{El}(\mathrm{toProp}_A(p)) \equiv A \; \mathrm{type}}
  • Judgmental computation rules:
ΓAtypeΓp:isProp(A)Γproptrunc(toProp A(p))p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{proptrunc}(\mathrm{toProp}_A(p)) \equiv p:\mathrm{isProp}(A)}
  • Typal computation rules:
ΓAtypeΓp:isProp(A)Γβ Prop proptrunc,A(p):proptrunc(toProp A(p))= isProp(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{proptrunc},A}(p):\mathrm{proptrunc}(\mathrm{toProp}_A(p)) =_{\mathrm{isProp}(A)} p}

Uniqueness rules for the type of all propositions:

  • Judgmental computation rules:

    ΓA:PropΓAtoProp El(A)(proptrunc(A)):Prop\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash A \equiv \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A)):\mathrm{Prop}}
  • Typal computation rules:

    ΓA:PropΓη Prop(A):A= ProptoProp El(A)(proptrunc(A))\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \eta_{\mathrm{Prop}}(A):A =_{\mathrm{Prop}} \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))}

Extensionality principle of the type of all propositions:

ΓA:PropΓB:PropΓext Prop(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Prop} \quad \Gamma \vdash B:\mathrm{Prop}} {\Gamma \vdash \mathrm{ext}_\mathrm{Prop}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}

As a weak Tarski universe

As a weak Tarski universe, the type of all propositions is given by the following natural deduction inference rules:

Formation rules for the type of all propositions:

ΓctxΓProptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Prop} \; \mathrm{type}}

Introduction rules for the type of all propositions:

ΓAtypeΓtoProp A:isProp(A)Prop\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toProp}_A:\mathrm{isProp}(A) \to \mathrm{Prop}}

Elimination rules for the type of all propositions:

ΓA:PropΓEl(A)typeΓA:PropΓproptrunc(A):isProp(El(A))\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(\mathrm{El}(A))}

Computation rules for the type of all propositions:

ΓAtypeΓp:isProp(A)Γβ Prop El,A(p):El(toProp A(p))Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{El}, A}(p):\mathrm{El}(\mathrm{toProp}_A(p)) \simeq A \; \mathrm{type}}
  • Judgmental computation rules:
ΓAtypeΓp:isProp(A)Γcongform isProp(β Prop El,A(p))(proptrunc(toProp A(p)))p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p))(\mathrm{proptrunc}(\mathrm{toProp}_A(p))) \equiv p:\mathrm{isProp}(A)}
  • Typal computation rules:
ΓAtypeΓp:isProp(A)Γβ Prop proptrunc,A(p):congform isProp(β Prop El,A(p))(proptrunc(toProp A(p)))= isProp(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{proptrunc},A}(p):\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p))(\mathrm{proptrunc}(\mathrm{toProp}_A(p))) =_{\mathrm{isProp}(A)} p}

where the equivalence

congform isProp(β Prop El,A(p)):isProp(El(toProp A(p)))isProp(A)\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p)):\mathrm{isProp}(\mathrm{El}(\mathrm{toProp}_A(p))) \simeq \mathrm{isProp}(A)

can always be constructed in a type theory with dependent product types, dependent sum types, and identity types, and function extensionality, as given types AA and BB and an equivalence e:ABe:A \simeq B, it is always possible to form the equivalence

congform isProp(e):isProp(A)isProp(B)\mathrm{congform}_\mathrm{isProp}(e):\mathrm{isProp}(A) \simeq \mathrm{isProp}(B)

For example, for isProp\mathrm{isProp} defined as the dependent product type x:A y:Ax= Ay\prod_{x:A} \prod_{y:A} x =_A y, we have that the application of the equivalence e:ABe:A \simeq B to identifications is itself an equivalence:

ap e(x,y):(x= Ay)(e(x)= Be(y))\mathrm{ap}_e(x, y):(x =_A y) \simeq (e(x) =_B e(y))

Then by the typal congruence rules of dependent function types, there is an equivalence

congform isProp(e)congform (e,λx:A.congform (e,λy:A.ap e(x,y))):( x:A y:Ax= Ay)( x:B y:Bx= By)\mathrm{congform}_\mathrm{isProp}(e) \equiv \mathrm{congform}_{\prod}(e, \lambda x:A.\mathrm{congform}_{\prod}(e, \lambda y:A.\mathrm{ap}_e(x, y))):\left(\prod_{x:A} \prod_{y:A} x =_A y\right) \simeq \left(\prod_{x:B} \prod_{y:B} x =_B y\right)

And for any other definition of isProp\mathrm{isProp}, we have an equivalence δ isProp(A):isProp(A) x:A y:Ax= Ay\delta_{\mathrm{isProp}(A)}:\mathrm{isProp}(A) \simeq \prod_{x:A} \prod_{y:A} x =_A y for type AA, and so there is an equivalence

congform isProp(e)δ isProp(B) 1congform (e,λx:A.congform (e,λy:A.ap e(x,y)))δ isProp(A):isProp(A)isProp(B)\mathrm{congform}_\mathrm{isProp}(e) \equiv \delta_{\mathrm{isProp}(B)}^{-1} \circ \mathrm{congform}_{\prod}(e, \lambda x:A.\mathrm{congform}_{\prod}(e, \lambda y:A.\mathrm{ap}_e(x, y))) \circ \delta_{\mathrm{isProp}(A)}:\mathrm{isProp}(A) \simeq \mathrm{isProp}(B)

Uniqueness rules for the type of all propositions:

  • Judgmental computation rules:

    ΓA:PropΓAtoProp El(A)(proptrunc(A)):Prop\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash A \equiv \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A)):\mathrm{Prop}}
  • Typal computation rules:

    ΓA:PropΓη Prop(A):A= ProptoProp El(A)(proptrunc(A))\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \eta_{\mathrm{Prop}}(A):A =_{\mathrm{Prop}} \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))}

Extensionality principle of the type of all propositions:

ΓA:PropΓB:PropΓext Prop(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Prop} \quad \Gamma \vdash B:\mathrm{Prop}} {\Gamma \vdash \mathrm{ext}_\mathrm{Prop}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}

As a Russell universe

As a Russell universe, the type of all propositions is given by the following natural deduction inference rules:

Formation rules for the type of all propositions:

ΓctxΓProptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Prop} \; \mathrm{type}}

Introduction rules for the type of all propositions:

ΓAtypeΓtoProp A:isProp(A)Prop\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toProp}_A:\mathrm{isProp}(A) \to \mathrm{Prop}}

Elimination rules for the type of all propositions:

ΓA:PropΓAtypeΓA:PropΓproptrunc(A):isProp(A)\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(A)}

Computation rules for the type of all propositions:

ΓAtypeΓp:isProp(A)ΓtoProp A(p)Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{toProp}_A(p) \equiv A \; \mathrm{type}}
  • Judgmental computation rules:
ΓAtypeΓp:isProp(A)Γproptrunc(toProp A(p))p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{proptrunc}(\mathrm{toProp}_A(p)) \equiv p:\mathrm{isProp}(A)}
  • Typal computation rules:
ΓAtypeΓp:isProp(A)Γβ Prop proptrunc,A(p):proptrunc(toProp A(p))= isProp(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{proptrunc},A}(p):\mathrm{proptrunc}(\mathrm{toProp}_A(p)) =_{\mathrm{isProp}(A)} p}

Uniqueness rules for the type of all propositions:

  • Judgmental computation rules:

    ΓA:PropΓAtoProp A(proptrunc(A)):Prop\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash A \equiv \mathrm{toProp}_{A}(\mathrm{proptrunc}(A)):\mathrm{Prop}}
  • Typal computation rules:

    ΓA:PropΓη Prop(A):A= ProptoProp A(proptrunc(A))\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \eta_{\mathrm{Prop}}(A):A =_{\mathrm{Prop}} \mathrm{toProp}_{A}(\mathrm{proptrunc}(A))}

Extensionality principle for the type of all propositions:

ΓA:PropΓB:PropΓext Prop(A,B):(A= PropB)(AB)\frac{\Gamma \vdash A:\mathrm{Prop} \quad \Gamma \vdash B:\mathrm{Prop}} {\Gamma \vdash \mathrm{ext}_\mathrm{Prop}(A, B):(A =_\mathrm{Prop} B) \simeq (A \simeq B)}

Other types of propositions

Other types of propositions include

  • the boolean domain, which is the type of decidable propositions.

  • any dominance, which is the type of open propositions, or the type of semi-decidable propositions.

  • For a Russell universe UU, the type A:UisProp(A)\sum_{A:U} \mathrm{isProp}(A) is the type of UU-small propositions. Similarly, for a Tarski universe (U,T)(U, T), the type A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A)) is the type of UU-small propositions

  • sProp, which is the type of strict propositions

  • any contractible type, which is (equivalent to) the type of pointed propositions or the type of contractible types.

In general, these types of propositions can also be distinguished between their Russell and Tarski variants, where elements of the type of propositions are actual types, or indices for the type family El\mathrm{El}.

Most generally, a type of propositions is a type Ω\Omega with a type family TT such that

  • for every elements P:ΩP:\Omega, the type T(P)T(P) is an h-proposition:
    P:Ω a:T(P) b:T(P)a= T(P)b\prod_{P:\Omega} \prod_{a:T(P)} \prod_{b:T(P)} a =_{T(P)} b
  • the transport function
    trans T(P,Q):P= ΩQ(T(P)T(Q))\mathrm{trans}^T(P, Q):P =_\Omega Q \to (T(P) \simeq T(Q))

    is an equivalence of types for all elements P:ΩP:\Omega and Q:ΩQ:\Omega

    P:Ω Q:ΩisEquiv(trans T(P,Q))\prod_{P:\Omega} \prod_{Q:\Omega} \mathrm{isEquiv}(\mathrm{trans}^T(P, Q))

These axioms imply that (Ω,T)(\Omega, T) satisfy propositional extensionality and thus that Ω\Omega is an h-set.

Predicate logic

In this section, we assume that function extensionality or weak function extensionality is true for all dependent function types.

The empty type and falsehood

For Russell types of all propositions, the type P:PropP\prod_{P:\mathrm{Prop}} P is the empty type \emptyset, which by weak function extensionality is a proposition, so is already in the type of all propositions ( P:PropP):Prop\left(\prod_{P:\mathrm{Prop}} P\right):\mathrm{Prop}. Similarly, for Tarski types of all propositions, the type P:PropEl(P)\prod_{P:\mathrm{Prop}} \mathrm{El}(P) is the empty type, which by weak function extensionality is a proposition, and so one has the element ( P:PropEl(P)) Prop:Prop\left(\prod_{P:\mathrm{Prop}} \mathrm{El}(P)\right)_\mathrm{Prop}:\mathrm{Prop}.

In either case, the definition implies that if the empty type has an element, then every proposition has an element and is thus contractible. This implies that the empty type represents falsehood \bot in the type of all propositions.

The type of pointed propositions and truth

The type of pointed propositions Prop *\mathrm{Prop}_* is given by the type P:PropP\sum_{P:\mathrm{Prop}} P for Russell types of propositions and P:PropEl(P)\sum_{P:\mathrm{Prop}} \mathrm{El}(P) for Tarski types of propositions, and because pointed propositions are contractible types, pointed propositions are equivalent to each other, and thus by the extensionality principle of Prop\mathrm{Prop}, they are equal to each other; thus, the type of pointed propositions is a proposition.

Because Prop *\mathrm{Prop}_* is itself a proposition, Prop *\mathrm{Prop}_* is an element of itself, and thus a pointed proposition and a contractible type. This implies that the type of pointed propositions represents truth \top in the type of all propositions.

Propositional truncations

Given the type of all propositions Prop\mathrm{Prop} and given a type AA, the propositional truncation of a type AA, which turns AA into an element of Prop\mathrm{Prop}, is given for Russell types of all propositions by the type

[A] P:Prop(AP)P[A] \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to P

and for Tarski types of all propositions by the type

[A] P:Prop(AEl(P))El(P)[A] \equiv \prod_{P:\mathrm{Prop}} (A \to \mathrm{El}(P)) \to \mathrm{El}(P)

By weak function extensionality, both of these types are propositions.

Universal quantification

Given any type AA and family of propositions P(x)P(x) indexed by x:Ax:A, by weak function extensionality, the dependent function type x:AP(x)\prod_{x:A} P(x) is also a proposition. This means that the propositional truncation of x:AP(x)\prod_{x:A} P(x) is equivalent to x:AP(x)\prod_{x:A} P(x), and the dependent function type is used as the universal quantifier.

More generally, given any type AA and family of propositions B(x)B(x) indexed by x:Ax:A, the universal quantifier is given by propositional truncation of the dependent product type:

x:A.B(x)[ x:AB(x)]\forall x:A.B(x) \equiv \left[\prod_{x:A} B(x)\right]

Implication and negation

Given any proposition QQ and PP, by weak function extensionality, the function type QPQ \to P is also a proposition. This means that the propositional truncation of APA \to P is equivalent to QPQ \to P, and the function type is used as implication. If PP is the empty type or falsehood defined above, then the function type represents the negation of QQ, ¬QQ\neg Q \equiv Q \to \emptyset.

More generally, given any type AA and BB, implication is given by propositional truncation of the function type:

AB[AB]A \implies B \equiv \left[A \to B\right]

Biconditionals

Given any proposition PP and QQ, by weak function extensionality, the equivalence type PQP \simeq Q is also a proposition. This means that the propositional truncation of PQP \simeq Q is equivalent to PQP \simeq Q, and the equivalence type is used as the biconditional.

More generally, given any type AA and BB, the biconditional is given by propositional truncation of the equivalence type:

AB[AB]A \iff B \equiv \left[A \simeq B\right]

Existential quantification

Given any type AA and family of types B(x)B(x) indexed by x:Ax:A, the existential quantifier is given by the type

x:A.B(x) P:Prop( x:AB(x)P)P\exists x:A.B(x) \equiv \prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P

for Russell types of propositions and

x:A.B(x) P:Prop( x:AB(x)El(P))El(P)\exists x:A.B(x) \equiv \prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to \mathrm{El}(P)\right) \to \mathrm{El}(P)

for Tarski types of propositions.

If the type theory also has dependent sum types, the existential quantifier is equivalently given by the propositional truncation of the dependent sum type

x:A.B(x)[ x:AB(x)]\exists x:A.B(x) \equiv \left[\sum_{x:A} B(x)\right]

since by currying there is an equivalence

(( x:AB(x))P)( x:AB(x)P)\left(\left(\sum_{x:A} B(x)\right) \to P\right) \simeq \left(\prod_{x:A} B(x) \to P\right)

Conjunction

Given types AA and BB, the conjunction of AA and BB is given by the type

AB P:Prop(A(BP))PA \wedge B \equiv \prod_{P:\mathrm{Prop}} \left(A \to (B \to P)\right) \to P

for Russell types of propositions and

AB P:Prop(A(BEl(P)))El(P)A \wedge B \equiv \prod_{P:\mathrm{Prop}} \left(A \to (B \to \mathrm{El}(P))\right) \to \mathrm{El}(P)

for Tarski types of propositions.

If the type theory also has product types, the existential quantifier is equivalently given by the propositional truncation of the product type

AB[A×B]A \wedge B \equiv \left[A \times B\right]

since by currying there is an equivalence

((A×B)P)(A(BP))\left((A \times B) \to P\right) \simeq \left(A \to (B \to P)\right)

Disjunctions

Given types AA and BB, the disjunction of AA and BB is given by the type

AB P:Prop(AP)(BP)PA \vee B \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to (B \to P) \to P

for Russell types of propositions and

AB P:Prop(AEl(P))(BEl(P))El(P)A \vee B \equiv \prod_{P:\mathrm{Prop}} (A \to \mathrm{El}(P)) \to (B \to \mathrm{El}(P)) \to \mathrm{El}(P)

for Tarski types of propositions.

If the type theory also has product types, the existential quantifier is equivalently given by the type

AB P:Prop((AP)×(BP))PA \vee B \equiv \prod_{P:\mathrm{Prop}} ((A \to P) \times (B \to P)) \to P

for Russell types of propositions and

AB P:Prop((AEl(P))×(BEl(P)))El(P)A \vee B \equiv \prod_{P:\mathrm{Prop}} ((A \to \mathrm{El}(P)) \times (B \to \mathrm{El}(P))) \to \mathrm{El}(P)

for Tarski types of propositions,

and if the type theory also has coproduct types, the existential quantifier is equivalently given by the propositional truncation of the coproduct type

AB[A+B]A \vee B \equiv \left[A + B\right]

since by currying there is an equivalence

((AP)×(BP))((A+B)P)\left((A \to P) \times (B \to P)\right) \simeq \left((A + B) \to P\right)

Decidable propositions and booleans

A decidable proposition is a proposition PP with a witness p:P¬Pp:P \vee \neg P that the disjunction of PP and its negation holds.

The type of booleans is the type of all decidable propositions in Prop\mathrm{Prop},

Bool P:PropP¬P\mathrm{Bool} \equiv \sum_{P:\mathrm{Prop}} P \vee \neg P

for Russell types of propositions, and

Bool P:PropEl(P)¬El(P)\mathrm{Bool} \equiv \sum_{P:\mathrm{Prop}} \mathrm{El}(P) \vee \neg \mathrm{El}(P)

for Tarski types of propositions.

The law of excluded middle states that every proposition is decidable lem: P:PropP¬P\mathrm{lem}:\prod_{P:\mathrm{Prop}} P \vee \neg P, or equivalently that there is an equivalence lem:BoolProp\mathrm{lem}':\mathrm{Bool} \simeq \mathrm{Prop} between the type of propositions and the type of booleans.

Impredicative polymorphism

Given a universe of all propositions Prop\mathrm{Prop}, impredicative polymorphism of Prop\mathrm{Prop} is equivalent to weak function extensionality.

More generally, a universe of propositions Ω\Omega has impredicative polymorphism if and only if Ω\Omega is closed under dependent product types of predicates valued in Ω\Omega.

Propositional resizing

Theorem

Any universe of propositions satisfying propositional resizing is a contractible type.

Proof

Given a universe of propositions Ω\Omega, the type of all propositions in Ω\Omega is Ω\Omega itself. Then propositional resizing says that Ω\Omega has an element Ω:Ω\Omega':\Omega such that its type reflection is Ω\Omega itself. This implies that Ω\Omega itself a mere proposition by definition of universe of proposiions, which implies that Ω\Omega is a contractible type by the element Ω:Ω\Omega':\Omega and the fact that for all other elements P:ΩP:\Omega, P=ΩP = \Omega'.

Theorem

Any universe of propositions Ω\Omega closed under the empty type does not satisfy propositional resizing.

Proof

Suppose that Ω\Omega is closed under the empty type \emptyset represented in Ω\Omega by the element :Ω\bot:\Omega, and satisfies propositional resizing. Then one has that =Ω\bot = \Omega' since Ω\Omega is a mere proposition, and by transport one has Ω\emptyset \simeq \Omega, but since Ω\Omega is contractible by propositional resizing, the empty type is also contractible, which is false.

Theorem

The universe of all propositions Prop\mathrm{Prop} does not satisfy propositional resizing.

Categorical semantics

The categorical semantics of the type of all propositions is the subobject classifier.

References

Detailed discussion of the type of propositions in Coq is in

Last revised on September 20, 2024 at 00:01:06. See the history of this page for a list of all contributions to it.