Free Groups in Homotopy Type Theory - Free Groups as Filtered Colimits

Abstract

While the construction of the free group on an arbitrary set is trivial in classical set-theory, in absence of decidable equality this is not so. This is the case in univalent mathematics, where not every set a priori has this property. Existing work uses the Church-Rosser property to get around this, while we propose a different appraoch. First, the free group is constructed for finite sets in the expected manner. This construction is then used as, secondly, the free group of an arbitrary set X is constructed as a filtered colimit of finite sets with maps into X. This necessitates showing that this comma category of finite sets is filtered, where coequalizers are given by induction on the cardinality of finite sets, as opposed to the conventional approach using quotients. Finally, we show that the resulting free group functor is indeed the left Kan extension. We formalize the resulting univalent construction in Agda.