remove CategoryOfCategories, which isnt ready yet

diff --git a/src/CategoryOfCategories_ch7_1.v b/src/CategoryOfCategories_ch7_1.v
deleted file mode 100644 (file)
index 77ed028..0000000
--- a/src/CategoryOfCategories_ch7_1.v
+++ /dev/null
@@ -1,55 +0,0 @@
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import InitialTerminal_ch2_2.
-Require Import Subcategories_ch7_1.
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import Coherence_ch7_8.
-Require Import MonoidalCategories_ch7_8.
-Require Import Enrichment_ch2_8.
-
-(*******************************************************************************)
-(* Category of Categories enriched in some fixed category V                    *)
-
-Section CategoryOfCategories.
-
-  Context {VOb}{VHom}(V:Category VOb VHom){VI}{MFobj}{MF}(VM:MonoidalCat V VI MFobj MF).
-
-  Class ECat :=
-  { ecat_obj :  Type
-  ; ecat_hom :  ecat_obj -> ecat_obj -> VOb
-  ; ecat_cat :> ECategory VM ecat_obj ecat_hom
-  }.
-  Implicit Arguments ecat_obj [ ].
-  Implicit Arguments ecat_cat [ ].
-  Implicit Arguments ecat_hom [ ].
-  Instance ToECat {co}{ch}(c:ECategory VM co ch) : ECat := { ecat_cat := c }.
-
-  Class EFunc (C1 C2:ECat) :=
-  { efunc_fobj    : ecat_obj C1 -> ecat_obj C2
-  ; efunc_functor : EFunctor (ecat_cat C1) (ecat_cat C2) efunc_fobj
-  }.
-  Implicit Arguments efunc_fobj    [ C1 C2 ].
-  Implicit Arguments efunc_functor [ C1 C2 ].
-  Instance ToEFunc {C1}{C2}{eo}(F:EFunctor (ecat_cat C1) (ecat_cat C2) eo)
-     : EFunc C1 C2 := { efunc_functor := F }.
-
-  (* FIXME: should be enriched in whatever V is enriched in *)
-  Instance CategoryOfCategories : Category ECat EFunc :=
-  { id    := fun c                                     => ToEFunc (efunctor_id (ecat_cat c))
-(*  ; eqv   := fun c1 c2 f1 f2                           => f1 ≃ f2 *)
-  ; comp  := fun c1 c2 c3 (g:EFunc c1 c2)(f:EFunc c2 c3) => ToEFunc (efunctor_comp _ _ _ (efunc_functor g) (efunc_functor f))
-  }.
-  admit.
-  admit.
-  admit.
-  Defined.
-
-  (* FIXME: show that subcategories are monos in __Cat__ *)
-
-End CategoryOfCategories.

diff --git a/src/Main.v b/src/Main.v
index 2653fb8..5ef4f55 100644 (file)
--- a/src/Main.v
+++ b/src/Main.v
@@ -27,7 +27,7 @@ Require Import Coherence_ch7_8.
 Require Import MonoidalCategories_ch7_8.
 
 Require Import Exponentials_ch6.
-Require Import CategoryOfCategories_ch7_1.
+(*Require Import CategoryOfCategories_ch7_1.*)
 Require Import Yoneda_ch8.
 Require Import Adjoints_ch9.