(a : a_part) (b : b_part a) := Eval simpl in forall x, (((left_identity_natural_transformation_1 _) o (p_identity_of G _ oR _) o (B_to_A _1 b x) o (_ oL (p_identity_of F _)^-1) o (left_identity_natural_transformation_2 _)) = 1)%natural_transformation.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Pseudofunctor.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import NaturalTransformation.Identity.