1 (*********************************************************************************************************************************)
5 (*********************************************************************************************************************************)
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.
27 (* in the paper this is called simply an "enrichment" *)
28 Structure Enrichment :=
30 ; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
31 ; enr_v : Category enr_v_ob enr_v_hom
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
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
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
46 Coercion enr_c : Enrichment >-> ECategory.
48 Structure SurjectiveEnrichment :=
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
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
62 ; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i
65 Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
67 {| enr_v_ob := senr_v_ob se
68 ; enr_v_hom := senr_v_hom 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
78 ; enr_c_bin := senr_c_bin se
79 ; enr_c_i := senr_c_i se
80 ; enr_c_pm := senr_c_pm se
83 Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
86 Definition MonoidalEnrichment (e:Enrichment) :=
90 (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))).
92 Definition MonoidalEnrichment (e:Enrichment) :=
96 (HomFunctor e (pmon_I (enr_c_pm e))).
99 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
101 Definition SurjectiveEnrichment (ec:Enrichment) :=
102 @treeDecomposition (enr_v ec) (option (ec*ec))
103 (fun t => match t with
105 | Some x => match x with pair y z => enr_c_hom ec y z end
110 Class MonicEnrichment {e:Enrichment} :=
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
118 Implicit Arguments MonicEnrichment [ ].
119 Coercion me_enr : MonicEnrichment >-> Enrichment.
120 Transparent HomFunctor.
122 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
124 { smme_e : SurjectiveEnrichment
125 (*; smme_see : SurjectiveEnrichment smme_e*)
126 ; smme_mon : MonoidalEnrichment smme_e
127 ; smme_mee : MonicEnrichment smme_e
129 Coercion smme_e : SMME >-> SurjectiveEnrichment.
130 Coercion smme_mon : SMME >-> MonoidalEnrichment.
132 Definition SMMEs : SmallCategories.
133 refine {| small_cat := SMME
134 ; small_cat_cat := fun smme => enr_v smme