proposition: Lemma transport_iso_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup} (phi : GroupIsomorphism B B') (f : GroupHomomorphism A B) : transport (Hom A) (equiv_path_abgroup phi) f = grp_homo_compose phi f.
proof: Proof. refine (transport_abgrouphomomorphism_from_const _ _ @ _). by rewrite eissect. 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