proposition: Lemma path_adjunction' (A A' : F -| G) : unit A = unit A' -> counit A = counit A' -> A = A'.
proof: Proof. intros. destruct A, A'; simpl in *. path_induction. f_ap; exact (center _). Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core Functor.Identity Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths Types Trunc Basics.Tactics