path_adjunction' (A A' : F -| G) : unit A = unit A' -> counit A = counit A' -> A = A'. Proof. intros. destruct A, A'; simpl in *. path_induction. f_ap; exact (center _). 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.