Processing math: 100%

Library CT.Instance.NaturalTransformation.NaturalIsomorphism

Require Import CT.Category.
Require Import CT.Functor.
Require Import CT.Isomorphism.
Require Import CT.Instance.Category.FunctorCategory.

Natural Isomorphism

Given the functor category {C, D}, a natural isomorphism is an isomorphism between two objects of this category (i.e., functors between C and D).
Section NaturalIsomorphism.
  Context {C D : Category}.
  Context (F G : Functor C D).
  Definition NaturalIsomorphism := @Isomorphism (FunctorCategory C D) F G.
End NaturalIsomorphism.