src/WeakFunctorCategory.v

   1 (*********************************************************************************************************************************)
   2 (* WeakFunctorCategory:                                                                                                          *)
   3 (*                                                                                                                               *)
   4 (*   A category whose morphisms are functors, identified up to natural isomorphism (not equality).  This pulls most of the       *)
   5 (*   heavy lifting out of ReificationsEquivalentToGeneralizedArrows, since the definitions in that context cause Coq to bog      *)
   6 (*   down and run unbearably slowly                                                                                              *)
   7 (*                                                                                                                               *)
   8 (*********************************************************************************************************************************)
   9
  10 Generalizable All Variables.
  11 Require Import Preamble.
  12 Require Import General.
  13 Require Import Categories_ch1_3.
  14 Require Import Functors_ch1_4.
  15 Require Import Isomorphisms_ch1_5.
  16 Require Import ProductCategories_ch1_6_1.
  17 Require Import OppositeCategories_ch1_6_2.
  18 Require Import Enrichment_ch2_8.
  19 Require Import Subcategories_ch7_1.
  20 Require Import NaturalTransformations_ch7_4.
  21 Require Import NaturalIsomorphisms_ch7_5.
  22 Require Import MonoidalCategories_ch7_8.
  23 Require Import Coherence_ch7_8.
  24
  25 Section WeakFunctorCategory.
  26
  27   (* We can't handle categories directly due to size issues.
  28    * Therefore, we ask the user to supply two types "Cat" and "Mor"
  29    * which index the "small categories"; we then construct a large
  30    * category relative to those. *)
  31   Structure SmallCategories :=
  32   { small_cat       : Type
  33   ; small_ob        : small_cat -> Type
  34   ; small_hom       : forall c:small_cat, small_ob c -> small_ob c -> Type
  35   ; small_cat_cat   : forall c:small_cat, Category (small_ob c) (small_hom c)
  36   }.
  37
  38   Context {sc:SmallCategories}.
  39   Structure SmallFunctors :=
  40   { small_func       : small_cat sc -> small_cat sc -> Type
  41   ; small_func_fobj  : forall {c1}{c2}, small_func c1 c2 -> (small_ob sc c1 -> small_ob sc c2)
  42   ; small_func_func  : forall {c1}{c2}(f:small_func c1 c2), Functor (small_cat_cat sc c1) (small_cat_cat sc c2) (small_func_fobj f)
  43
  44   (* proof that our chosen indexing contains identity functors and is closed under composition *)
  45   ; small_func_id    : forall  c1 , small_func c1 c1
  46   ; small_func_id_id : forall {c1}, small_func_func (small_func_id c1) ≃ functor_id (small_cat_cat sc c1)
  47   ; small_func_comp  : forall {c1}{c2}{c3}, small_func c1 c2 -> small_func c2 c3 -> small_func c1 c3
  48   ; small_func_comp_comp : forall {c1}{c2}{c3}(f:small_func c1 c2)(g:small_func c2 c3),
  49     small_func_func (small_func_comp f g) ≃ small_func_func f >>>> small_func_func g
  50   }.
  51
  52   Instance WeakFunctorCategory `(sf:SmallFunctors) : Category (small_cat sc) (small_func sf) :=
  53   { id   := fun a         => small_func_id sf a
  54   ; comp := fun a b c f g => small_func_comp sf f g
  55   ; eqv  := fun a b f g   => small_func_func sf f ≃ small_func_func sf g
  56   }.
  57     intros; simpl.
  58     apply Build_Equivalence.
  59       unfold Reflexive; simpl; intros; apply if_id.
  60       unfold Symmetric; simpl; intros; apply if_inv; auto.
  61       unfold Transitive; simpl; intros; eapply if_comp. apply H. apply H0.
  62     intros; simpl.
  63       unfold Proper; unfold respectful; simpl; intros.
  64       eapply if_comp.
  65       apply small_func_comp_comp.
  66       eapply if_inv.
  67       eapply if_comp.
  68       apply small_func_comp_comp.
  69       eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0.
  70     intros; simpl.
  71       eapply if_comp.
  72       apply small_func_comp_comp.
  73       eapply if_comp; [ idtac | apply if_left_identity ].
  74       eapply if_respects; try apply if_id.
  75       apply small_func_id_id.
  76     intros; simpl.
  77       eapply if_comp.
  78       apply small_func_comp_comp.
  79       eapply if_comp; [ idtac | apply if_right_identity ].
  80       eapply if_respects; try apply if_id.
  81       apply small_func_id_id.
  82     intros; simpl.
  83       eapply if_comp.
  84       eapply if_comp ; [ idtac | apply small_func_comp_comp ].
  85       apply if_id.
  86       apply if_inv.
  87       eapply if_comp.
  88       eapply if_comp ; [ idtac | apply small_func_comp_comp ].
  89       apply if_id.
  90       eapply if_comp.
  91       eapply if_respects.
  92       eapply if_id.
  93       eapply small_func_comp_comp.
  94       apply if_inv.
  95       eapply if_comp.
  96       eapply if_respects.
  97       eapply small_func_comp_comp.
  98       eapply if_id.
  99       set (@if_associativity) as q.
 100       apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)).
 101       Defined.
 102 End WeakFunctorCategory.
 103 Coercion WeakFunctorCategory : SmallFunctors >-> Category.
 104 Coercion small_func_func : small_func >-> Functor.
 105 Coercion small_cat_cat : small_cat >-> Category.
 106 Coercion small_cat : SmallCategories >-> Sortclass.