Group. Proof. snrapply (Build_Group amal_type); repeat split; exact _. Defined.
Require Import Basics Types. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. Require Import WildCat.