{A : Type} {B : A -> Type} `{forall x, IsGraph (B x)} (F G : forall (x : A), B x) := forall (a : A), F a $-> G a.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.