X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowCategory.v;h=745484b91ca9639873fd681e18d9ea63cea2a1ef;hp=3a6a74a5b64d18ea65f453b1b52427c879a1a9c2;hb=77e8c70f4fd7a32db036fee5884a98208d450de2;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index 3a6a74a..745484b 100644
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -62,6 +62,8 @@ Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1
 Instance compose_generalizedArrows (s0 s1 s2:SMMEs) 
   (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 :=
     { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }.
+  apply ga_host_lang_pure.
+  Defined.
 
 Definition generalizedArrowOrIdentityComp
   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.