{G H : ZeroGpd} (f : G $<~> H) {x y : G} (h : equiv_fun_0gpd f x $== equiv_fun_0gpd f y) : x $== y. Proof. exact ((cat_eissect f x)^$ $@ fmap (equiv_fun_0gpd f^-1$) h $@ cat_eissect f y). Defined.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd