GroupPresentation -> Group. Proof. intros [X I R]. exact (GroupCoeq (FreeGroup_rec I (FreeGroup X) R) (FreeGroup_rec I (FreeGroup X) (fun x => @group_unit (FreeGroup X)))). Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.FreeGroup. Require Import Algebra.Groups.GroupCoeq. Require Import Spaces.Finite Spaces.List.Core. Require Import WildCat.