X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationCategory.v;h=d271c024d85e0abd80a99faa45371e3bb452fd5c;hp=eb6b5fdec186cdb4b14784eb7b62ea848f6c4ef1;hb=ac32299199705b8824231454a21af4ca70eedd7f;hpb=e15a8b6d72e0b28af765acfda7ddad21b50704ee

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index eb6b5fd..d271c02 100644
--- 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