X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsAndGeneralizedArrows.v;h=7924a43a52d546fc01af0b5b3eee54529c6add78;hp=4056c779052ba2fd53fd93df63bfb12439b56850;hb=e539b49ae3148ab1967b5ea0709734171180b86d;hpb=4e5aa4bcc6024aa7add9c1bf1c2ad9fd2a6a3685

diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v
index 4056c77..7924a43 100644
--- a/src/ReificationsAndGeneralizedArrows.v
+++ b/src/ReificationsAndGeneralizedArrows.v
@@ -71,9 +71,8 @@ Section ReificationsEquivalentToGeneralizedArrows.
     Qed.
 
   Lemma roundtrip_garrow_to_garrow
-    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM)
+    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
     : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
-
     apply if_inv.
     eapply if_comp.
     eapply if_inv.