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.
 109
 110 (*
 111 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
 112   reflexivity proved by  (@Equivalence_Reflexive  _ _ (eqv_equivalence a b))
 113   symmetry proved by     (@Equivalence_Symmetric  _ _ (eqv_equivalence a b))
 114   transitivity proved by (@Equivalence_Transitive _ _ (eqv_equivalence a b))
 115   as parametric_relation_eqv.
 116   Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
 117   with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
 118   auto.
 119   Defined.*)
 120
 121 Section WeakFunctorCategoryIsomorphism.
 122   (* Here we sort of set up exactly the conditions needed to trigger
 123    * the ReificationsAreGeneralizedArrows proof; again, I'm doing it here
 124    * because the instant I import Reification or GeneralizedArrow, Coq
 125    * becomes nearly unusable.  *)
 126
 127   (* same objects (SMME's) for both categories, and the functor is IIO *)
 128   Context {SMMEs:SmallCategories}.
 129   Context {GA:@SmallFunctors SMMEs}.
 130   Context {RE:@SmallFunctors SMMEs}.
 131
 132   Context (M1:forall c1 c2, (c1~~{GA}~~>c2) -> (c1~~{RE}~~>c2)).
 133   Context (M2:forall c1 c2, (c1~~{RE}~~>c2) -> (c1~~{GA}~~>c2)).
 134   Implicit Arguments M1 [[c1][c2]].
 135   Implicit Arguments M2 [[c1][c2]].
 136
 137   Section GeneralCase.
 138     Context (m1_respects_eqv
 139       : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2) (g:c1~~{GA}~~>c2),
 140                (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func RE (M1 f) ≃ small_func_func RE (M1 g)).
 141     Context (m2_respects_eqv
 142       : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2) (g:c1~~{RE}~~>c2),
 143                (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func GA (M2 f) ≃ small_func_func GA (M2 g)).
 144     Context (m1_preserves_id
 145       : forall c1, small_func_func _ (M1 (small_func_id GA c1)) ≃ small_func_id RE c1).
 146     Context (m2_preserves_id
 147       : forall c1, small_func_func _ (M2 (small_func_id RE c1)) ≃ small_func_id GA c1).
 148     Context (m1_respects_comp :
 149       forall (c1 c2 c3:SMMEs) (f:c1~~{GA}~~>c2) (g:c2~~{GA}~~>c3),
 150         small_func_func _ (small_func_comp _ (M1 f) (M1 g)) ≃
 151         small_func_func _ ((M1 (small_func_comp _ f g)))).
 152     Context (m2_respects_comp :
 153       forall (c1 c2 c3:SMMEs) (f:c1~~{RE}~~>c2) (g:c2~~{RE}~~>c3),
 154         small_func_func _ (small_func_comp _ (M2 f) (M2 g)) ≃
 155         small_func_func _ ((M2 (small_func_comp _ f g)))).
 156     Context (m1_m2_id
 157       : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2),
 158         small_func_func _ (M2 (M1 f)) ≃ small_func_func _ f).
 159     Context (m2_m1_id
 160       : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2),
 161         small_func_func _ (M1 (M2 f)) ≃ small_func_func _ f).
 162
 163     Definition F1 : Functor GA RE (fun x => x).
 164       refine  {| fmor := fun a b f => M1 f |}.
 165       intros.
 166         unfold eqv; simpl.
 167         apply m1_respects_eqv.
 168         apply H.
 169       intros.
 170         unfold eqv; simpl; intros.
 171         apply m1_preserves_id.
 172       intros.
 173         unfold eqv; simpl.
 174         set m1_respects_comp as q.
 175         unfold eqv in q.
 176         apply q.
 177         Defined.
 178
 179     Definition F2 : Functor RE GA (fun x => x).
 180       refine  {| fmor := fun a b f => M2 f |}.
 181       intros.
 182         unfold eqv; simpl.
 183         apply m2_respects_eqv.
 184         apply H.
 185       intros.
 186         unfold eqv; simpl; intros.
 187         apply m2_preserves_id.
 188       intros.
 189         unfold eqv; simpl.
 190         set m2_respects_comp as q.
 191         unfold eqv in q.
 192         apply q.
 193         Defined.
 194
 195     Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
 196       apply Build_IsomorphicCategories.
 197       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 198         eapply if_comp.
 199         apply m1_m2_id.
 200         apply H.
 201       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
 202         eapply if_comp.
 203         apply m2_m1_id.
 204         apply H.
 205         Qed.
 206
 207   End GeneralCase.
 208 (*
 209   (* now, the special case we can really use: M1 and M2 each consist of post-composition *)
 210   Section WeakFunctorCategoryPostCompositionIsomorphism.
 211
 212     Context (M1_postcompose_obj : forall c1:SMMEs, c1 -> c1).
 213     Context (M1_postcompose     : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)).
 214
 215     Context (M2_postcompose_obj : forall c1:SMMEs, c1 -> c1).
 216     Context (M2_postcompose     : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)).
 217
 218     Context (M1_M2_id           : forall c1:SMMEs, M1_postcompose c1 >>>> M2_postcompose c1 ≃ functor_id _).
 219     Context (M2_M1_id           : forall c1:SMMEs, M2_postcompose c1 >>>> M1_postcompose c1 ≃ functor_id _).
 220
 221     Context (M1_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{GA}~~>c2),
 222       small_func_func _ (M1 f) ≃ small_func_func _ f >>>> M1_postcompose c2).
 223     Context (M2_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{RE}~~>c2),
 224       small_func_func _ (M2 f) ≃ small_func_func _ f >>>> M2_postcompose c2).
 225
 226     Definition F1' : Functor GA RE (fun x => x).
 227       apply F1; intros; simpl.
 228         eapply if_comp.
 229         apply M1_postcompose_act.
 230         apply if_inv.
 231         eapply if_comp.
 232         apply M1_postcompose_act.
 233         apply if_respects; try apply if_id.
 234         apply if_inv; auto.
 235       apply (if_comp (M1_postcompose_act _ _ _)).
 236         apply M1_postcompose_act.
 237
 238
 239     Theorem WeakFunctorCategoryPostCompositionIsomorphism : IsomorphicCategories GA RE F1 F2
 240     End WeakFunctorCategoryPostCompositionIsomorphism.
 241     *)
 242 End WeakFunctorCategoryIsomorphism.
 243
 244