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 (* Technically reifications form merely a *semicategory* (no identity
  30  * maps), but one can always freely adjoin identity maps (and nothing
  31  * else) to a semicategory to get a category whose non-identity-map
  32  * portion is identical to the original semicategory
  33  *
  34  * Also, technically this category has ALL enrichments (not just the
  35  * surjective monic monoidal ones), though there maps OUT OF only the
  36  * surjective enrichments and INTO only the monic monoidal
  37  * enrichments.  It's a big pain to do this in Coq, but sort of might
  38  * matter in real life: a language with really severe substructural
  39  * restrictions might fail to be monoidally enriched, meaning we can't
  40  * use it as a host language.  But that's for the next paper...
  41  *)
  42 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
  43   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
  44   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.
  45
  46 Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
  47   match f with
  48   | roi_id   s       => (fun x => x)
  49   | roi_reif s1 s2 f => reification_rstar_obj f
  50   end.
  51
  52 Definition reificationOrIdentityFunc
  53   : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
  54   intros.
  55   destruct f.
  56   apply functor_id.
  57   unfold reificationOrIdentityFobj.
  58   apply (reification_rstar_f r).
  59   Defined.
  60
  61 Definition compose_reifications (s0 s1 s2:SMMEs) :
  62   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
  63   intros.
  64   refine
  65     {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
  66      ; reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
  67      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
  68     |}.
  69   intro K.
  70   set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (RepresentableFunctor s2 (mon_i s2))) as q.
  71   eapply ni_comp.
  72   apply q.
  73   clear q.
  74   set (reification_commutes X K) as comm1.
  75   set (reification_commutes X0 (mon_i s1)) as comm2.
  76   set (RepresentableFunctor s0 K) as a in *.
  77   set (reification_rstar_f X) as a' in *.
  78   set (reification_rstar_f X0) as x in *.
  79   set (reification_r X K) as b in *.
  80   set (reification_r X0 (mon_i s1)) as c in *.
  81   set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
  82   set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
  83   apply (ni_comp(F2:=b >>>> (b' >>>> x))).
  84   apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
  85   apply ni_id.
  86   apply comm2.
  87   eapply ni_comp.
  88   eapply ni_inv.
  89   apply (ni_associativity b b' x).
  90   eapply ni_inv.
  91   eapply ni_comp.
  92   eapply ni_inv.
  93   apply (ni_associativity a a' x).
  94   apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
  95   apply ni_inv.
  96   apply comm1.
  97   apply ni_id.
  98   Defined.
  99
 100 Definition reificationOrIdentityComp
 101   : forall s1 s2 s3, ReificationOrIdentity s1 s2 -> ReificationOrIdentity s2 s3 -> ReificationOrIdentity s1 s3.
 102   intros.
 103   destruct X.
 104     apply X0.
 105   destruct X0.
 106     apply (roi_reif _ _ r).
 107     apply (roi_reif _ _ (compose_reifications _ _ _ r r0)).
 108     Defined.
 109
 110 Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
 111   refine {| small_func      := ReificationOrIdentity
 112           ; small_func_id   := fun s => roi_id s
 113           ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
 114           ; small_func_comp := reificationOrIdentityComp
 115          |}; intros; simpl.
 116   apply if_id.
 117   destruct f as [|fobj f]; simpl in *.
 118     apply if_inv.
 119     apply if_left_identity.
 120   destruct g as [|gobj g]; simpl in *.
 121     apply if_inv.
 122     apply if_right_identity.
 123   apply if_id.
 124   Defined.
 125
 126 Definition CategoryOfReifications :=
 127   WeakFunctorCategory MorphismsOfCategoryOfReifications.