--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
Require Import ReificationCategory.
Require Import ReificationsAndGeneralizedArrows.
Require Import WeakFunctorCategory.
+Require Import BijectionLemma.
Section ReificationsIsomorphicToGeneralizedArrows.
- Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
- (step1_functor s0 s1 r01 >>>>
- InclusionFunctor (enr_v s1) (FullImage (HomFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
- ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
- admit.
- Defined.
-
Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
apply (garrow_from_reification s1 s2 r).
Defined.
+ Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
+ (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
+ (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
+ generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
+ unfold hom in *.
+ set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+ destruct f; simpl in *.
+ apply H.
+ apply if_inv.
+ apply (if_comp (if_inv H)).
+ clear H.
+ unfold mf_f in q.
+ apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
+ (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
+ apply q.
+ apply if_id.
+ Qed.
+
+
+ Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
+ (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
+ (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
+ reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
+ unfold hom in *.
+ set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+ destruct f; simpl.
+ apply H.
+ apply if_inv.
+ apply (if_comp (if_inv H)).
+ clear H.
+ simpl.
+ unfold mf_f; simpl.
+ simpl in q.
+ unfold mf_f in q.
+ simpl in q.
+ apply q.
+ Qed.
+
Lemma M2_respects :
forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
f ~~ f' ->
unfold garrow_functor.
unfold step2_functor.
apply if_inv in H.
- set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
- set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
apply if_inv.
apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
- apply yy'.
+ apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
Qed.
Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
refine {| fmor := fun a b f => M2 _ _ f |}.
apply M2_respects.
intros; simpl; apply if_id.
- intros.
- simpl.
- destruct f; simpl.
- apply if_id.
- destruct g; simpl.
- apply if_id.
- unfold mf_f; simpl.
- apply (if_respects
- (F0:=((garrow_functor s1 s0 r >>>> HomFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
- (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
- (G0:=(HomFunctor s2 (mon_i s2)))
- (G1:=(HomFunctor s2 (mon_i s2))));
- [ idtac | apply if_id ].
- eapply if_comp.
- idtac.
- apply (if_associativity (garrow_functor s1 s0 r) (HomFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
- idtac.
- unfold garrow_functor at 1.
- unfold step2_functor at 1.
- set (roundtrip_lemma'
- (HomFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
- (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
- (step1_functor (smme_see s1) (smme_mee s0) r)
- ) as q.
- set (if_respects
- (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
- (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
- q (if_id _)) as q'.
- apply (if_comp q').
- clear q' q.
- unfold garrow_functor at 2.
- unfold garrow_functor at 1.
- eapply if_comp.
- eapply if_inv.
- apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
- apply (if_respects
- (G0:=step2_functor s2)
- (G1:=step2_functor s2)); [ idtac | apply if_id ].
- apply step1_lemma.
- Defined.
+ intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
+ apply M2_respects; auto.
+ unfold fmor; simpl.
+ apply (@eqv1 _ _ f0 f0).
+ apply if_id.
+ unfold fmor; simpl.
+ apply (@eqv2 _ _ f0 f0).
+ apply if_id.
+ Defined.
Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
- unfold hom in *.
- set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
- destruct f; simpl in *.
- apply H.
- apply if_inv.
- apply (if_comp (if_inv H)).
- clear H.
- unfold mf_f in q.
- apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
- (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
- apply q.
- apply if_id.
-
+ apply (eqv1 _ _ f f'); auto.
unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
- unfold hom in *.
- set (@roundtrip_reification_to_reification _ a _ _ b) as q.
- destruct f; simpl.
- apply H.
- apply if_inv.
- apply (if_comp (if_inv H)).
- clear H.
- simpl.
- unfold mf_f; simpl.
- simpl in q.
- unfold mf_f in q.
- simpl in q.
- apply q.
- Qed.
+ apply (eqv2 _ _ f f'); auto.
+ Qed.
End ReificationsIsomorphicToGeneralizedArrows.