X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowCategory.v;h=d98f85ace1934d03df00424a4ef1a154edc8e0b3;hp=cd43282c594abbe6aabf5ceed5b3576c48cf683b;hb=992203bb4a221ea2f415c0d14bb34d35af2ee637;hpb=f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index cd43282..d98f85a 100644
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.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 GeneralizedArrow.
+
+Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow.
+  admit.
+  Qed.