{A : Type} `{HasEquivs A} `{!HasMorExt A} {a b : A} : (b $<~> a) -> (opyon1 a $<~> opyon1 b). Proof. intro e. snrapply Build_NatEquiv. - intros c. exact (equiv_precompose_cat_equiv e). - rapply is1natural_opyoneda. 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.