`{Univalence} {B A : AbGroup@{u}} {E : AbSES B A} : (@equiv_path_abses_iso _ B A E E)^-1 idpath = Id E. Proof. apply moveR_equiv_M; symmetry. apply equiv_path_abses_1. Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.