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.