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_bobj       :  enr_c_obj -> enr_c_obj -> enr_c_obj
  41 ; enr_c_bin        :  EBinoidalCat enr_c enr_c_bobj
  42 ; enr_c_i          :  enr_c
  43 ; enr_c_pm         :  PreMonoidalCat enr_c_bin enr_c_i
  44 ; enr_c_center     := Center enr_c_bin
  45 ; enr_c_center_mon := Center_is_Monoidal enr_c_pm
  46 }.
  47 Coercion enr_c   : Enrichment >-> ECategory.
  48
  49 (* Coq grinds down into a performance bog when I try to use this *)
  50 Definition WeaklySurjectiveEnrichment (ec:Enrichment) :=
  51   @treeDecomposition (enr_v ec) (option (ec*ec))
  52                   (fun t => match t with
  53                             | None   => enr_v_i ec
  54                             | Some x => match x with pair y z => enr_c_hom ec y z end
  55                             end)
  56                   (enr_v_bobj ec).
  57
  58 (* technically this ought to be a "strictly surjective enrichment" *)
  59 Structure SurjectiveEnrichment :=
  60 { senr_c_obj      :  Type
  61 ; senr_v_ob       := Tree ??(senr_c_obj * senr_c_obj)
  62 ; senr_c_hom      := fun (c1 c2:senr_c_obj) => [(c1, c2)]
  63 ; senr_v_hom      :  senr_v_ob -> senr_v_ob -> Type
  64 ; senr_v          :  Category senr_v_ob senr_v_hom
  65 ; senr_v_i        := []
  66 ; senr_v_bobj     := @T_Branch ??(senr_c_obj * senr_c_obj)
  67 ; senr_v_bin      :  BinoidalCat senr_v senr_v_bobj
  68 ; senr_v_pmon     :  PreMonoidalCat senr_v_bin senr_v_i
  69 ; senr_v_mon      :  MonoidalCat senr_v_pmon
  70 ; senr_c          :  ECategory senr_v_mon senr_c_obj senr_c_hom
  71 ; senr_c_bobj     :  senr_c_obj -> senr_c_obj -> senr_c_obj
  72 ; senr_c_bin      :  EBinoidalCat senr_c senr_c_bobj
  73 ; senr_c_i        :  senr_c
  74 ; senr_c_pm       :  PreMonoidalCat senr_c_bin senr_c_i
  75 }.
  76
  77 Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
  78 refine
  79 {| enr_v_ob      := senr_v_ob se
  80 ; enr_v_hom      := senr_v_hom se
  81 ; enr_v          := senr_v se
  82 ; enr_v_i        := senr_v_i se
  83 ; enr_v_bobj     := senr_v_bobj se
  84 ; enr_v_bin      := senr_v_bin se
  85 ; enr_v_pmon     := senr_v_pmon se
  86 ; enr_v_mon      := senr_v_mon se
  87 ; enr_c_obj      := senr_c_obj se
  88 ; enr_c_hom      := senr_c_hom se
  89 ; enr_c          := senr_c se
  90 ; enr_c_bin      := senr_c_bin se
  91 ; enr_c_i        := senr_c_i se
  92 ; enr_c_pm       := senr_c_pm se
  93 |}.
  94 Defined.
  95 Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
  96
  97 Definition MonoidalEnrichment (e:Enrichment) :=
  98   PreMonoidalFunctor
  99     (enr_c_pm e)
 100     (enr_v_pmon e)
 101     (HomFunctor e (pmon_I (enr_c_pm e))).
 102
 103 Class MonicEnrichment {e:Enrichment} :=
 104 { me_enr          := e
 105 ; me_homfunctor   := HomFunctor e (enr_c_i e)
 106 ; me_full         :  FullFunctor         me_homfunctor
 107 ; me_faithful     :  FaithfulFunctor     me_homfunctor
 108 ; me_conservative :  ConservativeFunctor me_homfunctor
 109 (*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
 110 }.
 111 Implicit Arguments MonicEnrichment [ ].
 112 Coercion me_enr : MonicEnrichment >-> Enrichment.
 113 Transparent HomFunctor.
 114
 115 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
 116 Structure SMME :=
 117 { smme_e   : SurjectiveEnrichment
 118 ; smme_mon : MonoidalEnrichment smme_e
 119 ; smme_mee : MonicEnrichment smme_e
 120 }.
 121 Coercion smme_e   : SMME >-> SurjectiveEnrichment.
 122 Coercion smme_mon : SMME >-> MonoidalEnrichment.
 123
 124 Definition SMMEs : SmallCategories.
 125   refine {| small_cat       := SMME
 126           ; small_cat_cat   := fun smme => enr_v smme
 127           |}.
 128   Defined.