src/ReificationsIsomorphicToGeneralizedArrows.v

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