1open HolKernel Parse boolLib boolSimps bossLib SatisfySimps categoryTheory functorTheory pred_setTheory limitTheory;
2
3val _ = new_theory "ens_cat";
4val _ = ParseExtras.temp_loose_equality()
5
6val HasFunType_def = Define`
7  HasFunType f X Y = extensional f X ��� ���x. x ��� X ��� f x ��� Y`;
8
9val IsTypedFun_def = Define`
10  IsTypedFun f = HasFunType f.map f.dom f.cod`;
11
12val TypedFun_ext = Q.store_thm(
13"TypedFun_ext",
14`���f g. IsTypedFun f ��� IsTypedFun g ���
15  ((f = g) = ((f.dom = g.dom) ��� (f.cod = g.cod) ��� (���x. x ��� f.dom ��� (f.map x = g.map x))))`,
16srw_tac [][morphism_component_equality,IsTypedFun_def,HasFunType_def,extensional_def] >>
17srw_tac [][EQ_IMP_THM] >>
18srw_tac [][FUN_EQ_THM] >>
19Cases_on `x ��� f.dom` >> srw_tac [][] >>
20pop_assum mp_tac >> srw_tac [][]);
21
22val TypedGraphFun_def = Define`
23  TypedGraphFun (X,Y) f = <|
24    dom := X; cod := Y; map := restrict f X |>`;
25
26val TypedGraphFun_components = Q.store_thm(
27"TypedGraphFun_components",
28`���X Y f. ((TypedGraphFun (X,Y) f).dom = X) ���
29         ((TypedGraphFun (X,Y) f).cod = Y) ���
30         ((TypedGraphFun (X,Y) f).map = restrict f X)`,
31srw_tac [][TypedGraphFun_def]);
32val _ = export_rewrites["TypedGraphFun_components"];
33
34val IsTypedFunTypedGraphFun = Q.store_thm(
35"IsTypedFunTypedGraphFun",
36`���f X Y. IsTypedFun (TypedGraphFun (X,Y) f) = ���x. x ��� X ��� f x ��� Y`,
37srw_tac [][EQ_IMP_THM,IsTypedFun_def,TypedGraphFun_def,HasFunType_def,restrict_def,extensional_def]);
38val _ = export_rewrites["IsTypedFunTypedGraphFun"];
39
40val TypedGraphFun_Ext = Q.store_thm(
41"TypedGraphFun_Ext",
42`���X Y f X' Y' f'. (TypedGraphFun (X,Y) f = TypedGraphFun (X',Y') f') ��� ((X = X') ��� (Y = Y') ��� ���x. x ��� X ��� (f x = f' x))`,
43srw_tac [][TypedGraphFun_def,restrict_def,EQ_IMP_THM] >> metis_tac []);
44
45val ComposeFun_def = Define`
46  ComposeFun (X,Y) g f = restrict ((restrict g Y) o f) X`;
47
48val ComposeTypedFun_def = Define`
49  ComposeTypedFun = compose (��f g. ComposeFun (f.dom,g.dom) g.map f.map)`;
50
51val _ = overload_on("o",``��g f. ComposeTypedFun f g``);
52val _ = overload_on("o",``��g f. (combin$o) g f``);
53
54val ComposeTypedFun_components = Q.store_thm(
55"ComposeTypedFun_components",
56`���f g. (f ���> g) ���
57((g o f).dom = f.dom) ���
58((g o f).cod = g.cod) ���
59((g o f).map = ComposeFun(f.dom,g.dom) g.map f.map)`,
60srw_tac [][ComposeTypedFun_def]);
61val _ = export_rewrites["ComposeTypedFun_components"];
62
63val IdFun_def = Define`
64  IdFun s = restrict I s`;
65
66val IdFunAp = Q.store_thm(
67"IdFunAp",
68`���x s. x ��� s ��� (IdFun s x = x)`,
69srw_tac [][IdFun_def,restrict_def]);
70val _ = export_rewrites["IdFunAp"];
71
72val IdFunType = Q.store_thm(
73"IdFunType",
74`���s. HasFunType (IdFun s) s s`,
75srw_tac [][HasFunType_def,IdFun_def]);
76val _ = export_rewrites["IdFunType"];
77
78val ComposeFunId = Q.store_thm(
79"ComposeFunId",
80`���X Y f. HasFunType f X Y ���
81(ComposeFun (X,X) f (IdFun X) = f) ���
82(ComposeFun (X,Y) (IdFun Y) f = f)`,
83srw_tac [][ComposeFun_def,IdFun_def,FUN_EQ_THM,HasFunType_def] >>
84fsrw_tac [][restrict_def,extensional_def] >>
85metis_tac []);
86val _ = export_rewrites["ComposeFunId"];
87
88val ComposeFunAssoc = Q.store_thm(
89"ComposeFunAssoc",
90`���a f b g c h ab bc ac.
91  HasFunType f a b ��� HasFunType g b c ���
92  (ab = (a,b)) ��� (bc = (b,c)) ��� (ac = (a,c)) ���
93  (ComposeFun ac h (ComposeFun ab g f) = ComposeFun ab (ComposeFun bc h g) f)`,
94srw_tac [][ComposeFun_def,FUN_EQ_THM] >>
95fsrw_tac [][HasFunType_def,extensional_def,restrict_def]);
96val _ = export_rewrites["ComposeFunAssoc"];
97
98val ComposeFunType = Q.store_thm(
99"ComposeFunType",
100`���X f Y g XY Z. HasFunType f X Y ��� HasFunType g Y Z ��� (XY = (X,Y)) ��� HasFunType (ComposeFun XY g f) X Z`,
101srw_tac [][HasFunType_def,ComposeFun_def] >>
102fsrw_tac [][extensional_def,restrict_def]);
103val _ = export_rewrites["ComposeFunType"];
104
105val _ = overload_on("IsTypedFunIn",``��U f. f.dom ��� U ��� f.cod ��� U ��� IsTypedFun f``);
106
107val ens_cat_def = Define`
108  ens_cat U = mk_cat <|
109    obj := U ;
110    mor := {f | IsTypedFunIn U f} ;
111    id_map := IdFun ;
112    comp := ��f g. (g o f).map |>`;
113
114val is_category_ens_cat = Q.store_thm(
115"is_category_ens_cat",
116`���U. is_category (ens_cat U)`,
117srw_tac [][ens_cat_def] >>
118srw_tac [][category_axioms_def] >- (
119  srw_tac [][maps_to_in_def,id_in_def,IsTypedFun_def,restrict_def] )
120>- (
121  srw_tac [][id_in_def,restrict_def] >>
122  srw_tac [][compose_in_def,restrict_def] >>
123  fsrw_tac [SATISFY_ss][IsTypedFun_def,morphism_component_equality] >>
124  fsrw_tac [][composable_in_def] >> fsrw_tac [][])
125>- (
126  srw_tac [][id_in_def,restrict_def] >>
127  srw_tac [][compose_in_def,restrict_def] >>
128  fsrw_tac [SATISFY_ss][IsTypedFun_def,morphism_component_equality] >>
129  fsrw_tac [][composable_in_def] >> fsrw_tac [][])
130>- (
131  fsrw_tac [][compose_in_def,restrict_def] >>
132  fsrw_tac [][composable_in_def] >>
133  fsrw_tac [][compose_def,restrict_def] >>
134  fsrw_tac [][IsTypedFun_def]) >>
135fsrw_tac [][maps_to_in_def] >>
136fsrw_tac [][compose_in_def,restrict_def,composable_in_def] >>
137fsrw_tac [][IsTypedFun_def]);
138val _ = export_rewrites["is_category_ens_cat"];
139
140val ens_cat_obj = Q.store_thm(
141"ens_cat_obj",
142`���U. (ens_cat U).obj = U`,
143srw_tac [][ens_cat_def]);
144
145val ens_cat_mor = Q.store_thm(
146"ens_cat_mor",
147`���U f. f ��� (ens_cat U).mor ��� IsTypedFunIn U f`,
148srw_tac [][ens_cat_def]);
149
150val ens_cat_id = Q.store_thm(
151"ens_cat_id",
152`���U x. x ��� U ��� ((id x -:(ens_cat U)) = TypedGraphFun (x,x) (IdFun x))`,
153srw_tac [][id_in_def,ens_cat_def,mk_cat_def,restrict_def,TypedGraphFun_def,IdFun_def]);
154
155val ens_cat_composable_in = Q.store_thm(
156"ens_cat_composable_in",
157`���U f g. f ���> g -:(ens_cat U) ��� IsTypedFunIn U f ��� IsTypedFunIn U g ��� f ���> g`,
158srw_tac [][composable_in_def,ens_cat_mor]);
159
160val ens_cat_comp = Q.store_thm(
161"ens_cat_comp",
162`���U f g. f ���> g -:(ens_cat U) ��� ((ens_cat U).comp f g = ComposeFun(f.dom,g.dom) g.map f.map)`,
163srw_tac [][ens_cat_def,mk_cat_def,restrict_def,composable_in_def]);
164
165val ens_cat_compose_in = Q.store_thm(
166"ens_cat_compose_in",
167`���U f g. f ���> g -:(ens_cat U) ��� (g o f -:(ens_cat U) = g o f)`,
168srw_tac [][compose_in_def,morphism_component_equality,ens_cat_comp,ens_cat_composable_in,restrict_def]>>
169metis_tac []);
170
171val ens_cat_maps_to_in = Q.store_thm(
172"ens_cat_maps_to_in",
173`���U f x y. f :- x ��� y -:(ens_cat U) ��� IsTypedFunIn U f ��� f :- x ��� y`,
174srw_tac [][maps_to_in_def,EQ_IMP_THM,ens_cat_mor]);
175
176val _ = export_rewrites[
177"ens_cat_obj","ens_cat_mor","ens_cat_id",
178"ens_cat_composable_in","ens_cat_comp",
179"ens_cat_compose_in","ens_cat_maps_to_in"];
180
181val ens_cat_empty_terminal = Q.store_thm(
182"ens_cat_empty_terminal",
183`���U. is_terminal (ens_cat U) ��� = ��� ��� U ��� ���x. x ��� U ��� (x = ���)`,
184srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >- (
185  first_x_assum (qspec_then `x` mp_tac) >>
186  srw_tac [][] >>
187  fsrw_tac [][IsTypedFun_def,HasFunType_def,EXTENSION] )
188>- (
189  qexists_tac `TypedGraphFun (���,���) ARB` >>
190  srw_tac [][] ) >>
191srw_tac [][TypedFun_ext]);
192
193Theorem ens_cat_terminal_objects:
194  ���U t. (���s. s ��� U ��� s ��� ���) ���
195  (is_terminal (ens_cat U) t = ���x. (t = {x}) ��� t ��� U)
196Proof
197  srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >>
198  srw_tac [][]
199  >- (srw_tac [][EXTENSION] >>
200      Cases_on ���t = {}���
201      >- (first_x_assum (qspec_then ���s��� mp_tac) >>
202          srw_tac [][] >>
203          disj1_tac >>
204          srw_tac [][] >>
205          Cases_on ���f.dom = s��� >> srw_tac [][] >>
206          Cases_on ���f.cod = ������ >> srw_tac [][] >>
207          srw_tac [][IsTypedFun_def,HasFunType_def,MEMBER_NOT_EMPTY] ) >>
208      qexists_tac ���CHOICE t��� >>
209      srw_tac [][EQ_IMP_THM,CHOICE_DEF] >>
210      first_x_assum (qspec_then ���t��� mp_tac) >>
211      srw_tac [][] >>
212      qmatch_assum_rename_tac ���x ��� f.cod��� >>
213      first_x_assum
214      (qspecl_then [���TypedGraphFun (f.dom,f.cod) (K x)���,
215                    ���TypedGraphFun (f.dom,f.cod) (K (CHOICE f.cod))���] mp_tac) >>
216      srw_tac [][CHOICE_DEF] >>
217      fsrw_tac [][morphism_component_equality,restrict_def] >>
218      qmatch_assum_abbrev_tac ���ff = gg��� >>
219      ���ff x = gg x��� by simp[] >>
220      pop_assum mp_tac >>
221      unabbrev_all_tac >>
222      qpat_x_assum ���x ��� f.cod��� mp_tac >>
223      simp_tac std_ss [] )
224  >- (qmatch_assum_rename_tac ���y ��� U��� >>
225      qexists_tac ���TypedGraphFun (y,{x}) (K x)��� >>
226      srw_tac [][] ) >>
227  srw_tac [][TypedFun_ext] >>
228  rpt (qpat_x_assum ���IsTypedFun X��� mp_tac) >>
229  fsrw_tac [][IsTypedFun_def,HasFunType_def]
230QED
231
232(*
233val ens_cat_has_binary_products = Q.store_thm(
234"ens_cat_has_binary_products",
235`���U J. (INJ J {{(x,y) | x ��� a ��� y ��� b} | a ��� U ��� b ��� U} U) ��� has_binary_products (ens_cat U)`,
236srw_tac [][has_binary_products_thm,is_binary_product_thm] >>
237`J {(x,y) | x ��� a ��� y ��� b} ��� U` by fsrw_tac [DNF_ss][INJ_DEF] >>
238qmatch_assum_abbrev_tac `J axb ��� U` >>
239qmatch_assum_abbrev_tac `INJ J UU U` >>
240qexists_tac `TypedGraphFun (J axb, a) (��p. (LINV J UU axb)` >>
241LINV_DEF
242srw_tac [][]
243``TypedGraphFun ((J:('a # 'a set -> 'a set)) (a,b), a)``
244``(LINV (J:(('a # 'a) set -> 'a set)) UU)``
245type_of it
246*)
247
248val pre_inclusion_functor_def = Define`
249  pre_inclusion_functor u1 u2 = <|
250    dom := ens_cat u1;
251    cod := ens_cat u2;
252    map := I|>`;
253
254val pre_inclusion_functor_components = Q.store_thm(
255"pre_inclusion_functor_components",
256`���u1 u2. ((pre_inclusion_functor u1 u2).dom = ens_cat u1) ���
257         ((pre_inclusion_functor u1 u2).cod = ens_cat u2) ���
258         (���f. f ��� (ens_cat u1).mor ��� ((pre_inclusion_functor u1 u2)##f = f)) ���
259         (���x. x ��� u1 ��� x ��� u2 ��� ((pre_inclusion_functor u1 u2)@@x = x))`,
260srw_tac [][pre_inclusion_functor_def,morf_def,objf_def] >>
261SELECT_ELIM_TAC >>
262conj_tac >- ( qexists_tac `x` >> srw_tac [][] ) >>
263srw_tac [][] >>
264pop_assum mp_tac >>
265fsrw_tac [][morphism_component_equality]);
266val _ = export_rewrites["pre_inclusion_functor_components"];
267
268val inclusion_functor_def = Define`
269  inclusion_functor u1 u2 = mk_functor (pre_inclusion_functor u1 u2)`;
270
271val inclusion_functor_components = Q.store_thm(
272"inclusion_functor_components",
273`���u1 u2. ((inclusion_functor u1 u2).dom = ens_cat u1) ���
274         ((inclusion_functor u1 u2).cod = ens_cat u2) ���
275         (���f. f ��� (ens_cat u1).mor ��� ((inclusion_functor u1 u2)##f = f)) ���
276         (���x. x ��� u1 ��� x ��� u2 ��� ((inclusion_functor u1 u2)@@x = x))`,
277srw_tac [][inclusion_functor_def]);
278val _ = export_rewrites["inclusion_functor_components"];
279
280val is_functor_inclusion_functor = Q.store_thm(
281"is_functor_inclusion_functor",
282`���u1 u2. u1 ��� u2 ��� is_functor (inclusion_functor u1 u2)`,
283srw_tac [][inclusion_functor_def] >>
284srw_tac [][functor_axioms_def] >>
285fsrw_tac [][SUBSET_DEF] >- (
286  qexists_tac `x` >> srw_tac [][] ) >>
287`(g o f) ��� (ens_cat u1).mor` by (
288  srw_tac [][] >> fsrw_tac [][IsTypedFun_def] ) >>
289srw_tac [][]);
290val _ = export_rewrites["is_functor_inclusion_functor"];
291
292val _ = export_theory();
293