nLab
mere proposition

Mere Propositions

Mere Propositions

Idea

In homotopy type theory, the notion of mere proposition is an internalization of the notion of proposition / (-1)-truncated object. Mere propositions are also called h-propositions, types of h-level 11, (1)(-1)-truncated types, or even just propositions if no ambiguity will result. Semantically, mere propositions correspond to (-1)-groupoids or more generally (-1)-truncated objects.

Mere propositions are one way to embed logic into homotopy type theory, via the propositions as some types / bracket types approach. For many purposes, this is the “correct” way to embed logic (as opposed to the propositions as types approach — for instance, the PAT version of excluded middle contradicts the univalence axiom, whereas the mere-propositional version does not).

Definition

Consider intensional type theory with dependent sums, dependent products, and identity types.

There are many equivalent definitions of a type being an h-proposition. Perhaps the simplest is as follows.

Definition

For AA a type, let isProp(A)isProp(A) denote the dependent product of the identity types for all pairs of terms of AA:

isProp(A) x:A y:A(x=y) isProp(A) \coloneqq \prod_{x\colon A} \prod_{y\colon A} (x=y)

We say that AA is an h-proposition if isProp(A)isProp(A) is an inhabited type.

In propositions as types language, this can be pronounced as “every two elements of AA are equal”.

Proposition

The following are two provably equivalent definitions of isProp(A)isProp(A), in terms of the dependent type isContr()isContr(-) that checks for contractible types:

  • isProp(A) x:A y:AisContr(x=y)isProp(A) \coloneqq \prod_{x\colon A} \prod_{y\colon A} isContr(x=y)
  • isProp(A)(AisContr(A)) isProp(A) \coloneqq (A \to isContr(A))

The first fits into the general inductive definition of n-groupoid: an \infty-groupoid is an nn-groupoid if all its hom-groupoids are (n1)(n-1)-groupoids. The second says that being a proposition is equivalent to being “contractible if inhabited”.

Properties

  • We can prove that for any AA, the type isProp(A)isProp(A) is an h-proposition, i.e. isProp(isProp(A))isProp(isProp(A)). Thus, any two inhabitants of isProp(A)isProp(A) (witnesses that AA is an h-proposition) are “equal”.

  • If AA and BB are h-props and there exist maps ABA\to B and BAB\to A, then AA and BB are equivalent.

Categorical semantics

We discuss the categorical semantics of h-propositions.

Let 𝒞\mathcal{C} be a locally cartesian closed category with sufficient structure to interpret all the above type theory. This means that CC has a weak factorization system with stable path objects, and that trivial cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.)

Then for a fibrant object AA, the object isProp(A)isProp(A) defined above (with the first definition) is obtained by taking dependent product of the path-object A IA×AA^I \to A\times A along the projection A×A1A\times A\to 1. By adjunction, a global element of isProp(A)isProp(A) is therefore equivalent to a section of the path-object, which exactly means a (right) homotopy between the two projections A×AAA\times A\;\rightrightarrows\; A. The existence of such a homotopy, in turn, is equivalent to saying that any two maps XAX\;\rightrightarrows\; A are homotopic.

More generally, we may apply this locally. Suppose that ABA\to B is a fibration, which we can regard as a dependent type

x:BA(x):Type.x\colon B \vdash A(x)\colon Type.

Then we have a dependent type

x:BisProp(A(x)):Typex\colon B \vdash isProp(A(x))\colon Type

represented by a fibration isProp(A)BisProp(A)\to B. By applying the above argument in the slice category 𝒞/B\mathcal{C}/B, we see that isProp(A)BisProp(A)\to B has a section exactly when any two maps in 𝒞/B\mathcal{C}/B into ABA\to B are homotopic over BB. We can also construct the type

x:BisProp(A(x))\prod_{x\colon B} isProp(A(x))

in global context, which has a global element precisely when isProp(A)BisProp(A)\to B has a section.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

References

Last revised on March 11, 2014 at 09:47:07. See the history of this page for a list of all contributions to it.