X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMain.v;h=2a054b7a57105b8847124dff667330dd8eb285bf;hp=2653fb8ed39e29046261b21613e6f9537b97c46b;hb=2403342ad32f12dd56a82ce575dd2d35d91f545a;hpb=ff3003c261295c60d367580b6700396102eb5a9c

diff --git a/src/Main.v b/src/Main.v
index 2653fb8..2a054b7 100644
--- a/src/Main.v
+++ b/src/Main.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
@@ -24,25 +23,31 @@ Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import FunctorCategories_ch7_7.
 Require Import Coherence_ch7_8.
+
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.
 Require Import MonoidalCategories_ch7_8.
+Require Import PreMonoidalCenter.
 
 Require Import Exponentials_ch6.
-Require Import CategoryOfCategories_ch7_1.
 Require Import Yoneda_ch8.
 Require Import Adjoints_ch9.
 
+(*Require Import CategoryOfCategories_ch7_1.*)
 (*Require Import PolynomialCategories.*)
 (*Require Import CoqCategory.*)
-(*Require Import NaturalDeduction.*)
-(*Require Import NaturalDeductionCategories.*)
-(*Require Import CartesianEnrichmentsHaveMonoidalRepresentableFunctors.*)
-(*Require Import Reification.*)
-(*Require Import GeneralizedArrow.*)
-(*Require Import ReificationFromGArrow.*)
-(*Require Import GArrowFromReification.*)
-(*Require Import Roundtrip.*)
-(*Require Import RoundtripSlides.*)
+(*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*)
+
+Require Import RepresentableStructure_ch7_2.
+
+Require Import EquivalentCategories_ch7_8.
+Require Import FreydAFT_ch9_8.
+Require Import KanExtension_ch9_6.
+Require Import LCCCs_ch9_7.
+Require Import Monads_ch10.
+Require Import NaturalNumbersObject_ch9_8.
+Require Import Presheaves_ch9_7.
 
 (* very slow! *)
-(*Require Import FreydCategories.*)
+Require Import FreydCategories.
 (*Require Import Arrows.*)