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 Structure SurjectiveEnrichment :=
  49 { senr_c_obj      :  Type
  50 ; senr_v_ob       := Tree ??(senr_c_obj * senr_c_obj)
  51 ; senr_c_hom      := fun (c1 c2:senr_c_obj) => [(c1, c2)]
  52 ; senr_v_hom      : senr_v_ob -> senr_v_ob -> Type
  53 ; senr_v          : Category senr_v_ob senr_v_hom
  54 ; senr_v_i        := []
  55 ; senr_v_bobj     := @T_Branch (option (senr_c_obj * senr_c_obj))
  56 ; senr_v_bin      : BinoidalCat senr_v senr_v_bobj
  57 ; senr_v_pmon     : PreMonoidalCat senr_v_bin senr_v_i
  58 ; senr_v_mon      : MonoidalCat senr_v_pmon
  59 ; senr_c          : ECategory senr_v_mon senr_c_obj senr_c_hom
  60 ; senr_c_bin      : EBinoidalCat senr_c
  61 ; senr_c_i        : senr_c
  62 ; senr_c_pm       : PreMonoidalCat senr_c_bin senr_c_i
  63 }.
  64
  65 Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
  66 refine
  67 {| enr_v_ob      := senr_v_ob se
  68 ; enr_v_hom      := senr_v_hom se
  69 ; enr_v          := senr_v se
  70 ; enr_v_i        := senr_v_i se
  71 ; enr_v_bobj     := senr_v_bobj se
  72 ; enr_v_bin      := senr_v_bin se
  73 ; enr_v_pmon     := senr_v_pmon se
  74 ; enr_v_mon      := senr_v_mon se
  75 ; enr_c_obj      := senr_c_obj se
  76 ; enr_c_hom      := senr_c_hom se
  77 ; enr_c          := senr_c se
  78 ; enr_c_bin      := senr_c_bin se
  79 ; enr_c_i        := senr_c_i se
  80 ; enr_c_pm       := senr_c_pm se
  81 |}.
  82 Defined.
  83 Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
  84
  85 (*
  86 Definition MonoidalEnrichment (e:Enrichment) :=
  87   PreMonoidalFunctor
  88     (enr_c_center_mon e)
  89     (enr_v_pmon e)
  90     (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))).
  91 *)
  92 Definition MonoidalEnrichment (e:Enrichment) :=
  93   PreMonoidalFunctor
  94     (enr_c_pm e)
  95     (enr_v_pmon e)
  96     (HomFunctor e (pmon_I (enr_c_pm e))).
  97
  98
  99 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
 100 (*
 101 Definition SurjectiveEnrichment (ec:Enrichment) :=
 102   @treeDecomposition (enr_v ec) (option (ec*ec))
 103                   (fun t => match t with
 104                             | None   => enr_v_i ec
 105                             | Some x => match x with pair y z => enr_c_hom ec y z end
 106                             end)
 107                   (enr_v_bobj ec).
 108 *)
 109
 110 Class MonicEnrichment {e:Enrichment} :=
 111 { me_enr          := e
 112 ; me_homfunctor   := HomFunctor e (enr_c_i e)
 113 (*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
 114 ; me_full         :  FullFunctor         me_homfunctor
 115 ; me_faithful     :  FaithfulFunctor     me_homfunctor
 116 ; me_conservative :  ConservativeFunctor me_homfunctor
 117 }.
 118 Implicit Arguments MonicEnrichment [ ].
 119 Coercion me_enr : MonicEnrichment >-> Enrichment.
 120 Transparent HomFunctor.
 121
 122 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
 123 Structure SMME :=
 124 { smme_e   : SurjectiveEnrichment
 125 (*; smme_see : SurjectiveEnrichment smme_e*)
 126 ; smme_mon : MonoidalEnrichment smme_e
 127 ; smme_mee : MonicEnrichment smme_e
 128 }.
 129 Coercion smme_e   : SMME >-> SurjectiveEnrichment.
 130 Coercion smme_mon : SMME >-> MonoidalEnrichment.
 131
 132 Definition SMMEs : SmallCategories.
 133   refine {| small_cat       := SMME
 134           ; small_cat_cat   := fun smme => enr_v smme
 135           |}.
 136   Defined.