NaturalTransformation 1 ((G o G') o (F' o F)). Proof. pose (unit A) as eta. pose (unit A') as eta'. refine ((fun (T : NaturalTransformation _ _) (U : NaturalTransformation _ _) => T o (G oL eta' oR F) o U o eta) _ _); NaturalTransformation.Composition.Laws.nt_solve_associator. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import Functor.Identity. Require Import Adjoint.UnitCounit Adjoint.Core. Require Import HoTT.Tactics. Require Import Basics.Tactics.