X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationCategory.v;h=d271c024d85e0abd80a99faa45371e3bb452fd5c;hp=4d83b787e3b557fda6c6ccc410423499da39b75a;hb=428a230cd3ddc9182695ddacaff9eabd67d954f7;hpb=76f4613eaa5989e29bfd59d716c216ee5386c5f7

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 4d83b78..d271c02 100644
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -9,6 +9,21 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+Require Import 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