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