update to new coq-categories, base ND_Relation on inert sequences

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

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index bf7743b..9149734 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -20,14 +20,22 @@ Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 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 RepresentableStructure_ch7_2.

+Require Import PreMonoidalCenter.
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.

 
 Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
 
 Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=

-{ 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
+{ ga_functor_obj      : enr_v K -> ce
+; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm ce) ga_functor_obj
+; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor
+(*
+; ga_functor          : Functor         (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj
+; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor
+*)

 }.
 }.

-Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
+Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.

 
 Implicit Arguments GeneralizedArrow    [ [ce] ].
 Implicit Arguments ga_functor_obj      [ K ce C ].
 
 Implicit Arguments GeneralizedArrow    [ [ce] ].
 Implicit Arguments ga_functor_obj      [ K ce C ].