C : @Adjunction C C 1 1 := @Build_AdjunctionUnitCounit C C 1 1 1 1 (fun _ => identity_identity _ _) (fun _ => identity_identity _ _).
Require Import Category.Core. Require Import Functor.Identity NaturalTransformation.Identity. Require Import Adjoint.UnitCounit Adjoint.Core.