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