NaturalTransformation ((F' o F) o (G o G')) 1. Proof. pose (counit A) as eps. pose (counit A') as eps'. refine ((fun (T : NaturalTransformation _ _) (U : NaturalTransformation _ _) => eps' o U o (F' oL eps oR G') o T) _ _); 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.