(x y : PreCategory) (f : Functor x y) : f oL 1 o 1 = (right_identity_natural_transformation_2 f) o @morphism_isomorphic _ _ _ (idtoiso (x -> y) (ap idmap (Functor.Composition.Laws.right_identity f))). Proof. t. Defined.
Require Import FunctorCategory.Morphisms. Require Import Category.Core Functor.Core. Require Import NaturalTransformation.Isomorphisms. Require Import NaturalTransformation.Paths. Require Import Cat.Core. Require Import Pseudofunctor.Core. Import NaturalTransformation.Identity. Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Import Category.Morphisms. Import FunctorCategory.Core. Require Import PathGroupoids.