From 94c04c97042ab15b3ec62eba87ccccccd7162ce0 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 09:58:55 -0700 Subject: [PATCH] remove CategoryOfCategories, which isnt ready yet --- src/CategoryOfCategories_ch7_1.v | 55 -------------------------------------- src/Main.v | 2 +- 2 files changed, 1 insertion(+), 56 deletions(-) delete mode 100644 src/CategoryOfCategories_ch7_1.v diff --git a/src/CategoryOfCategories_ch7_1.v b/src/CategoryOfCategories_ch7_1.v deleted file mode 100644 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 --- 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. -- 1.7.10.4