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
  24 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
  25 (*
  26 Definition SurjectiveEnrichment `(ec:ECategory(Hom:=Vhom)(V:=V)(bin_obj':=Vbobj)(EI:=EI)) :=
  27   @treeDecomposition _ _
  28                   (fun t => match t with
  29                             | None   => EI
  30                             | Some x => match x with pair y z => Vhom y z end
  31                             end)
  32                   bin_obj.
  33 *)
  34
  35 (* in the paper this is called simply an "enrichment" *)
  36 Structure PreMonoidalEnrichment :=
  37 { enr_v_ob       : Type
  38 ; enr_v_hom      : enr_v_ob -> enr_v_ob -> Type
  39 ; enr_v          : Category enr_v_ob enr_v_hom
  40 ; enr_v_i        : enr_v_ob
  41 ; enr_v_bobj     : enr_v -> enr_v -> enr_v
  42 ; enr_v_bin      : BinoidalCat enr_v enr_v_bobj
  43 ; enr_v_pmon     : PreMonoidalCat enr_v_bin enr_v_i
  44 ; enr_v_mon      : MonoidalCat enr_v_pmon
  45 ; enr_c_obj      : Type
  46 ; enr_c_hom      : enr_c_obj -> enr_c_obj -> enr_v
  47 ; enr_c          : ECategory enr_v_mon enr_c_obj enr_c_hom
  48 ; enr_c_bin      : EBinoidalCat enr_c
  49 ; enr_c_i        : enr_c
  50 ; enr_c_pm       : PreMonoidalCat enr_c_bin enr_c_i
  51 }.
  52 Coercion enr_c   : PreMonoidalEnrichment >-> ECategory.
  53
  54 (*
  55 Structure MonoidalEnrichment {e:Enrichment} :=
  56 { me_enr         :=e
  57 ; me_fobj        : prod_obj e e -> e
  58 ; me_f           : Functor (e ×× e) e me_fobj
  59 ; me_i           : e
  60 ; me_mon         : MonoidalCat e me_fobj me_f me_i
  61 ; me_mf          : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
  62 }.
  63 Implicit Arguments MonoidalEnrichment [ ].
  64 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
  65 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
  66
  67 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
  68 Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
  69 { ffme_enr             := me
  70 ; ffme_mf_full         : FullFunctor         (HomFunctor e (me_i me))
  71 ; ffme_mf_faithful     : FaithfulFunctor     (HomFunctor e (me_i me))
  72 ; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
  73 }.
  74 Implicit Arguments MonicMonoidalEnrichment [ ].
  75 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
  76 Transparent HomFunctor.
  77
  78 Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
  79 { smme_se       : SurjectiveEnrichment e
  80 ; smme_monoidal : MonoidalEnrichment e
  81 ; smme_me       : MonicMonoidalEnrichment _ smme_monoidal
  82 }.
  83 Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
  84 Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
  85
  86 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
  87 Structure SMME :=
  88 { smme_e   : Enrichment
  89 ; smme_see : SurjectiveEnrichment smme_e
  90 ; smme_mon : MonoidalEnrichment smme_e
  91 ; smme_mee : MonicMonoidalEnrichment _ smme_mon
  92 }.
  93 Coercion smme_e   : SMME >-> Enrichment.
  94 Coercion smme_see : SMME >-> SurjectiveEnrichment.
  95 Coercion smme_mon : SMME >-> MonoidalEnrichment.
  96 Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.
  97 *)