{x0 x : PreCategory} {x4 : Functor x0 x0} {x5 : x4 = 1%functor} {x2 x3 : Functor x0 x} {x6 : x2 = x3} {x7 : x2 = (x3 o x4)%functor} (H0' : P x0) (H' : P x) : (x3 oL (Category.Morphisms.idtoiso (x0 -> x0) x5 : morphism _ _ _) o (Category.Morphisms.idtoiso (x0 -> x) x7 : morphism _ _ _))%natural_transformation = ((NaturalTransformation.Composition.Laws.right_identity_natural_transformation_2 x3) o (Category.Morphisms.idtoiso (x0 -> x) x6 : morphism _ _ _))%natural_transformation. Proof. clear F. simpl; pseudofunctor_t. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import Functor.Identity. Require Import Pseudofunctor.Core. Require Import Cat.Core. Require Import FunctorCategory.Core. Require Import FunctorCategory.Morphisms NaturalTransformation.Isomorphisms. Require Import Category.Morphisms NaturalTransformation.Paths. Require Import Basics.PathGroupoids Basics.Trunc.