{A B : Type} `{Is01Cat B} {F G K : A -> B} (gamma : G $=> K) (alpha : F $=> G) : F $=> K := fun a => gamma a $o alpha a.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.