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