a b c : abel_in (a * (b * c)) = abel_in (a * (c * b)). Proof. apply (ap tr). exact (cglue (a, b, c)). Defined.
Require Import Basics Types Truncations.Core. Require Import Cubical.DPath WildCat. Require Import Colimits.Coeq. Require Import Algebra.AbGroups.AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.