X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=1b626a2aea54fdaf4d925436909122d403cd5bc8;hp=a81c895c0ba04215100e4f61614795bc8f7ac80d;hb=992203bb4a221ea2f415c0d14bb34d35af2ee637;hpb=f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index a81c895..1b626a2 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -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.