(I : Type) (G : I -> ZeroGpd) : ZeroGpd. Proof. rapply (Build_ZeroGpd (forall i, G i)). Defined.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd