{A} `{HasEquivs A} {a b} (f : a $<~> b) : f^-1$ $o f $== Id a. Proof. refine (_ $@ ' a b f). refine (_ $@R f). apply cate_buildequiv_fun'. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.