`{Univalence} (B A : AbGroup@{u}) : Group. Proof. snrapply (Build_Group (Ext B A)). - intros E F. strip_truncations. exact (tr (abses_baer_sum E F)). - exact (point (Ext B A)). - unfold Negate. exact (Trunc_functor _ (abses_pullback (- grp_homo_id))). - repeat split. 1: apply istrunc_truncation. all: intro E. 1: intros F G. all: strip_truncations; unfold mon_unit, point; apply (ap tr). + symmetry; apply baer_sum_associative. + apply baer_sum_unit_l. + apply baer_sum_unit_r. + apply baer_sum_inverse_r. + apply baer_sum_inverse_l. 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.