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