fact: Definition functor_ab_biprod {A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B') : ab_biprod A B $-> ab_biprod A' B' := (ab_biprod_corec (f $o ab_biprod_pr1) (g $o ab_biprod_pr2)).
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse