|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|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|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)|
|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|
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||(-1)-groupoid/truth value||h-proposition|
|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|
Coq-code for h-propositions is in