{I : Type} {G : I -> ZeroGpd} : forall i, prod_0gpd I G $-> G i. Proof. intros i. snrapply Build_Morphism_0Gpd. 1: exact (fun f => f i). snrapply Build_Is0Functor; cbn beta. intros f g p. exact (p i). Defined.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd