{B C : Type} `{Is1Cat B, Is1Gpd C} `{IsPointed B, IsPointed C} (F G : B -->* C) := {eta : F $=> G & eta (point _) $== bp_pointed F $@ (bp_pointed G)^$}.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.