ReificationsIsomorphicToGeneralizedArrows: use EqDep
[coq-hetmet.git] / src / ReificationsEquivalentToGeneralizedArrows.v
index c8a7f72..0428638 100644 (file)
@@ -83,8 +83,4 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
-  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
-    admit.
-    Qed.
-
 End ReificationsEquivalentToGeneralizedArrows.