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.