|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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 , -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).
There are many equivalent definitions of a type being an h-proposition. Perhaps the simplest is as follows.
We say that is an h-proposition if is an inhabited type.
In propositions as types language, this can be pronounced as “every two elements of are equal”.
The first fits into the general inductive definition of n-groupoid: an -groupoid is an -groupoid if all its hom-groupoids are -groupoids. The second says that being a proposition is equivalent to being “contractible if inhabited”.
We can prove that for any , the type is an h-proposition, i.e. . Thus, any two inhabitants of (witnesses that is an h-proposition) are “equal”.
If and are h-props and there exist maps and , then and are equivalent.
We discuss the categorical semantics of h-propositions.
Let be a locally cartesian closed category with sufficient structure to interpret all the above type theory. This means that 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 , the object defined above (with the first definition) is obtained by taking dependent product of the path-object along the projection . By adjunction, a global element of is therefore equivalent to a section of the path-object, which exactly means a (right) homotopy between the two projections . The existence of such a homotopy, in turn, is equivalent to saying that any two maps are homotopic.
More generally, we may apply this locally. Suppose that is a fibration, which we can regard as a dependent type
Then we have a dependent type
in global context, which has a global element precisely when has a section.
|homotopy level||n-truncation||homotopy theory||higher category theory||higher topos theory||homotopy type theory|
|h-level 0||(-2)-truncated||contractible space||(-2)-groupoid||true/unit type/contractible type|
|h-level 1||(-1)-truncated||contractible-if-inhabited||(-1)-groupoid/truth value||(0,1)-sheaf/ideal||mere proposition/h-proposition|
|h-level 2||0-truncated||homotopy 0-type||0-groupoid/set||sheaf||h-set|
|h-level 3||1-truncated||homotopy 1-type||1-groupoid/groupoid||(2,1)-sheaf/stack||h-groupoid|
|h-level 4||2-truncated||homotopy 2-type||2-groupoid||(3,1)-sheaf/2-stack||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||(4,1)-sheaf/3-stack||h-3-groupoid|