`{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. refine (transport_abgrouphomomorphism_from_const _ _ @ _). by rewrite eissect. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.