proposition: Lemma φ_adjunction_natural_left_inv `(g: c ⟶ G d) `(k: d ⟶ d'): φ⁻¹ (fmap G k ◎ g) = k ◎ φ⁻¹ g.
proof: Proof. Proof with try reflexivity; try apply _. intros. apply (injective φ). rewrite surjective_applied... rewrite φ_adjunction_natural_left... rewrite surjective_applied... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories MathClasses.misc.workaround_tactics MathClasses.theory.jections