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 MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import Reification.
  26 Require Import WeakFunctorCategory.
  27 Require Import SmallSMMEs.
  28
  29 (*
  30  * Technically reifications form merely a *semicategory* (no identity
  31  * maps), but one can always freely adjoin identity maps (and nothing
  32  * else) to a semicategory to get a category whose non-identity-map
  33  * portion is identical to the original semicategory (closing under
  34  * composition after putting in the identity maps never produces any
  35  * additional maps)
  36  *
  37  * Also, technically this category has ALL enrichments (not just the
  38  * surjective monic monoidal ones), though there maps OUT OF only the
  39  * surjective enrichments and INTO only the monic monoidal
  40  * enrichments.  It's a big pain to do this in Coq, but sort of might
  41  * matter in real life: a language with really severe substructural
  42  * restrictions might fail to be monoidally enriched, meaning we can't
  43  * use it as a host language.  But that's for the next paper...
  44  *)
  45 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
  46   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
  47   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.
  48
  49 Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
  50   match f with
  51   | roi_id   s       => (fun x => x)
  52   | roi_reif s1 s2 f => reification_rstar_obj f
  53   end.
  54
  55 Definition reificationOrIdentityFunc
  56   : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
  57   intros.
  58   destruct f.
  59   apply functor_id.
  60   unfold reificationOrIdentityFobj.
  61   apply (reification_rstar_f r).
  62   Defined.
  63
  64 Definition compose_reifications (s0 s1 s2:SMMEs) :
  65   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
  66   intros.
  67   refine
  68     {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
  69      ; reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
  70      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
  71     |}.
  72   intro K.
  73   set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (HomFunctor s2 (mon_i s2))) as q.
  74   eapply ni_comp.
  75   apply q.
  76   clear q.
  77   set (reification_commutes X K) as comm1.
  78   set (reification_commutes X0 (mon_i s1)) as comm2.
  79   set (HomFunctor s0 K) as a in *.
  80   set (reification_rstar_f X) as a' in *.
  81   set (reification_rstar_f X0) as x in *.
  82   set (reification_r X K) as b in *.
  83   set (reification_r X0 (mon_i s1)) as c in *.
  84   set (HomFunctor s2 (mon_i s2)) as c' in *.
  85   set (HomFunctor s1 (mon_i s1)) as b' in *.
  86   apply (ni_comp(F2:=b >>>> (b' >>>> x))).
  87   apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
  88   apply ni_id.
  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_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
  98   apply ni_inv.
  99   apply comm1.
 100   apply ni_id.
 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.