+(*********************************************************************************************************************************)
+(* 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.