{I : Type} {G : ZeroGpd} {H : I -> ZeroGpd} : (forall i, G $-> H i) <~> (G $-> prod_0gpd I H). Proof. snrapply Build_Equiv. { intro f. snrapply Build_Morphism_0Gpd. 1: exact (fun x i => f i x). snrapply Build_Is0Functor; cbn beta. intros x y p i; simpl. exact (fmap (f i) p). } snrapply Build_IsEquiv. - intro f. intros i. exact (prod_0gpd_pr i $o f). - intro f. reflexivity. - intro f. reflexivity. - reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd