From: Adam Megacz Date: Sun, 24 Apr 2011 07:00:24 +0000 (-0700) Subject: add inverse form of ni_commutes X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=422dab8d300548c294b95c0f4bbf27aecadbd745 add inverse form of ni_commutes --- 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 *)