{Z X Y A B : AbGroup} (f0 : Z $-> X) (f1 : Z $-> Y) (g0 : X $-> A) (g1 : Y $-> B) : functor_ab_biprod g0 g1 $o ab_biprod_corec f0 f1 $== ab_biprod_corec (g0 $o f0) (g1 $o f1) := fun _ => idpath. Global Instance is0bifunctor_ab_biprod : Is0Bifunctor ab_biprod. Proof. srapply Build_Is0Bifunctor'. snrapply Build_Is0Functor. intros [A B] [A' B'] [f g]. exact (functor_ab_biprod f g). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.