natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
There are various different paradigms for the interpretation of predicate logic in type theory. In “logic-enriched type theory”, there is a separate class of “propositions” from the class of “types”. But we can also identify propositions with particular types. In the propositions as types-paradigm, every proposition is a type, and also every type is identified with a proposition (the proposition that it is an inhabited type).
By contrast, in the paradigm that may be called propositions as some types, every proposition is a type, but not every type is a proposition. The types which are propositions are generally those which “have at most one inhabitant” — in homotopy type theory this is called being of h-level 1 or being a (-1)-type. This paradigm is often used in the categorical semantics of type theory, such as the internal logic of various kinds of categories.
Under “propositions as types”, all type-theoretic operations represent corresponding logical operations (dependent sum is the existential quantifier, dependent product the universal quantifier, and so on). However, under “propositions as some types”, not every such operation preserves the class of propositions; this is particularly the case for dependent sum and disjunction(or). Thus, in order to obtain the correct logical operations, we need to reflect these constructions back into propositions somehow, finding the “underlying proposition”, corresponding to the (-1)-truncation/h-level 1-projection. This operation in type theory is called the bracket type (when denoted ); in homotopy type theory it can be identified with the higher inductive type .
In dependent type theory, the propositional truncation of a type is defined as the higher inductive type generated by the two constructors
In any dependent type theory with identity types, given type , the support of denoted or or or or or, lastly, , is the higher inductive type defined by the two constructors
where in the last sequent on the right we have the identity type. (Voevodsky, HoTTLibrary)
This says that is the type which is universal with the property that the terms of map to it and that any two term of become equivalent in .
data isinhab {i : Level} (A : Set i) : Set i where
inhab : A → isinhab A
inhab-path : (x y : isinhab A) → x ≡ y
The recursion principle for says that if is a mere proposition and we have , then there is an induced such that for all . In other words, any mere proposition which follows from (the inhabitedness of) already follows from . Thus, , as a mere proposition, contains no more information than the inhabitedness of .
The induction principle states that if we have a family of mere propositions indexed by and we have , then there is an induced such that for all .
The inference rules for bracket types are as follows:
Suppose the dependent type theory has a univalent type of all propositions . Then the bracket type of could be defined as the type
Let be the unit type and let be the boolean domain. The bracket type of a type is the localization of at the unique function .
By definition, the type of functions is an equivalence of types.
This is the special case of the n-truncation modality as the n-truncation modality is localization at the unique map from the -dimensional sphere type to the unit type, and is the zero-dimensional sphere type.
For more see at n-truncation modality.
Let denote the join type of and , and let be the iterated join type, inductively defined on the natural numbers by and .
Then the propositional truncation of is the sequential colimit of the sequence of functions
Let be a type and be a binary family of contractible types indexed by and , so that the product projection function for the dependent sum type
is an equivalence of types. Then the propositional truncation of is the quotient set . (The quotient set in dependent type theory can be defined using inference rules without propositional truncations.)
There is another definition of the bracket type as a higher inductive type using functions from the boolean domain. The bracket type is generated by the two constructors
The induction principle states that if we have a family of mere propositions indexed by and we have , then there is an induced such that for all . Here, a mere proposition is defined as a type for which every function from the boolean domain is a weakly constant function, or equivalently, that satisfies .
In section 7.3 of the HoTT Book UFP13, the authors give another definition of the propositional truncation using the hubs and spokes construction developed in section 6.7. Since the boolean domain is the zero-dimensional sphere, the propositional truncation of is a higher inductive type generated by
A function
For each function , a hub point
For each function and each boolean , a spoke path
In dependent type theory, a weakly constant function from type to is a function with a dependent function .
Given a weakly constant function with , by the recursion principle of bracket types, one has
such that
In particular, by the judgmental congruence rule for the introduction rule of function types, every weakly constant function with factors through by
Weakly constant functions can also be regarded directly as functions , similar to how paths in can be regarded as functions from the the interval type rather than the application of said function along the path generator of the interval type.
Given a type , there exists a function defined by
One presentation of the internal type theory of regular categories consists of dependent type theory with the unit type, strong extensional equality types?, strong dependent sums, and bracket types. (The internal logic of a regular category can alternatively be presented as a logic-enriched type theory?.)
The semantics of bracket types in a regular category is as follows.
A dependent type (a type in context )
is interpreted in as an arbitrary morphism
The corresponding bracket type
is interpreted then as the image-factorization
Therefore is a monomorphism, and hence the interpretation of a proposition about the elements of .
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 |
h-level | -truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h--groupoid |
h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid |
The original articles are
(which speaks of “mono types”) and
Frank Pfenning, Intensionality, extensionality, and proof irrelevance in modal type theory, In Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS’01), June 2001.
Steve Awodey, Andrej Bauer, Propositions as Types, Journal of Logic and Computation, 14 (2004) 447-471 [doi:10.1093/logcom/14.4.447, pdf]
Discussion in the context of homotopy type theory:
Exposition:
Formalization:
Vladimir Voevodsky, The hProp version of the “inhabited” construction. (web)
Discussion in the more general context of -truncations:
More on the universal property of propositional truncation:
For propositional truncations as sequential colimits, see section 26.5 of
as well as section 16.2 of the lecture notes:
For n-truncations as localizations at sphere types, see:
That propositional truncations with judgmental computation rules along with the boolean domain imply function extensionality:
Last revised on July 6, 2024 at 11:37:49. See the history of this page for a list of all contributions to it.