ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}. Proof. snrapply (Build_AbGroup (grp_ext@{u v} B A)). intros E F. strip_truncations; cbn. apply ap. apply baer_sum_commutative. Defined.
Require Import Basics Types Truncations.Core. Require Import Pointed WildCat. Require Import Truncations.SeparatedTrunc. Require Import AbelianGroup AbHom AbProjective. Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.