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