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
Let $G$ be an abelian group, and $n$ a natural number. The Eilenberg-MacLane space $K(G,n)$ is the unique space that has $\pi_n(K(G,n))\cong G$ and its other homotopy groups trivial. These spaces are a basic tool in classical algebraic topology, they can be used to define cohomology.
There is an analogous construction in homotopy type theory.
Let $G$ be a group. The Eilenberg-MacLane space type $K(G,1)$ is the higher inductive 1-type with the following constructors:
$base$ is a point of $K(G,1)$, $loop$ is a function that constructs a path from $base$ to $base$ for each element of $G$. $id$ says the path constructed from the identity element is the trivial loop. Finally, $comp$ says that the path constructed from group multiplication of elements is the concatenation of paths.
It should be noted that this type is 1-truncated which could be added as another constructor:
To define a function $f : K(G,1) \to C$ for some type $C$, it suffices to give
Then $f$ satisfies the equations
It should be noted that the above can be compressed, to specify a function $f : K(G,1) \to C$, it suffices to give:
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Dan Licata, Eric Finster, Eilenberg-MacLane spaces in homotopy type theory, LICS 2014 (pdf text, Agda HoTT code, web discussion)
Formalization that $K(G,n)$ is a spectrum here
Last revised on June 9, 2022 at 06:13:31. See the history of this page for a list of all contributions to it.