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.
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.
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. *)
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}.
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]].
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)))).
157 : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2),
158 small_func_func _ (M2 (M1 f)) ≃ small_func_func _ f).
160 : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2),
161 small_func_func _ (M1 (M2 f)) ≃ small_func_func _ f).
163 Definition F1 : Functor GA RE (fun x => x).
164 refine {| fmor := fun a b f => M1 f |}.
167 apply m1_respects_eqv.
170 unfold eqv; simpl; intros.
171 apply m1_preserves_id.
174 set m1_respects_comp as q.
179 Definition F2 : Functor RE GA (fun x => x).
180 refine {| fmor := fun a b f => M2 f |}.
183 apply m2_respects_eqv.
186 unfold eqv; simpl; intros.
187 apply m2_preserves_id.
190 set m2_respects_comp as q.
195 Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
196 refine {| ic_f := F1 ; ic_g := F2 |}.
197 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
201 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
209 (* now, the special case we can really use: M1 and M2 each consist of post-composition *)
210 Section WeakFunctorCategoryPostCompositionIsomorphism.
212 Context (M1_postcompose_obj : forall c1:SMMEs, c1 -> c1).
213 Context (M1_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)).
215 Context (M2_postcompose_obj : forall c1:SMMEs, c1 -> c1).
216 Context (M2_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)).
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 _).
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).
226 Definition F1' : Functor GA RE (fun x => x).
227 apply F1; intros; simpl.
229 apply M1_postcompose_act.
232 apply M1_postcompose_act.
233 apply if_respects; try apply if_id.
235 apply (if_comp (M1_postcompose_act _ _ _)).
236 apply M1_postcompose_act.
239 Theorem WeakFunctorCategoryPostCompositionIsomorphism : IsomorphicCategories GA RE F1 F2
240 End WeakFunctorCategoryPostCompositionIsomorphism.
242 End WeakFunctorCategoryIsomorphism.