((_, _); 1 o A) = ((_, _); A) :> AdjunctionWithFunctors C D. Proof. apply path_sigma_uncurried; simpl. (exists (path_prod' (Functor.Composition.Laws. _) (Functor.Composition.Laws.right_identity _))). Adjoint.Composition.LawsTactic.law_t. Qed.
Require Import Category.Core Functor.Core. Require Import Adjoint.Composition.Core Adjoint.Core Adjoint.Identity. Require Import Types.Sigma Types.Prod.