1 (*********************************************************************************************************************************)
4 (* Used in the proof that the mapping between the category of reifications and category of generalized arrows is in fact *)
7 (*********************************************************************************************************************************)
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.
26 Section BijectionLemma.
28 (* given two categories with (for simplicity) the same objects *)
30 Context {CHom}{C:Category Obj CHom}.
31 Context {DHom}{D:Category Obj DHom}.
33 (* and a functor which is (for simplicity) identity on objects *)
34 Context {F:Functor C D (fun x => x)}.
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}.
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.
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
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).
60 rewrite <- (lem2 _ _ f).
61 rewrite <- (lem2 _ _ g).
63 set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q.