projects
/
coq-categories.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
split MonoidalCategories into Binoidal and PreMonoidal
[coq-categories.git]
/
src
/
Enrichment_ch2_8.v
diff --git
a/src/Enrichment_ch2_8.v
b/src/Enrichment_ch2_8.v
index
32a7701
..
84cc674
100644
(file)
--- a/
src/Enrichment_ch2_8.v
+++ b/
src/Enrichment_ch2_8.v
@@
-10,6
+10,8
@@
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
Require Import MonoidalCategories_ch7_8.
(******************************************************************************)
Require Import MonoidalCategories_ch7_8.
(******************************************************************************)
@@
-374,14
+376,14
@@
Structure Enrichment :=
Coercion enr_c : Enrichment >-> ECategory.
(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
Coercion enr_c : Enrichment >-> ECategory.
(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
-Structure SurjectiveEnrichment :=
-{ se_enr : Enrichment
-; se_decomp : @treeDecomposition (enr_v se_enr) (option ((enr_c_obj se_enr)*(enr_c_obj se_enr)))
+Structure SurjectiveEnrichment (e:Enrichment) :=
+{ se_enr := e
+; se_decomp : @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e)))
(fun t => match t with
(fun t => match t with
- | None => enr_v_i se_enr
- | Some x => match x with pair y z => enr_c_hom se_enr y z end
+ | None => enr_v_i e
+ | Some x => match x with pair y z => enr_c_hom e y z end
end)
end)
- (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (pair_obj d1 d2))
+ (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
}.
Coercion se_enr : SurjectiveEnrichment >-> Enrichment.
}.
Coercion se_enr : SurjectiveEnrichment >-> Enrichment.