src/ReificationsEquivalentToGeneralizedArrows.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
  31 Section ReificationsEquivalentToGeneralizedArrows.
  32
  33   Ltac if_transitive :=
  34     match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
  35     end.
  36
  37   Lemma roundtrip_lemma'
  38     `{C:Category}`{D:Category}`{E:Category}
  39     {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) :
  40     ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _).
  41     if_transitive.
  42       apply (if_associativity F (ff_functor_section_functor G _ _) G).
  43       apply if_respects.
  44         apply if_id.
  45         if_transitive; [ idtac | apply if_left_identity ].
  46     apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)).
  47     apply if_inv.
  48     apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
  49     apply if_respects.
  50     apply ff_functor_section_splits_niso.
  51     apply if_id.
  52     Qed.
  53
  54   Definition roundtrip_lemma
  55     (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
  56     := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
  57
  58   Lemma roundtrip_reification_to_reification
  59     (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
  60     : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
  61     simpl.
  62     unfold mon_f.
  63     unfold garrow_functor.
  64     apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
  65        apply step1_niso.
  66        apply (if_inv (roundtrip_lemma K C reification)).
  67     Qed.
  68     (* FIXME: show that the R-functors are naturally isomorphic as well; should follow pretty easily from the proof for Rstar *)
  69
  70   Lemma roundtrip_garrow_to_garrow
  71     (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (garrow : GeneralizedArrow K C)
  72     : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
  73     apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)).
  74     apply if_inv.
  75     apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
  76            >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
  77     unfold mf_f.
  78     unfold garrow_from_reification.
  79     unfold garrow_functor.
  80     unfold step2_functor.
  81     apply roundtrip_lemma.
  82     apply if_inv.
  83     apply (step1_niso K C (reification_from_garrow K C garrow)).
  84     Qed.
  85
  86   Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
  87     admit.
  88     Qed.
  89
  90 End ReificationsEquivalentToGeneralizedArrows.