C D (F F' F'' : Functor C D) (T' : F' = F'') (T : F = F') : ((Category.Morphisms.idtoiso (_ -> _) T' : morphism _ _ _) o (Category.Morphisms.idtoiso (_ -> _) T : morphism _ _ _))%natural_transformation = (Category.Morphisms.idtoiso (_ -> _) (T @ T')%path : morphism _ _ _). Proof. path_natural_transformation; path_induction; simpl; auto with morphism. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import NaturalTransformation.Composition.Core. Require Import Functor.Composition.Core. Require Import Category.Morphisms. Require Import FunctorCategory.Core. Require Import NaturalTransformation.Paths. Require Import Basics.Tactics.