1 (*********************************************************************************************************************************)
2 (* WeakFunctorCategory: *)
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 *)
8 (*********************************************************************************************************************************)
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.*)
27 Section WeakFunctorCategory.
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 :=
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)
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)
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
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
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.
65 unfold Proper; unfold respectful; simpl; intros.
67 apply small_func_comp_comp.
70 apply small_func_comp_comp.
71 eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0.
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.
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.
86 eapply if_comp ; [ idtac | apply small_func_comp_comp ].
90 eapply if_comp ; [ idtac | apply small_func_comp_comp ].
95 eapply small_func_comp_comp.
99 eapply small_func_comp_comp.
101 set (@if_associativity) as q.
102 apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)).
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.