clean up demo code

[coq-hetmet.git] / src / GeneralizedArrow.v

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index f246567..f246cbe 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -20,14 +20,23 @@ Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
+Require Import Enrichments.
 Require Import RepresentableStructure_ch7_2.
+Require Import PreMonoidalCenter.
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.
 
-Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) :=
-{ ga_functor_obj      : enr_v_mon K -> C
-; ga_functor          : Functor (enr_v_mon K) C ga_functor_obj
-; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor
+Class GeneralizedArrow (K:Enrichment)(C:Enrichment) :=
+{ ga_functor_obj      : enr_v K -> C
+; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm C) ga_functor_obj
+; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm C) ga_functor
+
+(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
+ * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
+ * host language, and toss on the inclusion functor to the full language *)
+; ga_host_lang_pure   : CommutativeCat (enr_c_pm C)
 }.
-Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
+Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
 
 Implicit Arguments GeneralizedArrow    [ ].
 Implicit Arguments ga_functor_obj      [ K C ].