NatEquiv (A := C^op * D) (fun01_compose fun01_hom (fun01_profunctor F idmap)) (fun01_compose fun01_hom (fun01_profunctor idmap G)). Proof. snrapply Build_NatEquiv. 1: intros [x y]; exact (equiv_adjunction adj x y). snrapply Build_Is1Natural. intros [a b] [a' b'] [f g] K. refine (_ @ ap (fun x : a $-> G b' => x $o f) (is1natural_equiv_adjunction_r adj a b b' g K)). exact (is1natural_equiv_adjunction_l adj _ _ _ f (g $o K)). 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.