X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FNaturalIsomorphisms_ch7_5.v;h=ce97ce6f9bc8ba3038fd5f435c9be85e73accf89;hp=680e743fbe312a853fd2659c32e0ac4f17eedc71;hb=422dab8d300548c294b95c0f4bbf27aecadbd745;hpb=e6eee3c9787855479899acb82cb65f9cdd0259c6

diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
index 680e743..ce97ce6 100644
--- a/src/NaturalIsomorphisms_ch7_5.v
+++ b/src/NaturalIsomorphisms_ch7_5.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
@@ -19,6 +19,17 @@ Implicit Arguments ni_commutes [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2 A B].
 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 *)