(A A' : F -| G) : components_of (unit A) == components_of (unit A') -> components_of (counit A) == components_of (counit A') -> A = A'. Proof. intros. apply '; apply path_natural_transformation; assumption. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core Functor.Identity. Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths. Require Import Types Trunc. Require Import Basics.Tactics.