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
  34 Section ReificationsIsomorphicToGeneralizedArrows.
  35
  36     Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
  37       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
  38       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
  39       intro GA.
  40       destruct GA; [ apply roi_id | idtac ].
  41       apply roi_reif.
  42       apply reification_from_garrow.
  43       apply g.
  44       Defined.
  45
  46     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
  47       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
  48       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
  49       intro RE.
  50       destruct RE; [ apply gaoi_id | idtac ].
  51       apply gaoi_ga.
  52       apply (garrow_from_reification s1 s2 r).
  53       Defined.
  54
  55     (*
  56
  57      * Oh my, this is massively embarrassing.  In the paper I claim
  58      * that Generalized Arrows form a category and Reifications form a
  59      * category, when in fact they form merely a SEMIcategory (see
  60      * http://ncatlab.org/nlab/show/semicategory) since we cannot be sure that the identity functor on the
  61
  62     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
  63       apply WeakFunctorCategoriesIsomorphic with (M1:=M1) (M2:=M2).
  64       destruct g.
  65       intros.
  66       simpl.
  67       simpl in H.
  68       split f.
  69       destruct f.
  70       dependent destruction f.
  71       intros until g.
  72       destruct f.
  73       simpl.
  74       inversion g.
  75       destruct f as [ ] _eqn.
  76       destruct g as [ ] _eqn.
  77       destruct g.
  78       subst.
  79       simpl.
  80       case g.
  81       simpl.
  82       inversion g; subst; intros.
  83       destruct g.
  84       Qed.
  85
  86 End ReificationsIsomorphicToGeneralizedArrows.