cate_inv_compose' {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c) : cate_fun (f $oE e)^-1$ $== e^-1$ $o f^-1$. Proof. nrefine (_ $@ cate_buildequiv_fun _). nrapply cate_inv_compose. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.