Coercion ni_iso : NaturalIsomorphism >-> Funclass.
Notation "F <~~~> G" := (@NaturalIsomorphism _ _ _ _ _ _ _ _ F G) : category_scope.
+(* same as ni_commutes, but phrased in terms of inverses *)
+Lemma ni_commutes' `(ni:NaturalIsomorphism) : forall `(f:A~>B), F2 \ f >>> #(ni_iso ni B)⁻¹ ~~ #(ni_iso ni A)⁻¹ >>> F1 \ f.
+ intros.
+ apply iso_shift_right'.
+ setoid_rewrite <- associativity.
+ symmetry.
+ apply iso_shift_left'.
+ symmetry.
+ apply ni_commutes.
+ Qed.
+
(* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
(* every natural iso is invertible, and that inverse is also a natural iso *)