`{Univalence} {A A' B : AbGroup} (p : A = A') (f : GroupHomomorphism A B) : transport (fun G => Hom G B) p f = grp_homo_compose f (grp_iso_inverse (equiv_path_abgroup^-1 p)). Proof. induction p; cbn. by apply equiv_path_grouphomomorphism. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.