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           apply if_inv.
 216           eapply if_comp.
 217           apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
 218           apply if_inv.
 219           eapply if_comp.
 220           apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
 221                    ff_functor_section_functor me_homfunctor me_full me_faithful))
 222           (HomFunctor (senr_c smme) (senr_c_i smme))).
 223           apply (if_respects (RestrictToImage x) (RestrictToImage x)).
 224           apply (if_id (RestrictToImage x)).
 225           unfold mf_F.
 226           eapply if_comp.
 227             apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
 228               (HomFunctor (senr_c smme) (senr_c_i smme))).
 229           set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
 230           set (R' smme smme x) as f.
 231           set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
 232           unfold HomFunctor_fullimage in f.
 233           unfold mf_F in f.
 234           set (q ff _ _ (FullImage x) _ f) as q'.
 235           unfold me_homfunctor in q'.
 236           exact q'.
 237
 238       simpl in *.
 239         destruct f'; simpl in *.
 240         simpl in *.
 241         apply if_inv in H.
 242         eapply if_comp; [ idtac | eapply if_inv; apply H ].
 243         clear H.
 244         unfold garrow_functor.
 245         unfold step2_functor.
 246         apply if_inv.
 247         eapply if_comp.
 248         apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
 249
 250         rename r into x.
 251         apply if_inv.
 252         eapply if_comp.
 253         apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
 254                  ff_functor_section_functor me_homfunctor me_full me_faithful))
 255         (HomFunctor (senr_c smme) (senr_c_i smme))).
 256         apply if_inv.
 257         eapply if_comp.
 258         apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
 259         apply (if_respects (RestrictToImage x) (RestrictToImage x)).
 260         apply (if_id (RestrictToImage x)).
 261
 262         unfold mf_F.
 263         apply if_inv.
 264
 265         eapply if_comp.
 266           apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
 267             (HomFunctor (senr_c smme) (senr_c_i smme))).
 268         set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
 269           set (R' smme smme x) as f.
 270           set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
 271           unfold HomFunctor_fullimage in f.
 272           unfold mf_F in f.
 273           set (q ff _ _ (FullImage x) _ f) as q'.
 274           unfold me_homfunctor in q'.
 275           exact q'.
 276
 277       simpl in *.
 278         unfold garrow_functor.
 279         unfold step2_functor.
 280         set (step1_niso s1 (smme_mee s2) s2 r) as q.
 281         apply if_inv in q.
 282         eapply if_comp.
 283         eapply if_comp; [ idtac | apply q ].
 284
 285         eapply if_comp.
 286         apply (if_associativity
 287           (RestrictToImage r)
 288           (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
 289           (HomFunctor (senr_c s2) (senr_c_i s2))).
 290         apply if_inv.
 291         eapply if_comp.
 292         apply (if_associativity
 293           (RestrictToImage r)
 294           (R' s1 s2 r)
 295           (FullImage_InclusionFunctor _)).
 296         apply (if_respects
 297           (RestrictToImage r)
 298           (RestrictToImage r)
 299           (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
 300           (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
 301              HomFunctor (senr_c s2) (senr_c_i s2)))).
 302         apply (if_id _).
 303         apply if_inv.
 304         eapply if_comp.
 305         apply (if_associativity
 306           (R' s1 s2 r)
 307           (ff_functor_section_functor me_homfunctor me_full me_faithful)
 308           (HomFunctor (senr_c s2) (senr_c_i s2))).
 309         apply roundtrip_lemma.
 310
 311         apply if_inv.
 312         set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
 313         apply if_inv in q'.
 314         eapply if_comp.
 315         eapply if_comp; [ idtac | apply q' ].
 316         eapply if_comp.
 317         apply (if_associativity
 318           (RestrictToImage r0)
 319           (R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
 320           (HomFunctor (senr_c s2) (senr_c_i s2))).
 321         apply if_inv.
 322         eapply if_comp.
 323         apply (if_associativity
 324           (RestrictToImage r0)
 325           (R' s1 s2 r0)
 326           (FullImage_InclusionFunctor _)).
 327         apply (if_respects
 328           (RestrictToImage r0)
 329           (RestrictToImage r0)
 330           (R' s1 s2 r0 >>>> FullImage_InclusionFunctor _)
 331           (((R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
 332              HomFunctor (senr_c s2) (senr_c_i s2)))).
 333         apply (if_id _).
 334         apply if_inv.
 335         eapply if_comp.
 336         apply (if_associativity
 337           (R' s1 s2 r0)
 338           (ff_functor_section_functor me_homfunctor me_full me_faithful)
 339           (HomFunctor (senr_c s2) (senr_c_i s2))).
 340         apply roundtrip_lemma.
 341         apply if_inv.
 342         apply H.
 343         Qed.
 344
 345     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
 346       refine {| fmor := fun a b f => M2 _ _ f |}.
 347       apply M2_respects.
 348       intros; simpl; apply if_id.
 349       intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
 350       apply M2_respects; auto.
 351       unfold fmor; simpl.
 352       apply (@eqv1 _ _ f0 f0).
 353       apply if_id.
 354       unfold fmor; simpl.
 355       apply (@eqv2 _ _ f0 f0).
 356       apply if_id.
 357       Defined.
 358
 359     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
 360       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
 361       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 362       apply (eqv1 _ _ f f'); auto.
 363       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 364       apply (eqv2 _ _ f f'); auto.
 365       Qed.
 366
 367 End ReificationsIsomorphicToGeneralizedArrows.