{A} `{HasEquivs A} {a b} (f : a $<~> b) : f $o f^-1$ $== Id b := cate_issect (A:=A^op) (b:=a) (a:=b) f.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.