Suppose is an adjunction, and is fully faithful, then counit is an isomorphism
Proof [local-2]
Forward direction [local-0]
To prove counit is an isomorphism, we need to find an inverse and show pre and post composition of them are identity. Let , then we have two targets
-
Apply to get
hence the target is , right triangle fills the target.
-
Use counit naturality on to get
Therefore, we have target , left triangle fills the target.
Backward direction [local-1]
For is faithful, we want to know if then . We first obtain two equations via naturality of counit:
Replace with then we have , counit is an isomorphism and hence left-cancellable, .
For is full, we want to show every there is a such that . Let (where is the hom-set equivalence of adjunction), this is same as asking
because isomorphism property, we have
now we use isomorphism to cancel right, so .