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 (*Require Import Enrichment_ch2_8.*)
  25 (*Require Import RepresentableStructure_ch7_2.*)
  26
  27 Section WeakFunctorCategory.
  28
  29   (* We can't handle categories directly due to size issues.
  30    * Therefore, we ask the user to supply two types "Cat" and "Mor"
  31    * which index the "small categories"; we then construct a large
  32    * category relative to those. *)
  33   Structure SmallCategories :=
  34   { small_cat       : Type
  35   ; small_ob        : small_cat -> Type
  36   ; small_hom       : forall c:small_cat, small_ob c -> small_ob c -> Type
  37   ; small_cat_cat   : forall c:small_cat, Category (small_ob c) (small_hom c)
  38   }.
  39
  40   Context {sc:SmallCategories}.
  41   Structure SmallFunctors :=
  42   { small_func       : small_cat sc -> small_cat sc -> Type
  43   ; small_func_fobj  : forall {c1}{c2}, small_func c1 c2 -> (small_ob sc c1 -> small_ob sc c2)
  44   ; 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)
  45
  46   (* proof that our chosen indexing contains identity functors and is closed under composition *)
  47   ; small_func_id    : forall  c1 , small_func c1 c1
  48   ; small_func_id_id : forall {c1}, small_func_func (small_func_id c1) ≃ functor_id (small_cat_cat sc c1)
  49   ; small_func_comp  : forall {c1}{c2}{c3}, small_func c1 c2 -> small_func c2 c3 -> small_func c1 c3
  50   ; small_func_comp_comp : forall {c1}{c2}{c3}(f:small_func c1 c2)(g:small_func c2 c3),
  51     small_func_func (small_func_comp f g) ≃ small_func_func f >>>> small_func_func g
  52   }.
  53
  54   Instance WeakFunctorCategory `(sf:SmallFunctors) : Category (small_cat sc) (small_func sf) :=
  55   { id   := fun a         => small_func_id sf a
  56   ; comp := fun a b c f g => small_func_comp sf f g
  57   ; eqv  := fun a b f g   => small_func_func sf f ≃ small_func_func sf g
  58   }.
  59     intros; simpl.
  60     apply Build_Equivalence.
  61       unfold Reflexive; simpl; intros; apply if_id.
  62       unfold Symmetric; simpl; intros; apply if_inv; auto.
  63       unfold Transitive; simpl; intros; eapply if_comp. apply H. apply H0.
  64     intros; simpl.
  65       unfold Proper; unfold respectful; simpl; intros.
  66       eapply if_comp.
  67       apply small_func_comp_comp.
  68       eapply if_inv.
  69       eapply if_comp.
  70       apply small_func_comp_comp.
  71       eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0.
  72     intros; simpl.
  73       eapply if_comp.
  74       apply small_func_comp_comp.
  75       eapply if_comp; [ idtac | apply if_left_identity ].
  76       eapply if_respects; try apply if_id.
  77       apply small_func_id_id.
  78     intros; simpl.
  79       eapply if_comp.
  80       apply small_func_comp_comp.
  81       eapply if_comp; [ idtac | apply if_right_identity ].
  82       eapply if_respects; try apply if_id.
  83       apply small_func_id_id.
  84     intros; simpl.
  85       eapply if_comp.
  86       eapply if_comp ; [ idtac | apply small_func_comp_comp ].
  87       apply if_id.
  88       apply if_inv.
  89       eapply if_comp.
  90       eapply if_comp ; [ idtac | apply small_func_comp_comp ].
  91       apply if_id.
  92       eapply if_comp.
  93       eapply if_respects.
  94       eapply if_id.
  95       eapply small_func_comp_comp.
  96       apply if_inv.
  97       eapply if_comp.
  98       eapply if_respects.
  99       eapply small_func_comp_comp.
 100       eapply if_id.
 101       set (@if_associativity) as q.
 102       apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)).
 103       Defined.
 104 End WeakFunctorCategory.
 105 Coercion WeakFunctorCategory : SmallFunctors >-> Category.
 106 Coercion small_func_func : small_func >-> Functor.
 107 Coercion small_cat_cat : small_cat >-> Category.
 108 Coercion small_cat : SmallCategories >-> Sortclass.