{A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c) : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$). Proof. refine (_ $@ (compose_cate_fun _ _)^$). apply cate_inv_adjointify. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.