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