From 422dab8d300548c294b95c0f4bbf27aecadbd745 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 24 Apr 2011 00:00:24 -0700 Subject: [PATCH] add inverse form of ni_commutes --- src/NaturalIsomorphisms_ch7_5.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v index c62ba15..ce97ce6 100644 --- a/src/NaturalIsomorphisms_ch7_5.v +++ b/src/NaturalIsomorphisms_ch7_5.v @@ -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 *) -- 1.7.10.4