(P : Abel -> Type) `{forall x, IsHProp (P x)} (a : forall x, P (abel_in x)) : forall (x : Abel), P x. Proof. srapply Trunc_ind. srapply Coeq_ind_hprop. exact a. 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.