+(* 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.
+