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 be an abelian group, and a natural number. The Eilenberg-MacLane space is the unique space that has 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 be a group. The Eilenberg-MacLane space type is the higher inductive 1-type with the following constructors:
is a point of , is a function that constructs a path from to for each element of . says the path constructed from the identity element is the trivial loop. Finally, 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 for some type , it suffices to give
Then satisfies the equations
It should be noted that the above can be compressed, to specify a function , 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 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.