|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-level 1-type/h-prop|
|classical type theory?||internal logic||classical type theory?, logic programming?|
|cut elimination?||counit||beta reduction|
|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 monad||modal type theory, monad (in computer science)|
h-Propositions are also said to be of h-level .
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 intepret 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.
h-level 2 | 0-truncated | discrete space | 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 | | h-2-groupoid h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | | h-3-groupoid h-level | -truncated | homotopy n-type | n-groupoid | | h--groupoid | h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid
Coq-code for h-propositions is in