proposition: Corollary fmap_counit_unit {x} : fmap[U] ε ∘ η ≈ id[U x].
proof: Proof. unfold unit, counit. rewrite <- to_adj_nat_r; cat. sapply (@iso_to_from Sets _ _ (@adj _ (U x) x)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets