X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FNaturalIsomorphisms_ch7_5.v;h=c62ba158f8a2b42cc58d15cb8043b07b3d723ecc;hp=f82dba8b3ec6f7ac5308ff3e6e9ad15fdd96e949;hb=105a7461c7531f8b4e49f34e7242021ac6bb5ebe;hpb=e928451c4c45cdbdd975bbfb229e8cc2616b8194

diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
index f82dba8..c62ba15 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.
@@ -78,6 +78,35 @@ Definition ni_comp `{C:Category}`{D:Category}
              reflexivity).
    Defined.
 
+Definition ni_respects1
+  `{A:Category}`{B:Category}
+  {Fobj}(F:Functor A B Fobj)
+  `{C:Category}
+  {G0obj}(G0:Functor B C G0obj)
+  {G1obj}(G1:Functor B C G1obj)
+  : (G0 <~~~> G1) -> ((F >>>> G0) <~~~> (F >>>> G1)).
+  intro phi.
+  destruct phi as [ phi_niso phi_comm ].
+  refine {| ni_iso := (fun a => phi_niso (Fobj a)) |}.
+  intros; simpl; apply phi_comm.
+  Defined.
+
+Definition ni_respects2
+  `{A:Category}`{B:Category}
+  {F0obj}(F0:Functor A B F0obj)
+  {F1obj}(F1:Functor A B F1obj)
+  `{C:Category}
+  {Gobj}(G:Functor B C Gobj)
+  : (F0 <~~~> F1) -> ((F0 >>>> G) <~~~> (F1 >>>> G)).
+  intro phi.
+  destruct phi as [ phi_niso phi_comm ].
+  refine {| ni_iso := fun a => (@functors_preserve_isos _ _ _ _ _ _ _ G) _ _ (phi_niso a) |}.
+  intros; simpl.
+  setoid_rewrite fmor_preserves_comp.
+  apply fmor_respects.
+  apply phi_comm.
+  Defined.
+
 Definition ni_respects
   `{A:Category}`{B:Category}
   {F0obj}(F0:Functor A B F0obj)