proposition: Lemma φ_adjunction_natural_right_inv `(g: c ⟶ G d) `(h: c' ⟶ c): φ⁻¹ (g ◎ h) = φ⁻¹ g ◎ fmap F h.
proof: Proof. Proof with try reflexivity; try apply _. intros. apply (injective φ). rewrite surjective_applied... rewrite φ_adjunction_natural_right... 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