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