fix {Reification,GeneralizedArrow}Category

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

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.
 
-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