`{Univalence} {B A : AbGroup@{u}} {E F : AbSES B A} (p : abses_path_data_iso E F) : (equiv_path_abses_iso p)^ = equiv_path_abses_iso (abses_path_data_inverse p). Proof. revert p. equiv_intro (equiv_path_abses_iso (E:=E) (F:=F))^-1 p; induction p. refine (ap _ (eisretr _ _) @ _); symmetry. nrefine (ap (equiv_path_abses_iso o abses_path_data_inverse) equiv_path_absesV_1 @ _). refine (ap equiv_path_abses_iso gpd_strong_rev_1 @ _). exact 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.