--- /dev/null
+(*********************************************************************************************************************************)
+(* ReificationCategory: *)
+(* *)
+(* There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms *)
+(* are reifications *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.