Definition group_varspec : varspec group_signature := make_varspec group_signature natset (λ _, group_sort).
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.