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
Basic structures
Generating functions
Proof techniques
Combinatorial identities
Polytopes
In dependent type theory (homotopy type theory), by $\pi$-finite types one means a kind of finite types which are not necessarily h-sets but have finite homotopy groups in each degree (what in homotopy theory are called a pi-finite homotopy types or similar).
For given natural number $n$, a type is called $\pi_n$-finite if
it has a finite type of connected components (0-truncation),
all its homotopy groups up to h-level $n$ at all base points are finite.
A type is $\pi$-finite type if it is $\pi_n$-finite for all $n \colon \mathbb{N}$.
Given two $\pi$-finite types $A$ and $B$, the types $A \times B$ and $A + B$ are both $\pi$-finite types. Similarly, given a family of $\pi$-finite types $B(x)$ indexed by a $\pi$-finite type $x:A$, the dependent sum type $\sum_{x:A} B(x)$ is a $\pi$-finite type.
Given a univalent universe $U$ and a natural number $n:\mathbb{N}$,
the type of all $U$-small types with $n$ elements is a $\pi$-finite type.
The type of all $U$-small finite groups of order $n$ is a $\pi$-finite type.
UniMath project, π-finite types (web)
UniMath project, Univalent combinatorics (web)
Last revised on August 12, 2023 at 13:30:47. See the history of this page for a list of all contributions to it.