src/Enrichments.v

   1 (*********************************************************************************************************************************)
   2 (* Enrichments                                                                                                                   *)
   3 (*                                                                                                                               *)
   4 (*                                                                                                                               *)
   5 (*********************************************************************************************************************************)
   6
   7 Generalizable All Variables.
   8 Require Import Preamble.
   9 Require Import General.
  10 Require Import Categories_ch1_3.
  11 Require Import Functors_ch1_4.
  12 Require Import Isomorphisms_ch1_5.
  13 Require Import ProductCategories_ch1_6_1.
  14 Require Import OppositeCategories_ch1_6_2.
  15 Require Import Enrichment_ch2_8.
  16 Require Import Subcategories_ch7_1.
  17 Require Import NaturalTransformations_ch7_4.
  18 Require Import NaturalIsomorphisms_ch7_5.
  19 Require Import MonoidalCategories_ch7_8.
  20 Require Import Coherence_ch7_8.
  21 Require Import BinoidalCategories.
  22 Require Import PreMonoidalCategories.
  23 Require Import PreMonoidalCenter.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import WeakFunctorCategory.
  26
  27 (* in the paper this is called simply an "enrichment" *)
  28 Structure Enrichment :=
  29 { enr_v_ob         :  Type
  30 ; enr_v_hom        :  enr_v_ob -> enr_v_ob -> Type
  31 ; enr_v            :  Category enr_v_ob enr_v_hom
  32 ; enr_v_i          :  enr_v_ob
  33 ; enr_v_bobj       :  enr_v -> enr_v -> enr_v
  34 ; enr_v_bin        :  BinoidalCat enr_v enr_v_bobj
  35 ; enr_v_pmon       :  PreMonoidalCat enr_v_bin enr_v_i
  36 ; enr_v_mon        :  MonoidalCat enr_v_pmon
  37 ; enr_c_obj        :  Type
  38 ; enr_c_hom        :  enr_c_obj -> enr_c_obj -> enr_v
  39 ; enr_c            :  ECategory enr_v_mon enr_c_obj enr_c_hom
  40 ; enr_c_bin        :  EBinoidalCat enr_c
  41 ; enr_c_i          :  enr_c
  42 ; enr_c_pm         :  PreMonoidalCat enr_c_bin enr_c_i
  43 ; enr_c_center     := Center enr_c_bin
  44 ; enr_c_center_mon := Center_is_Monoidal enr_c_pm
  45 }.
  46 Coercion enr_c   : Enrichment >-> ECategory.
  47
  48 (* Coq grinds down into a performance bog when I try to use this *)
  49 Definition WeaklySurjectiveEnrichment (ec:Enrichment) :=
  50   @treeDecomposition (enr_v ec) (option (ec*ec))
  51                   (fun t => match t with
  52                             | None   => enr_v_i ec
  53                             | Some x => match x with pair y z => enr_c_hom ec y z end
  54                             end)
  55                   (enr_v_bobj ec).
  56
  57 (* technically this ought to be a "strictly surjective enrichment" *)
  58 Structure SurjectiveEnrichment :=
  59 { senr_c_obj      :  Type
  60 ; senr_v_ob       := Tree ??(senr_c_obj * senr_c_obj)
  61 ; senr_c_hom      := fun (c1 c2:senr_c_obj) => [(c1, c2)]
  62 ; senr_v_hom      :  senr_v_ob -> senr_v_ob -> Type
  63 ; senr_v          :  Category senr_v_ob senr_v_hom
  64 ; senr_v_i        := []
  65 ; senr_v_bobj     := @T_Branch ??(senr_c_obj * senr_c_obj)
  66 ; senr_v_bin      :  BinoidalCat senr_v senr_v_bobj
  67 ; senr_v_pmon     :  PreMonoidalCat senr_v_bin senr_v_i
  68 ; senr_v_mon      :  MonoidalCat senr_v_pmon
  69 ; senr_c          :  ECategory senr_v_mon senr_c_obj senr_c_hom
  70 ; senr_c_bin      :  EBinoidalCat senr_c
  71 ; senr_c_i        :  senr_c
  72 ; senr_c_pm       :  PreMonoidalCat senr_c_bin senr_c_i
  73 }.
  74
  75 Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
  76 refine
  77 {| enr_v_ob      := senr_v_ob se
  78 ; enr_v_hom      := senr_v_hom se
  79 ; enr_v          := senr_v se
  80 ; enr_v_i        := senr_v_i se
  81 ; enr_v_bobj     := senr_v_bobj se
  82 ; enr_v_bin      := senr_v_bin se
  83 ; enr_v_pmon     := senr_v_pmon se
  84 ; enr_v_mon      := senr_v_mon se
  85 ; enr_c_obj      := senr_c_obj se
  86 ; enr_c_hom      := senr_c_hom se
  87 ; enr_c          := senr_c se
  88 ; enr_c_bin      := senr_c_bin se
  89 ; enr_c_i        := senr_c_i se
  90 ; enr_c_pm       := senr_c_pm se
  91 |}.
  92 Defined.
  93 Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
  94
  95 Definition MonoidalEnrichment (e:Enrichment) :=
  96   PreMonoidalFunctor
  97     (enr_c_pm e)
  98     (enr_v_pmon e)
  99     (HomFunctor e (pmon_I (enr_c_pm e))).
 100
 101 Class MonicEnrichment {e:Enrichment} :=
 102 { me_enr          := e
 103 ; me_homfunctor   := HomFunctor e (enr_c_i e)
 104 ; me_full         :  FullFunctor         me_homfunctor
 105 ; me_faithful     :  FaithfulFunctor     me_homfunctor
 106 ; me_conservative :  ConservativeFunctor me_homfunctor
 107 (*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
 108 }.
 109 Implicit Arguments MonicEnrichment [ ].
 110 Coercion me_enr : MonicEnrichment >-> Enrichment.
 111 Transparent HomFunctor.
 112
 113 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
 114 Structure SMME :=
 115 { smme_e   : SurjectiveEnrichment
 116 ; smme_mon : MonoidalEnrichment smme_e
 117 ; smme_mee : MonicEnrichment smme_e
 118 }.
 119 Coercion smme_e   : SMME >-> SurjectiveEnrichment.
 120 Coercion smme_mon : SMME >-> MonoidalEnrichment.
 121
 122 Definition SMMEs : SmallCategories.
 123   refine {| small_cat       := SMME
 124           ; small_cat_cat   := fun smme => enr_v smme
 125           |}.
 126   Defined.