proposition: Lemma φ_in_terms_of_ε `(g: x ⟶ G a): φ⁻¹ g = ε a ◎ fmap F g.
proof: Proof. rewrite <- (left_identity g) at 1. apply φ_adjunction_natural_right_inv. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories MathClasses.misc.workaround_tactics MathClasses.theory.jections