grp_pullback_corec' (X : Group) : {b : X $-> B & { c : X $-> C & f o b == g o c}} -> (X $-> grp_pullback). Proof. intros [b [c p]]; exact (grp_pullback_corec b c p). Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.