Andrew Swan: Computable and non-computable 2-groups

Abstract: 2-group is the simplest highest dimensional generalisation of group. Concretely, we can think of a 2-group as a pair of groups, where one acts on the other, together with some other algebraic structure, satisfying certain axioms. They naturally arise in homotopy theory, where every space has for each n not just an n-th homotopy group, but an nth homotopy 2-group. In particular, "up to homotopy," we can think of 2-groups as an algebraic way of thinking about 2-truncated spaces.

Computable groups are groups whose elements can be "computably" represented as natural numbers, making the group multiplication also computable. I'll give a synthetic definition of computable 2-group in homotopy type theory, using ideas from synthetic computability theory to simplify the definition of "computable" and ideas from synthetic homotopy theory to simplify the definition of "2-group." I'll give a couple of examples of non-computable finitely generated 2-group - one as a corollary of known results on computable groups, and one strictly making use of the higher structure of the 2-group.