`{Univalence} {A A' B : AbGroup} (phi : GroupIsomorphism A A') (f : GroupHomomorphism A B) : transport (fun G => Hom G B) (equiv_path_abgroup phi) f = grp_homo_compose f (grp_iso_inverse phi). Proof. refine (transport_abgrouphomomorphism_to_const _ _ @ _). by rewrite eissect. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.