src/CategoryOfCategories_ch7_1.v

   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.
  15
  16 (*******************************************************************************)
  17 (* Category of Categories enriched in some fixed category V                    *)
  18
  19 Section CategoryOfCategories.
  20
  21   Context {VOb}{VHom}(V:Category VOb VHom){VI}{MFobj}{MF}(VM:MonoidalCat V VI MFobj MF).
  22
  23   Class ECat :=
  24   { ecat_obj :  Type
  25   ; ecat_hom :  ecat_obj -> ecat_obj -> VOb
  26   ; ecat_cat :> ECategory VM ecat_obj ecat_hom
  27   }.
  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 }.
  32
  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
  36   }.
  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 }.
  41
  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))
  47   }.
  48   admit.
  49   admit.
  50   admit.
  51   Defined.
  52
  53   (* FIXME: show that subcategories are monos in __Cat__ *)
  54
  55 End CategoryOfCategories.