`{Univalence} {A B B' : AbGroup} (p : B = B') (f : GroupHomomorphism A B) : transport (Hom A) p f = grp_homo_compose (equiv_path_abgroup^-1 p) f. Proof. induction p. 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.