remove unproven step1_lemma (it has a proof now)

[coq-hetmet.git] / src / BijectionLemma.v

diff --git a/src/BijectionLemma.v b/src/BijectionLemma.v
new file mode 100644 (file)
index 0000000..f63cf17
--- /dev/null
+++ b/src/BijectionLemma.v
@@ -0,0 +1,71 @@
+(*********************************************************************************************************************************)
+(* Bijection Lemma                                                                                                               *)
+(*                                                                                                                               *)
+(*    Used in the proof that the mapping between the category of reifications and category of generalized arrows is in fact      *)
+(*    a functor                                                                                                                  *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+
+Section BijectionLemma.
+
+  (* given two categories with (for simplicity) the same objects *)
+  Context  {Obj:Type}.
+  Context  {CHom}{C:Category Obj CHom}.
+  Context  {DHom}{D:Category Obj DHom}.
+
+  (* and a functor which is (for simplicity) identity on objects *)
+  Context  {F:Functor C D (fun x => x)}.
+
+  (* and a mapping in the opposite direction, which respects equivalence *)
+  Context  {M:forall x y, (x~~{D}~~>y) -> (x~~{C}~~>y)}.
+  Implicit Arguments M [ [x] [y] ].
+  Context  {M_respects:forall x y, forall (f g:x~~{D}~~>y), f~~g -> M f ~~ M g}.
+
+  Add Parametric Morphism (x y:Obj) : (@M x y)
+  with signature ((@eqv D _ D x y) ==> (@eqv C _ C x y)) as parametric_morphism_fmor''.
+    intros; apply M_respects; auto.
+    Defined.
+
+  (*
+   * If the functor and the mapping form a bijection, then the fact
+   * that the functor preserves composition forces the mapping to do so
+   * as well
+   *)
+
+  Lemma bijection_lemma :
+    (forall A B, forall f:(A~~{C}~~>B), M (F \ f) ~~ f) ->
+    (forall A B, forall f:(A~~{D}~~>B), F \ (M f) ~~ f) ->
+    forall A B C, forall f:(A~~{D}~~>B), forall g:(B~~{D}~~>C), M f >>> M g ~~ M (f >>> g).
+  
+    intro lem1.
+    intro lem2.
+    intros.
+    rewrite <- (lem2 _ _ f).
+    rewrite <- (lem2 _ _ g).
+
+    set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q.
+    rewrite q.
+    rewrite lem1.
+    rewrite lem1.
+    rewrite lem1.
+    reflexivity.
+    Qed.
+
+End BijectionLemma.