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 PreMonoidalCategories.
  21 Require Import MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_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 Require Import BijectionLemma.
  34 Require Import Enrichments.
  35
  36 Section ReificationsIsomorphicToGeneralizedArrows.
  37
  38     Definition M1 {c1 c2 : SMMEs} :
  39       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
  40       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
  41       intro GA.
  42       destruct GA; [ apply roi_id | idtac ].
  43       apply roi_reif.
  44       apply (reification_from_garrow s1 s2 g).
  45       Defined.
  46
  47     (* I tried really hard to avoid this *)
  48     Require Import Coq.Logic.Eqdep.
  49
  50     Inductive Heq : forall {A}{B}, A -> B -> Prop :=
  51       heq : forall {A} (a:A), Heq a a.
  52
  53     Lemma invert_ga' : forall (a b: SMME)
  54       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
  55       (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
  56       intros.
  57       destruct f.
  58       left; apply heq.
  59       subst; right.
  60       exists g.
  61       apply heq.
  62       Defined.
  63
  64     Lemma invert_ga : forall (a: SMME)
  65       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
  66       (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
  67       intros.
  68       set (invert_ga' a a f (refl_equal a)) as q.
  69       destruct q.
  70       left.
  71       inversion H.
  72       apply inj_pairT2 in H2.
  73       apply inj_pairT2 in H1.
  74       subst; auto.
  75       right.
  76       destruct H.
  77       exists x.
  78       inversion H.
  79       apply inj_pairT2 in H2.
  80       apply inj_pairT2 in H1.
  81       subst; auto.
  82       Qed.
  83
  84     Lemma invert_reif' : forall (a b: SMME)
  85       (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
  86       (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
  87       intros.
  88       destruct f.
  89       left; apply heq.
  90       subst; right.
  91       exists r.
  92       apply heq.
  93       Defined.
  94
  95     Lemma invert_reif : forall (a: SMME)
  96       (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
  97       (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
  98       intros.
  99       set (invert_reif' a a f (refl_equal a)) as q.
 100       destruct q.
 101       left.
 102       inversion H.
 103       apply inj_pairT2 in H2.
 104       apply inj_pairT2 in H1.
 105       subst; auto.
 106       right.
 107       destruct H.
 108       exists x.
 109       inversion H.
 110       apply inj_pairT2 in H2.
 111       apply inj_pairT2 in H1.
 112       subst; auto.
 113       Qed.
 114
 115     Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
 116       refine {| fmor := fun a b f => M1 f |}.
 117       intros.
 118         unfold hom in *.
 119         unfold eqv in *.
 120         simpl in *.
 121         destruct f.
 122         set (invert_ga _ f') as q.
 123         destruct q; subst.
 124         apply if_id.
 125         simpl in *.
 126         destruct H0; subst.
 127         apply H.
 128         simpl in *.
 129         destruct f'; simpl in *.
 130         apply H.
 131         apply H.
 132       intros; simpl.
 133         apply if_id.
 134       intros.
 135         simpl.
 136         destruct f; simpl.
 137         apply if_id.
 138         destruct g; simpl.
 139         apply if_id.
 140         simpl.
 141         apply (if_associativity
 142           ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
 143         Defined.
 144
 145     Definition M2 (c1 c2 : SMMEs) :
 146       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
 147       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
 148       intro RE.
 149       destruct RE; [ apply gaoi_id | idtac ].
 150       apply gaoi_ga.
 151       apply (garrow_from_reification s1 (smme_mee s2) s2 r).
 152       Defined.
 153
 154     Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
 155       (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
 156       (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
 157       generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
 158         unfold hom in *.
 159         set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon b)) as q.
 160         destruct f; simpl in *.
 161         apply H.
 162         apply if_inv.
 163         apply (if_comp (if_inv H)).
 164         clear H.
 165         apply (if_respects
 166           (ga_functor g)
 167           (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g))
 168           (HomFunctor (senr_c s2) (senr_c_i s2))
 169           (HomFunctor (senr_c s2) (senr_c_i s2))
 170         ).
 171         apply q.
 172         apply if_id.
 173         Qed.
 174
 175     Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
 176       (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
 177       (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
 178       reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
 179         unfold hom in *.
 180         set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon b)) as q.
 181         destruct f; simpl.
 182         apply H.
 183         apply if_inv.
 184         apply (if_comp (if_inv H)).
 185         clear H.
 186         simpl.
 187         simpl in q.
 188         simpl in q.
 189         apply q.
 190         Qed.
 191
 192     Lemma M2_respects :
 193       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
 194          f ~~ f' ->
 195          M2 a b f ~~ M2 a b f'.
 196       intros.
 197         unfold hom in *.
 198         unfold eqv in *.
 199         simpl in *.
 200         destruct f.
 201           set (invert_reif _ f') as q.
 202           destruct q; subst.
 203           apply if_id.
 204
 205           simpl in *.
 206           destruct H0; subst.
 207           simpl in *.
 208           unfold garrow_functor.
 209           unfold step2_functor.
 210           apply (if_comp H).
 211           clear H.
 212           eapply if_comp.
 213           apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
 214           apply if_inv.
 215           set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
 216           apply if_inv.
 217           eapply if_comp.
 218           apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
 219           apply if_inv.
 220           eapply if_comp.
 221           apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
 222                    ff_functor_section_functor me_homfunctor me_full me_faithful))
 223           (HomFunctor (senr_c smme) (senr_c_i smme))).
 224           apply (if_respects (RestrictToImage x) (RestrictToImage x)).
 225           apply (if_id (RestrictToImage x)).
 226           unfold mf_F.
 227           unfold me_homfunctor in q.
 228           unfold pmon_I.
 229           apply q.
 230
 231       simpl in *.
 232         destruct f'; simpl in *.
 233         simpl in *.
 234         apply if_inv in H.
 235         eapply if_comp; [ idtac | eapply if_inv; apply H ].
 236         clear H.
 237         unfold garrow_functor.
 238         unfold step2_functor.
 239         apply if_inv.
 240         eapply if_comp.
 241         apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
 242
 243         rename r into x.
 244         apply if_inv.
 245         eapply if_comp.
 246         apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
 247                  ff_functor_section_functor me_homfunctor me_full me_faithful))
 248         (HomFunctor (senr_c smme) (senr_c_i smme))).
 249         apply if_inv.
 250         eapply if_comp.
 251         apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
 252         apply (if_respects (RestrictToImage x) (RestrictToImage x)).
 253         apply (if_id (RestrictToImage x)).
 254
 255         unfold mf_F.
 256         set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
 257         apply if_inv.
 258         unfold me_homfunctor in q.
 259         unfold pmon_I.
 260         apply q.
 261
 262       simpl in *.
 263         unfold garrow_functor.
 264         unfold step2_functor.
 265         set (step1_niso s1 (smme_mee s2) s2 r) as q.
 266         apply if_inv in q.
 267         eapply if_comp.
 268         eapply if_comp; [ idtac | apply q ].
 269
 270         eapply if_comp.
 271         apply (if_associativity
 272           (RestrictToImage r)
 273           (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
 274           (HomFunctor (senr_c s2) (senr_c_i s2))).
 275         apply if_inv.
 276         eapply if_comp.
 277         apply (if_associativity
 278           (RestrictToImage r)
 279           (R' s1 s2 r)
 280           (FullImage_InclusionFunctor _)).
 281         apply (if_respects
 282           (RestrictToImage r)
 283           (RestrictToImage r)
 284           (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
 285           (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
 286              HomFunctor (senr_c s2) (senr_c_i s2)))).
 287         apply (if_id _).
 288         apply if_inv.
 289         eapply if_comp.
 290         apply (if_associativity
 291           (R' s1 s2 r)
 292           (ff_functor_section_functor me_homfunctor me_full me_faithful)
 293           (HomFunctor (senr_c s2) (senr_c_i s2))).
 294         apply if_inv.
 295         apply (if_respects
 296           (R' s1 s2 r)
 297           (R' s1 s2 r)
 298           (FullImage_InclusionFunctor _)
 299           ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
 300         ).
 301         apply (if_id _).
 302         apply if_inv.
 303         apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
 304         Qed.
 305
 306     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
 307       refine {| fmor := fun a b f => M2 _ _ f |}.
 308       apply M2_respects.
 309       intros; simpl; apply if_id.
 310       intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
 311       apply M2_respects; auto.
 312       unfold fmor; simpl.
 313       apply (@eqv1 _ _ f0 f0).
 314       apply if_id.
 315       unfold fmor; simpl.
 316       apply (@eqv2 _ _ f0 f0).
 317       apply if_id.
 318       Defined.
 319
 320     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
 321       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
 322       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 323       apply (eqv1 _ _ f f'); auto.
 324       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 325       apply (eqv2 _ _ f f'); auto.
 326       Qed.
 327
 328 End ReificationsIsomorphicToGeneralizedArrows.