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

diff --git a/src/Reification.v b/src/Reification.v
index 932d78e..0daca47 100644
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -35,6 +35,11 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
 ; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
 ; 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
+
+(* 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 *)
+; reification_host_lang_pure   : CommutativeCat (enr_c_pm C)
 }.
 Transparent HomFunctor.
 Transparent functor_comp.