src/ReificationsIsomorphicToGeneralizedArrows.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationsIsomorphicToGeneralizedArrows:                                                                                    *)
   3 (*                                                                                                                               *)
   4 (*   The category of generalized arrows and the category of reifications are isomorphic categories.                              *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import Functors_ch1_4.
  13 Require Import Isomorphisms_ch1_5.
  14 Require Import ProductCategories_ch1_6_1.
  15 Require Import OppositeCategories_ch1_6_2.
  16 Require Import Enrichment_ch2_8.
  17 Require Import Subcategories_ch7_1.
  18 Require Import NaturalTransformations_ch7_4.
  19 Require Import NaturalIsomorphisms_ch7_5.
  20 Require Import MonoidalCategories_ch7_8.
  21 Require Import Coherence_ch7_8.
  22 Require Import Enrichment_ch2_8.
  23 Require Import RepresentableStructure_ch7_2.
  24 Require Import Reification.
  25 Require Import GeneralizedArrow.
  26 Require Import GeneralizedArrowFromReification.
  27 Require Import ReificationFromGeneralizedArrow.
  28 Require Import ReificationCategory.
  29 Require Import GeneralizedArrowCategory.
  30 Require Import ReificationCategory.
  31 Require Import ReificationsAndGeneralizedArrows.
  32 Require Import WeakFunctorCategory.
  33
  34 Section ReificationsIsomorphicToGeneralizedArrows.
  35
  36     (*
  37     Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
  38       ∀A : enr_v_mon s0,
  39      garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A))
  40      ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A.
  41      *)
  42
  43     Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
  44       (step1_functor s0 s1 r01 >>>>
  45         InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
  46       ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
  47       admit.
  48       Defined.
  49
  50     Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
  51       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
  52       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
  53       intro GA.
  54       destruct GA; [ apply roi_id | idtac ].
  55       apply roi_reif.
  56       apply reification_from_garrow.
  57       apply g.
  58       Defined.
  59
  60     (* I tried really hard to avoid this *)
  61     Require Import Coq.Logic.Eqdep.
  62
  63     Inductive Heq : forall {A}{B}, A -> B -> Prop :=
  64       heq : forall {A} (a:A), Heq a a.
  65
  66     Lemma invert_ga' : forall (a b: SMME)
  67       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
  68       (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
  69       intros.
  70       destruct f.
  71       left; apply heq.
  72       subst; right.
  73       exists g.
  74       apply heq.
  75       Defined.
  76
  77     Lemma invert_ga : forall (a: SMME)
  78       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
  79       (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
  80       intros.
  81       set (invert_ga' a a f (refl_equal a)) as q.
  82       destruct q.
  83       left.
  84       inversion H.
  85       apply inj_pairT2 in H2.
  86       apply inj_pairT2 in H1.
  87       subst; auto.
  88       right.
  89       destruct H.
  90       exists x.
  91       inversion H.
  92       apply inj_pairT2 in H2.
  93       apply inj_pairT2 in H1.
  94       subst; auto.
  95       Qed.
  96
  97     Lemma invert_reif' : forall (a b: SMME)
  98       (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
  99       (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
 100       intros.
 101       destruct f.
 102       left; apply heq.
 103       subst; right.
 104       exists r.
 105       apply heq.
 106       Defined.
 107
 108     Lemma invert_reif : forall (a: SMME)
 109       (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
 110       (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
 111       intros.
 112       set (invert_reif' a a f (refl_equal a)) as q.
 113       destruct q.
 114       left.
 115       inversion H.
 116       apply inj_pairT2 in H2.
 117       apply inj_pairT2 in H1.
 118       subst; auto.
 119       right.
 120       destruct H.
 121       exists x.
 122       inversion H.
 123       apply inj_pairT2 in H2.
 124       apply inj_pairT2 in H1.
 125       subst; auto.
 126       Qed.
 127
 128     Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
 129       refine {| fmor := fun a b f => M1 f |}.
 130       intros.
 131         unfold hom in *.
 132         unfold eqv in *.
 133         simpl in *.
 134         destruct f.
 135         set (invert_ga _ f') as q.
 136         destruct q; subst.
 137         apply if_id.
 138         simpl in *.
 139         destruct H0; subst.
 140         apply H.
 141         simpl in *.
 142         destruct f'; simpl in *.
 143         apply H.
 144         apply H.
 145       intros; simpl.
 146         apply if_id.
 147       intros.
 148         simpl.
 149         destruct f; simpl.
 150         apply if_id.
 151         destruct g; simpl.
 152         apply if_id.
 153         unfold mf_f; simpl.
 154         apply (if_associativity
 155           ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
 156         Defined.
 157
 158     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
 159       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
 160       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
 161       intro RE.
 162       destruct RE; [ apply gaoi_id | idtac ].
 163       apply gaoi_ga.
 164       apply (garrow_from_reification s1 s2 r).
 165       Defined.
 166
 167     Lemma M2_respects :
 168       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
 169          f ~~ f' ->
 170          M2 a b f ~~ M2 a b f'.
 171       intros.
 172         unfold hom in *.
 173         unfold eqv in *.
 174         simpl in *.
 175         destruct f.
 176         set (invert_reif _ f') as q.
 177         destruct q; subst.
 178         apply if_id.
 179         simpl in *.
 180         destruct H0; subst.
 181         simpl in *.
 182         unfold garrow_functor.
 183         unfold step2_functor.
 184         apply (if_comp H).
 185         clear H.
 186         apply (if_comp (@step1_niso _ smme _ _ smme x)).
 187         apply if_inv.
 188         apply (@roundtrip_lemma _ smme _ _ smme x).
 189       simpl in *.
 190         destruct f'; simpl in *.
 191         apply if_inv.
 192         apply if_inv in H.
 193         apply (if_comp H).
 194         clear H.
 195         unfold garrow_functor.
 196         unfold step2_functor.
 197         apply (if_comp (@step1_niso _ smme _ _ smme r)).
 198         apply if_inv.
 199         apply (@roundtrip_lemma _ smme _ _ smme r).
 200       simpl in *.
 201         unfold garrow_functor.
 202         unfold step2_functor.
 203         apply if_inv in H.
 204         set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
 205         set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
 206         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
 207         apply if_inv.
 208         apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
 209         apply yy'.
 210         Qed.
 211
 212     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
 213       refine {| fmor := fun a b f => M2 _ _ f |}.
 214       apply M2_respects.
 215       intros; simpl; apply if_id.
 216       intros.
 217         simpl.
 218         destruct f; simpl.
 219         apply if_id.
 220         destruct g; simpl.
 221         apply if_id.
 222         unfold mf_f; simpl.
 223         apply (if_respects
 224           (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
 225           (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
 226           (G0:=(RepresentableFunctor s2 (mon_i s2)))
 227           (G1:=(RepresentableFunctor s2 (mon_i s2))));
 228         [ idtac | apply if_id ].
 229         eapply if_comp.
 230         idtac.
 231         apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
 232         Set Printing Coercions.
 233         idtac.
 234         unfold garrow_functor at 1.
 235         unfold step2_functor at 1.
 236         set (roundtrip_lemma'
 237           (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
 238           (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
 239           (step1_functor (smme_see s1) (smme_mee s0) r)
 240         ) as q.
 241         set (if_respects
 242           (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
 243           (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
 244           q (if_id _)) as q'.
 245         apply (if_comp q').
 246         Unset Printing Coercions.
 247         clear q' q.
 248         unfold garrow_functor at 2.
 249         unfold garrow_functor at 1.
 250         eapply if_comp.
 251         eapply if_inv.
 252         apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
 253         apply (if_respects
 254           (G0:=step2_functor s2)
 255           (G1:=step2_functor s2)); [ idtac | apply if_id ].
 256         apply step1_lemma.
 257         Defined.
 258
 259     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
 260       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
 261       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 262         unfold hom in *.
 263         set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
 264         destruct f; simpl in *.
 265         apply H.
 266         apply if_inv.
 267         apply (if_comp (if_inv H)).
 268         clear H.
 269         unfold mf_f in q.
 270         apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
 271           (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
 272         apply q.
 273         apply if_id.
 274
 275       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 276         unfold hom in *.
 277         set (@roundtrip_reification_to_reification _ a _ _ b) as q.
 278         destruct f; simpl.
 279         apply H.
 280         apply if_inv.
 281         apply (if_comp (if_inv H)).
 282         clear H.
 283         simpl.
 284         unfold mf_f; simpl.
 285         simpl in q.
 286         unfold mf_f in q.
 287         simpl in q.
 288         apply q.
 289         Qed.
 290
 291 End ReificationsIsomorphicToGeneralizedArrows.