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