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.
24 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
26 Definition SurjectiveEnrichment `(ec:ECategory(Hom:=Vhom)(V:=V)(bin_obj':=Vbobj)(EI:=EI)) :=
27 @treeDecomposition _ _
28 (fun t => match t with
30 | Some x => match x with pair y z => Vhom y z end
35 (* in the paper this is called simply an "enrichment" *)
36 Structure PreMonoidalEnrichment :=
38 ; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
39 ; enr_v : Category enr_v_ob enr_v_hom
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
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
50 ; enr_c_pm : PreMonoidalCat enr_c_bin enr_c_i
52 Coercion enr_c : PreMonoidalEnrichment >-> ECategory.
55 Structure MonoidalEnrichment {e:Enrichment} :=
57 ; me_fobj : prod_obj e e -> e
58 ; me_f : Functor (e ×× e) e me_fobj
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)
63 Implicit Arguments MonoidalEnrichment [ ].
64 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
65 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
67 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
68 Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
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))
74 Implicit Arguments MonicMonoidalEnrichment [ ].
75 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
76 Transparent HomFunctor.
78 Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
79 { smme_se : SurjectiveEnrichment e
80 ; smme_monoidal : MonoidalEnrichment e
81 ; smme_me : MonicMonoidalEnrichment _ smme_monoidal
83 Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
84 Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
86 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
89 ; smme_see : SurjectiveEnrichment smme_e
90 ; smme_mon : MonoidalEnrichment smme_e
91 ; smme_mee : MonicMonoidalEnrichment _ smme_mon
93 Coercion smme_e : SMME >-> Enrichment.
94 Coercion smme_see : SMME >-> SurjectiveEnrichment.
95 Coercion smme_mon : SMME >-> MonoidalEnrichment.
96 Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.