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 $\mathbf{2}$ as follows
One could prove that $(\mathbf{2}, 0, 1, \neg, \wedge, \vee, \implies)$ form a Boolean algebra. The poset structure is given by implication.
One could also inductively define observational equality on the booleans $\mathrm{Eq}_\mathbb{2}(x, y)$ as an indexed inductive type on the boolean type $\mathbb{2}$ with the following constructors
A boolean predicate valued in a type $T$ is a function $P: T \rightarrow \mathbf{2}$, and the type $T \to \mathbf{2}$ is a boolean function algebra for finite types $T$, and if path types exist, for all types $T$. Thus the functor $F: U \to BoolAlg$, $F(T) = T \to \mathbf{2}$ for a type universe $U$ is a Boolean hyperdoctrine, and one could do classical first-order logic inside $U$ if $\mathbf{2}$ and path types exist in $U$.
In fact, just with dependent sum types, dependent product types, empty type, unit type, and the two-valued type in a type universe $U$, any two-valued logic could be done inside $U$. Furthermore, since binary disjoint coproducts exist when $\mathbf{2}$ exists, all finite types exist in $U$, and any finitely-valued logic?, such as the internal logic of a finite cartesian power of Set, could be done inside $U$.
For finite types, one could also inductively define specific functions
from the type of boolean predicates on $A$ and $\mathbf{2}$ such that they behave like existential quantification and universal quantification.
A bi-pointed type is a type $A$ with a function $\mathbf{2}\to A$. 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 $\mathcal{U}$.
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.