1 (*********************************************************************************************************************************)
2 (* ReificationCategory: *)
4 (* There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms *)
7 (*********************************************************************************************************************************)
9 Generalizable All Variables.
10 Require Import Preamble.
11 Require Import General.
12 Require Import NaturalDeduction.
13 Require Import Coq.Strings.String.
14 Require Import Coq.Lists.List.