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