41 citations · 172 across the 17 of their papers we have counts for
1 paper · 1 filter
Nicolai Kraus, Thorsten Altenkirch
Given a type A in homotopy type theory (HoTT), we can define the free infinity-group on A as the loop space of the suspension of A+1. Equivalently, this free higher group can be de…