ProgrammingLanguage.v: add definitions for TypesL_{first,second}

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

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index 5b4c5ef..1b626a2 100644 (file)
--- 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.