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