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.
25 Section WeakFunctorCategory.
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 :=
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)
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)
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
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
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.
63 unfold Proper; unfold respectful; simpl; intros.
65 apply small_func_comp_comp.
68 apply small_func_comp_comp.
69 eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0.
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.
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.
84 eapply if_comp ; [ idtac | apply small_func_comp_comp ].
88 eapply if_comp ; [ idtac | apply small_func_comp_comp ].
93 eapply small_func_comp_comp.
97 eapply small_func_comp_comp.
99 set (@if_associativity) as q.
100 apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)).
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.