adjunction_sig <~> (F -| G). Proof. issig. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core Functor.Identity. Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths. Require Import Types Trunc. Require Import Basics.Tactics.