{A : Type} `{Is1Gpd A} {x y : A} {p : x $-> y} {q : y $-> x} (r : p $o q $== Id _) : p $== q^$. Proof. refine (_ $@ (cat_idl q^$)). refine (_ $@ (r $@R q^$)). exact (gpd_hh_V _ _)^$. Defined.
Require Import Basics.Overture Basics.Tactics.