{A : Type} `{HasEquivs A} `{!Is1Cat_Strong A} {a b : A} : (opyon1 a $<~> opyon1 b) -> (b $<~> a). Proof. intros f. refine (cate_adjointify (f a (Id a)) (f^-1$ b (Id b)) _ _); apply GpdHom_path; cbn in *. - refine ((isnat_natequiv (natequiv_inverse f) (f a (Id a)) (Id b))^ @ _); cbn. refine (_ @ cate_issect (f a) (Id a)); cbn. apply ap. srapply cat_idr_strong. - refine ((isnat_natequiv f (f^-1$ b (Id b)) (Id a))^ @ _); cbn. refine (_ @ cate_isretr (f b) (Id b)); cbn. apply ap. srapply cat_idr_strong. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Universe. Require Import WildCat.Opposite. Require Import WildCat.FunctorCat. Require Import WildCat.NatTrans. Require Import WildCat.Prod. Require Import WildCat.Bifunctor. Require Import WildCat.ZeroGroupoid.