(P : Abel -> Type) `{forall x, IsHSet (P x)} (a : forall x, P (abel_in x)) (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y)))) (x y z : G) : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z. Proof. refine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _). rapply Coeq_ind_beta_cglue. 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.