src/ReificationCategory.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationCategory:                                                                                                          *)
   3 (*                                                                                                                               *)
   4 (*   There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms                    *)
   5 (*   are reifications                                                                                                            *)
   6 (*                                                                                                                               *)
   7 (*********************************************************************************************************************************)
   8
   9 Generalizable All Variables.
  10 Require Import Preamble.
  11 Require Import General.
  12 Require Import Categories_ch1_3.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import PreMonoidalCategories.
  22 Require Import MonoidalCategories_ch7_8.
  23 Require Import Coherence_ch7_8.
  24 Require Import Enrichment_ch2_8.
  25 Require Import Enrichments.
  26 Require Import RepresentableStructure_ch7_2.
  27 Require Import Reification.
  28 Require Import WeakFunctorCategory.
  29
  30 (*
  31  * Technically reifications form merely a *semicategory* (no identity
  32  * maps), but one can always freely adjoin identity maps (and nothing
  33  * else) to a semicategory to get a category whose non-identity-map
  34  * portion is identical to the original semicategory (closing under
  35  * composition after putting in the identity maps never produces any
  36  * additional maps)
  37  *
  38  * Also, technically this category has ALL enrichments (not just the
  39  * surjective monic monoidal ones), though there maps OUT OF only the
  40  * surjective enrichments and INTO only the monic monoidal
  41  * enrichments.  It's a big pain to do this in Coq, but sort of might
  42  * matter in real life: a language with really severe substructural
  43  * restrictions might fail to be monoidally enriched, meaning we can't
  44  * use it as a host language.  But that's for the next paper...
  45  *)
  46 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
  47   | roi_id   : forall smme:SMMEs,                                    ReificationOrIdentity smme smme
  48   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (enr_c_i s2) -> ReificationOrIdentity s1   s2.
  49
  50 Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
  51   match f with
  52   | roi_id   s       => (fun x => x)
  53   | roi_reif s1 s2 f => reification_rstar_obj f
  54   end.
  55
  56 Definition reificationOrIdentityFunc
  57   : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
  58   intros.
  59   destruct f.
  60   apply functor_id.
  61   unfold reificationOrIdentityFobj.
  62   apply (reification_rstar_f r).
  63   Defined.
  64
  65 Definition compose_reifications (s0 s1 s2:SMMEs) :
  66   Reification s0 s1 (enr_c_i s1) -> Reification s1 s2 (enr_c_i s2) -> Reification s0 s2 (enr_c_i s2).
  67   intros.
  68   refine
  69     {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
  70      ; reification_rstar   := PreMonoidalFunctorsCompose (reification_rstar X) (reification_rstar X0)
  71      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (enr_c_i s1))
  72     |}.
  73   intro K.
  74   set (ni_associativity (reification_r X K) (reification_r X0 (enr_c_i s1)) (HomFunctor s2 (enr_c_i s2))) as q.
  75   eapply ni_comp.
  76   apply q.
  77   clear q.
  78   set (reification_commutes X K) as comm1.
  79   set (reification_commutes X0 (enr_c_i s1)) as comm2.
  80   set (HomFunctor s0 K) as a in *.
  81   set (reification_rstar_f X) as a' in *.
  82   set (reification_rstar_f X0) as x in *.
  83   set (reification_r X K) as b in *.
  84   set (reification_r X0 (enr_c_i s1)) as c in *.
  85   set (HomFunctor s2 (enr_c_i s2)) as c' in *.
  86   set (HomFunctor s1 (enr_c_i s1)) as b' in *.
  87   apply (ni_comp(F2:=b >>>> (b' >>>> x))).
  88   apply (ni_respects1 b (c >>>> c') (b' >>>> x)).
  89   apply comm2.
  90   eapply ni_comp.
  91   eapply ni_inv.
  92   apply (ni_associativity b b' x).
  93   eapply ni_inv.
  94   eapply ni_comp.
  95   eapply ni_inv.
  96   apply (ni_associativity a a' x).
  97   apply (ni_respects2 (a >>>> a') (b >>>> b') x).
  98   apply ni_inv.
  99   apply comm1.
 100   apply (reification_host_lang_pure _ _ _ X0).
 101   Defined.
 102
 103 Definition reificationOrIdentityComp
 104   : forall s1 s2 s3, ReificationOrIdentity s1 s2 -> ReificationOrIdentity s2 s3 -> ReificationOrIdentity s1 s3.
 105   intros.
 106   destruct X.
 107     apply X0.
 108   destruct X0.
 109     apply (roi_reif _ _ r).
 110     apply (roi_reif _ _ (compose_reifications _ _ _ r r0)).
 111     Defined.
 112
 113 Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
 114   refine {| small_func      := ReificationOrIdentity
 115           ; small_func_id   := fun s => roi_id s
 116           ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
 117           ; small_func_comp := reificationOrIdentityComp
 118          |}; intros; simpl.
 119   apply if_id.
 120   destruct f as [|fobj f]; simpl in *.
 121     apply if_inv.
 122     apply if_left_identity.
 123   destruct g as [|gobj g]; simpl in *.
 124     apply if_inv.
 125     apply if_right_identity.
 126   apply if_id.
 127   Defined.
 128
 129 Definition CategoryOfReifications :=
 130   WeakFunctorCategory MorphismsOfCategoryOfReifications.