1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import General.
4 Require Import Categories_ch1_3.
5 Require Import Functors_ch1_4.
6 Require Import Isomorphisms_ch1_5.
7 Require Import ProductCategories_ch1_6_1.
8 Require Import InitialTerminal_ch2_2.
9 Require Import Subcategories_ch7_1.
10 Require Import NaturalTransformations_ch7_4.
11 Require Import NaturalIsomorphisms_ch7_5.
12 Require Import Coherence_ch7_8.
13 Require Import MonoidalCategories_ch7_8.
14 Require Import Enrichment_ch2_8.
16 (*******************************************************************************)
17 (* Category of Categories enriched in some fixed category V *)
19 Section CategoryOfCategories.
21 Context {VOb}{VHom}(V:Category VOb VHom){VI}{MFobj}{MF}(VM:MonoidalCat V VI MFobj MF).
25 ; ecat_hom : ecat_obj -> ecat_obj -> VOb
26 ; ecat_cat :> ECategory VM ecat_obj ecat_hom
28 Implicit Arguments ecat_obj [ ].
29 Implicit Arguments ecat_cat [ ].
30 Implicit Arguments ecat_hom [ ].
31 Instance ToECat {co}{ch}(c:ECategory VM co ch) : ECat := { ecat_cat := c }.
33 Class EFunc (C1 C2:ECat) :=
34 { efunc_fobj : ecat_obj C1 -> ecat_obj C2
35 ; efunc_functor : EFunctor (ecat_cat C1) (ecat_cat C2) efunc_fobj
37 Implicit Arguments efunc_fobj [ C1 C2 ].
38 Implicit Arguments efunc_functor [ C1 C2 ].
39 Instance ToEFunc {C1}{C2}{eo}(F:EFunctor (ecat_cat C1) (ecat_cat C2) eo)
40 : EFunc C1 C2 := { efunc_functor := F }.
42 (* FIXME: should be enriched in whatever V is enriched in *)
43 Instance CategoryOfCategories : Category ECat EFunc :=
44 { id := fun c => ToEFunc (efunctor_id (ecat_cat c))
45 (* ; eqv := fun c1 c2 f1 f2 => f1 ≃ f2 *)
46 ; comp := fun c1 c2 c3 (g:EFunc c1 c2)(f:EFunc c2 c3) => ToEFunc (efunctor_comp _ _ _ (efunc_functor g) (efunc_functor f))
53 (* FIXME: show that subcategories are monos in __Cat__ *)
55 End CategoryOfCategories.