X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=1b626a2aea54fdaf4d925436909122d403cd5bc8;hp=5b4c5efde745ea3318991419eb3253824111b2f8;hb=61fb093700aab006b77998d1cbd30235e144ca1f;hpb=76f4613eaa5989e29bfd59d716c216ee5386c5f7

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index 5b4c5ef..1b626a2 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -23,8 +23,8 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
-Require Import GArrowFromReification.
-Require Import ReificationFromGArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.
 Require Import ReificationCategory.
 Require Import GeneralizedArrowCategory.
 
@@ -83,4 +83,8 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
+  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
+    admit.
+    Qed.
+
 End ReificationsEquivalentToGeneralizedArrows.