X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReification.v;h=932d78ef0890c816d8016435dda06ab796bc916e;hp=2b9aac9ad884a21fd1c99d1b39310bd6f8a2b44e;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hpb=562e94b529f34fb3854be7914a49190c5243c55a

diff --git a/src/Reification.v b/src/Reification.v
index 2b9aac9..932d78e 100644
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -33,13 +33,13 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
 ; reification_rstar_obj : enr_v K -> enr_v C
 ; reification_r         : forall k:K, Functor K C (reification_r_obj k)
 ; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
-; reification_rstar     :             MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
-; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
+; reification_rstar     :             PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
+; reification_commutes  : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
 }.
 Transparent HomFunctor.
 Transparent functor_comp.
 
-Coercion reification_rstar : Reification >-> MonoidalFunctor.
+Coercion reification_rstar : Reification >-> PreMonoidalFunctor.
 Implicit Arguments Reification                [ ].
 Implicit Arguments reification_r_obj          [ K C CI ].
 Implicit Arguments reification_r              [ K C CI ].