((_, _); (AH o AG) o AF) = ((_, _); AH o (AG o AF)) :> AdjunctionWithFunctors B E. Proof. apply path_sigma_uncurried; simpl. (exists (path_prod' (Functor.Composition.Laws. _ _ _) (symmetry _ _ (Functor.Composition.Laws. _ _ _)))); Adjoint.Composition.LawsTactic.law_t. Qed.
Require Import Category.Core Functor.Core. Require Import Adjoint.Composition.Core Adjoint.Core. Require Import Types.Sigma Types.Prod.