temporarily comment out

[coq-hetmet.git] / src / ReificationsEquivalentToGeneralizedArrows.v

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index c8a7f72..bb5df17 100644 (file)
--- 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.