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