{C D : Type} (F : C -> D) (G : D -> C) `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} (e : forall x, NatEquiv (opyon (F x)) (opyon x o G)) (is1nat_e : forall y, Is1Natural (A := C^op) (yon y o F) (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _) (yon (G y)) (fun x => e _ y)) : Adjunction F G. Proof. snrapply Build_Adjunction. 1: exact (fun x => e x). 1: exact is1nat_e. intros x; apply (is1natural_natequiv (e x)). Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Equiv. Require Import WildCat.Prod. Require Import WildCat.Opposite. Require Import WildCat.Yoneda. Require Import WildCat.FunctorCat. Require Import WildCat.Universe. Require Import Types.Prod.