{A : Type} `{HasEquivs A} {a b : A} (e : b $<~> a) : opyon1_0gpd a $<~> opyon1_0gpd b. Proof. snrapply Build_NatEquiv. - intro c; exact (equiv_precompose_cat_equiv_0gpd e). - rapply is1natural_opyoneda_0gpd. 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.