nLab type of strict propositions

Redirected from "sProp".

Contents

 Idea

In dependent type theory the type sProp\mathrm{sProp} is a type of strict propositions.

The type of strict proposition is used to formalize logic over type theory in dependent type theory without having to postulate a separate proposition judgment, since strict propositions are judgmentally proof irrelevant, and thus behave as propositions in traditional propositional logic.

Definition

The type of all strict propositions

The type of all strict propositions sProp\mathrm{sProp} 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 strict proposition in the type theory is literally an element of the type of all strict propositions, while in the latter, elements of sProp\mathrm{sProp} are only indices of a type family \Box of strict propositions; every strict proposition in the type theory is only essentially sProp \mathrm{sProp} -small for weak Tarski universes or judgmentally equal to an P\Box P for P:sPropP:\mathrm{sProp} for strict Tarski universes.

As a Russell universe

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

Formation rules:

ΓctxΓsProptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{sProp} \; \mathrm{type}}

Type reflection:

ΓA:sPropΓAtype\frac{\Gamma \vdash A:\mathrm{sProp}}{\Gamma \vdash A \; \mathrm{type}}

Strictness for each type reflection

ΓA:sPropΓ,x:A,y:Axy:A\frac{\Gamma \vdash A:\mathrm{sProp}}{\Gamma, x:A, y:A \vdash x \equiv y:A}

Introduction rule:

ΓAtypeΓ,x:A,y:Axy:AΓA:sProp\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x \equiv y:A}{\Gamma \vdash A:\mathrm{sProp}}

Univalence:

ΓA:sPropΓB:sPropΓunivalence(A,B):Id sProp(A,B)(AB)\frac{\Gamma \vdash A:\mathrm{sProp} \quad \Gamma \vdash B:\mathrm{sProp}} {\Gamma \vdash \mathrm{univalence}(A, B):\mathrm{Id}_\mathrm{sProp}(A, B) \simeq (A \simeq B)}

As a Tarski universe

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

Formation rules:

ΓctxΓsProptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{sProp} \; \mathrm{type}}

Type reflection:

ΓA:sPropΓAtype\frac{\Gamma \vdash A:\mathrm{sProp}}{\Gamma \vdash \Box A \; \mathrm{type}}

Strictness for each type reflection

ΓA:sPropΓ,x:A,y:Axy:A\frac{\Gamma \vdash A:\mathrm{sProp}}{\Gamma, x:A, y:A \vdash x \equiv y:A}

Introduction rule:

ΓAtypeΓ,x:A,y:Axy:AΓA Ω:sProp\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x \equiv y:A}{\Gamma \vdash A_\Omega:\mathrm{sProp}}

Essential smallness of propositions (for weak types of all propositions) or judgmental equality (for strict types of all propositions):

ΓAtypeΓ,x:A,y:Axy:AΓδ A:A ΩAweakΓAtypeΓ,x:A,y:Axy:AΓA ΩAtypestrict\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x \equiv y:A}{\Gamma \vdash \delta_A:\Box A_\Omega \simeq A}\mathrm{weak} \quad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x \equiv y:A}{\Gamma \vdash \Box A_\Omega \equiv A \; \mathrm{type}}\mathrm{strict}

Univalence:

ΓA:sPropΓB:sPropΓunivalence(A,B):isEquiv(transport box(A,B))\frac{\Gamma \vdash A:\mathrm{sProp} \quad \Gamma \vdash B:\mathrm{sProp}} {\Gamma \vdash \mathrm{univalence}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\box(A, B))}

The empty proposition and falsehood

To ensure that the type of all strict propositions isn’t a contractible type, one could include the following axiom, which states that there exists a strict proposition satisfying ex falso quodlibet:

ΓctxΓaxempty: :sProp C:sProp x:C(x)RussellΓctxΓaxempty: :sProp C:sProp x:C(x)Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{axempty}:\sum_{\bot:\mathrm{sProp}} \prod_{C:\bot \to \mathrm{sProp}} \prod_{x:\bot} C(x)}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{axempty}:\sum_{\bot:\mathrm{sProp}} \prod_{C:\Box \bot \to \mathrm{sProp}} \prod_{x:\Box \bot} \Box C(x)}\mathrm{Tarski}

 References

Last revised on September 17, 2023 at 16:40:50. See the history of this page for a list of all contributions to it.