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
The two-valued type is an axiomatization of the two-valued object in the context of homotopy type theory.
As an inductive type, the two-valued type is given by
Inductive Two : Type
| zero : Two
| one : Two
This says that the type is inductively constructed from two terms in the type Two, whose interpretation is as the two points of the type; hence the name two-valued type.
The two-valued type is also called the booleans type or the type of booleans. One could recursively define the logical functions on as follows
One could prove that form a Boolean algebra. The poset structure is given by implication.
One could also inductively define observational equality on the booleans as an indexed inductive type on the boolean type with the following constructors
A boolean predicate valued in a type is a function , and the type is a boolean function algebra for finite types , and if path types exist, for all types . Thus the functor , for a type universe is a Boolean hyperdoctrine, and one could do classical first-order logic inside if and path types exist in .
In fact, just with dependent sum types, dependent product types, empty type, unit type, and the two-valued type in a type universe , any two-valued logic could be done inside . Furthermore, since binary disjoint coproducts exist when exists, all finite types exist in , and any finitely-valued logic?, such as the internal logic of a finite cartesian power of Set, could be done inside .
For finite types, one could also inductively define specific functions
from the type of boolean predicates on and such that they behave like existential quantification and universal quantification.
A bi-pointed type is a type with a function . Examples include the interval type and the function type of the natural numbers type.
The two-valued type is the suspension type of the empty type, and the suspension of the two-valued type is the circle type. Geometrically, the two-valued type is a zero-dimensional sphere.
The two-valued type is homotopy equivalent to the type of decidable propositions in a universe .
As a result, sometimes the two-valued type is called a decidable subset classifier.
For discussion of booleans types in the context of homotopy type theory:
Last revised on December 1, 2022 at 15:03:18. See the history of this page for a list of all contributions to it.