proposition: Lemma φ_in_terms_of_η `(f: F x ⟶ a): φ f = fmap G f ◎ η x.
proof: Proof. rewrite <- (right_identity f) at 1. rewrite φ_adjunction_natural_left. reflexivity. apply _. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories MathClasses.misc.workaround_tactics MathClasses.theory.jections