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
In type theory, the binomial types or binomial sets are the categorification of the binomial coefficients and then the further generalization from finite types/finite sets to arbitrary types or sets.
Given types $A$ and $B$, the binomial type of $A$ and $B$ is defined as
where
$\sum_{(-)} (-)$ denotes the dependent pair type-formation;
$(-)\to(-)$ denotes function type-formation;
$\mathbb{2}$ denotes the finite type with two elements “$0$” and “$1$”;
$(-) =_\mathbb{2} (-)$ denotes its identification type;
$[-]$ denotes propositional truncation (bracket types).
Since $A \simeq B$ is defined as the dependent pair type $\sum_{f:A \to B} \mathrm{isEquiv}(f)$, the above definition is the same as
where given a type family $x:A \vdash B(x)$ the existential quantifier is defined as the propositional truncation of the dependent pair type
This definition can be translated directly into set theory notation as follows:
where $B^A$ is the function set with domain $A$ and codomain $B$ and $\mathbb{2}$ is the two-element set (the classical boolean domain), and the predicate $\mathrm{isBijection}(f)$ on the function set $f \in B^A$ is defined as
This results in binomial sets.
There is an alternative way to express the second definition, by use of a univalent universe, but the resulting type is only locally small relative to the universe.
We define the type of decidable embeddings as the type of functions whose fibers are decidable:
Let $(U, \mathrm{El})$ be a univalent Tarski universe, and given type $A$, let us define $U_A$ to be the type of all types in $U$ which are merely equivalent to $A$:
Then given essentially $U$-small types $A$ and $B$, the locally $U$-small binomial type is defined as
One could also translate the above definition into set theory:
Given a universe $U$ of small sets, the set $U_A$ is defined to be the set of all small sets in $U$ which are in bijection with $A$:
where $i^*(x)$ is the preimage or fiber of $i$ at $x$.
Then given small sets $A$ and $B$, the locally $U$-small binomial set of $A$ and $B$ is defined as the set of all $X \in U_B$ such that there exists a decidable injection from $X$ to $A$:
The above definitions of binomial types can be found, respectively, in remark 17.6.7 and definition 17.6.7 of:
Last revised on August 2, 2023 at 19:26:14. See the history of this page for a list of all contributions to it.