proposition: Lemma transport_abgrouphomomorphism_to_const `{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: Proof. induction p; cbn. by apply equiv_path_grouphomomorphism. Defined.
imports: Basics Types Classes.interfaces.canonical_names (Zero, zero) Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative) Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.QuotientGroup WildCat