c_part' (a : a_part) (b : b_part a) : forall (x y z : X) (m1 : morphism X y z) (m2 : morphism X x y), Type. Proof. hnf in a, b. pose (fun x y m => (b x y m : morphism _ _ _)) as bB; simpl in *. intros x y z m1 m2. exact (((associator_2 _ _ _) o (B_to_C_2 _1 bB x y z m1 m2) o (associator_1 _ _ _) o (B_to_C_1 _1 bB x y z m1 m2) o (associator_2 _ _ _)) = ((p_composition_of G _ _ _ m1 m2 oR _) o (B_to_C_3 _1 bB x y z m1 m2) o (_ oL (p_composition_of F _ _ _ m1 m2)^-1)))%natural_transformation. Defined.
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.