{A} `{HasEquivs A} {a b} (f : a $<~> b) (g : b $-> a) (p : f $o g $== Id b) : cate_fun f^-1$ $== g. Proof. refine ((cat_idr _)^$ $@ _). refine ((_ $@L p^$) $@ _). refine (cat_assoc_opp _ _ _ $@ _). refine (cate_issect f $@R _ $@ _). apply cat_idl. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.