Delooping presented groups in homotopy type theory

Camil Champin, Samuel Mimram, Emile Oleon

Homotopy type theory is a logical setting based on Martin-Löf type theory in which geometric constructions and proofs can be carried out synthetically. Here, types can be interpret…