From 758bf2a48a733870dca601e5b03390d4271ad1c7 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 27 Mar 2011 12:22:12 -0700 Subject: [PATCH] add SurjectiveEnrichment to SMME --- src/RepresentableStructure_ch7_2.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v index 38d715d..05da4ee 100644 --- a/src/RepresentableStructure_ch7_2.v +++ b/src/RepresentableStructure_ch7_2.v @@ -178,9 +178,11 @@ Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *) Structure SMME := { smme_e : Enrichment +; smme_see : SurjectiveEnrichment smme_e ; smme_mon : MonoidalEnrichment smme_e ; smme_mee : MonicMonoidalEnrichment _ smme_mon }. Coercion smme_e : SMME >-> Enrichment. +Coercion smme_see : SMME >-> SurjectiveEnrichment. Coercion smme_mon : SMME >-> MonoidalEnrichment. Coercion smme_mee : SMME >-> MonicMonoidalEnrichment. -- 1.7.10.4