fix {Reification,GeneralizedArrow}Category

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index d98f85a..974fdc3 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -24,6 +24,6 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import GeneralizedArrow.
 
 Require Import RepresentableStructure_ch7_2.
 Require Import GeneralizedArrow.
 

-Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow.
+Definition CategoryOfGeneralizedArrows : Category SMME (fun x y => @GeneralizedArrow x _ y).

   admit.
   Qed.
   admit.
   Qed.

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index eb6b5fd..d271c02 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -24,6 +24,6 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 

-Instance CategoryOfReifications : Category SMME Reification.
+Definition CategoryOfReifications : Category SMME (fun x y:SMME => Reification (smme_e x) (smme_e y) (mon_i (smme_mon y))).

   admit.
   Qed.
\ No newline at end of file
   admit.
   Qed.
\ No newline at end of file