clean up demo code
[coq-hetmet.git] / src / BijectionLemma.v
1 (*********************************************************************************************************************************)
2 (* Bijection Lemma                                                                                                               *)
3 (*                                                                                                                               *)
4 (*    Used in the proof that the mapping between the category of reifications and category of generalized arrows is in fact      *)
5 (*    a functor                                                                                                                  *)
6 (*                                                                                                                               *)
7 (*********************************************************************************************************************************)
8
9 Generalizable All Variables.
10 Require Import Preamble.
11 Require Import General.
12 Require Import Categories_ch1_3.
13 Require Import Functors_ch1_4.
14 Require Import Isomorphisms_ch1_5.
15 Require Import ProductCategories_ch1_6_1.
16 Require Import OppositeCategories_ch1_6_2.
17 Require Import Enrichment_ch2_8.
18 Require Import Subcategories_ch7_1.
19 Require Import NaturalTransformations_ch7_4.
20 Require Import NaturalIsomorphisms_ch7_5.
21 Require Import MonoidalCategories_ch7_8.
22 Require Import Coherence_ch7_8.
23 Require Import Enrichment_ch2_8.
24 Require Import RepresentableStructure_ch7_2.
25
26 Section BijectionLemma.
27
28   (* given two categories with (for simplicity) the same objects *)
29   Context  {Obj:Type}.
30   Context  {CHom}{C:Category Obj CHom}.
31   Context  {DHom}{D:Category Obj DHom}.
32
33   (* and a functor which is (for simplicity) identity on objects *)
34   Context  {F:Functor C D (fun x => x)}.
35
36   (* and a mapping in the opposite direction, which respects equivalence *)
37   Context  {M:forall x y, (x~~{D}~~>y) -> (x~~{C}~~>y)}.
38   Implicit Arguments M [ [x] [y] ].
39   Context  {M_respects:forall x y, forall (f g:x~~{D}~~>y), f~~g -> M f ~~ M g}.
40
41   Add Parametric Morphism (x y:Obj) : (@M x y)
42   with signature ((@eqv D _ D x y) ==> (@eqv C _ C x y)) as parametric_morphism_fmor''.
43     intros; apply M_respects; auto.
44     Defined.
45
46   (*
47    * If the functor and the mapping form a bijection, then the fact
48    * that the functor preserves composition forces the mapping to do so
49    * as well
50    *)
51
52   Lemma bijection_lemma :
53     (forall A B, forall f:(A~~{C}~~>B), M (F \ f) ~~ f) ->
54     (forall A B, forall f:(A~~{D}~~>B), F \ (M f) ~~ f) ->
55     forall A B C, forall f:(A~~{D}~~>B), forall g:(B~~{D}~~>C), M f >>> M g ~~ M (f >>> g).
56   
57     intro lem1.
58     intro lem2.
59     intros.
60     rewrite <- (lem2 _ _ f).
61     rewrite <- (lem2 _ _ g).
62
63     set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q.
64     rewrite q.
65     rewrite lem1.
66     rewrite lem1.
67     rewrite lem1.
68     reflexivity.
69     Qed.
70
71 End BijectionLemma.