{A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a. Proof. simple refine (cate_adjointify _ _ _ _). - exact (' a b f). - exact f. - exact (cate_issect' a b f). - exact (cate_isretr' a b f). Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.