Definition group_axioms : eqsystem group_signature group_varspec := ⟦ 3 ⟧,, three_rec group_mul_assoc group_mul_lid group_mul_rid.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Universal.EqAlgebras.