{B C : Type} `{Is1Cat B, Is1Gpd C} `{IsPointed B, IsPointed C} (F G : B -->* C) : (F $=>* G) -> (G $=>* F). Proof. intros [h p]. exists (fun x => (h x)^$). refine (gpd_rev2 p $@ _). refine (gpd_rev_pp _ _ $@ _). refine (_ $@L _). apply gpd_rev_rev. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.