proposition: Corollary exp_out_inj {x y z : C} (f g : F x ~> F (z^y)) : exp_out ∘ f ≈ exp_out ∘ g ↔ f ≈ g.
proof: Proof. split; intros Hexp. - rewrite <- id_left. rewrite <- exp_in_out. rewrite <- comp_assoc. rewrite Hexp. rewrite comp_assoc. autorewrite with functors; cat. - subst. rewrite Hexp. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian