X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=bb5df17fb0a5b55a99aea32e812b539509c7f18d;hp=c8a7f723cc31aea531bc99a3f2b48a75dd90b82d;hb=7300187652058f4c24fd4527d9a5833583959fb4;hpb=428a230cd3ddc9182695ddacaff9eabd67d954f7

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index c8a7f72..bb5df17 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -83,8 +83,9 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
-  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
+  (*
+  Theorem ReificationsAreGArrows :  IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
     admit.
-    Qed.
+    Qed.*)
 
 End ReificationsEquivalentToGeneralizedArrows.