{X Y A B : Group} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B) : grp_prod_corec g0 g1 $o f $== grp_prod_corec (g0 $o f) (g1 $o f) := fun _ => idpath.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.