1open HolKernel Parse boolLib bossLib lcsymtacs categoryTheory functorTheory;
2
3val _ = new_theory "nat_trans";
4
5val _ = type_abbrev("nat_trans",
6``:((��,��,��,��) functor,(��,��,��,��) functor,
7    �� -> (��,��) mor) morphism``);
8
9val _ = overload_on("ntdom", ``��n. n.dom.dom``);
10val _ = overload_on("ntcod", ``��n. n.cod.cod``);
11val _ = set_fixity "@+" (Infixl 2000);
12val _ = overload_on("@+", ``��(n:(��,��,��,��) nat_trans) x. n.map x``);
13
14val extensional_nat_trans_def = Define`
15  extensional_nat_trans n = extensional n.map (ntdom n).obj`;
16
17val nat_trans_axioms_def = Define`
18  nat_trans_axioms n =
19    is_functor n.dom ���
20    is_functor n.cod ���
21    (n.dom.dom = n.cod.dom) ���
22    (n.dom.cod = n.cod.cod) ���
23    (���x. x ��� (ntdom n).obj ���
24           (n@+x) :- (n.dom@@x) ��� (n.cod@@x) -:(ntcod n)) ���
25    (���f x y. f :- x ��� y -:(ntdom n) ���
26      (n@+y o (n.dom##f) -:(ntcod n) = (n.cod##f) o n@+x -:(ntcod n)))`;
27
28val is_nat_trans_def = Define`
29  is_nat_trans n = extensional_nat_trans n ��� nat_trans_axioms n`;
30
31val mk_nt_def = Define`
32  mk_nt n = <| dom := n.dom; cod := n.cod; map := restrict n.map (ntdom n).obj |>`;
33
34val mk_nt_dom = Q.store_thm(
35"mk_nt_dom",
36`���n. (mk_nt n).dom = n.dom`,
37srw_tac [][mk_nt_def]);
38
39val mk_nt_cod = Q.store_thm(
40"mk_nt_cod",
41`���n. (mk_nt n).cod = n.cod`,
42srw_tac [][mk_nt_def]);
43
44val _ = export_rewrites ["mk_nt_dom","mk_nt_cod"];
45
46val is_nat_trans_mk_nt = Q.store_thm(
47"is_nat_trans_mk_nt",
48`���n. is_nat_trans (mk_nt n) ��� nat_trans_axioms n`,
49gen_tac >> EQ_TAC >- (
50  srw_tac [][is_nat_trans_def,nat_trans_axioms_def,mk_nt_def,restrict_def] >>
51  `f :- x ��� y -:n.dom.dom` by metis_tac [] >>
52  res_tac >>
53  imp_res_tac is_functor_is_category >>
54  imp_res_tac maps_to_obj >>
55  fsrw_tac [][]) >>
56srw_tac [][mk_nt_def,is_nat_trans_def,extensional_nat_trans_def] >>
57fsrw_tac [][nat_trans_axioms_def] >>
58srw_tac [][restrict_def] >>
59imp_res_tac is_functor_is_category >>
60imp_res_tac maps_to_obj);
61val _ = export_rewrites["is_nat_trans_mk_nt"];
62
63val naturality = Q.store_thm(
64"naturality",
65`���n f g c k x y. is_nat_trans n ���
66  (n :- f ��� g) ��� (c = ntcod n) ��� k :- x ��� y -:(ntdom n) ���
67  (n@+y o f##k -:c = (g##k) o n@+x -:c)`,
68srw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
69first_assum match_mp_tac >> first_assum ACCEPT_TAC);
70
71val nt_at_maps_to = Q.store_thm(
72"nt_at_maps_to",
73`���n f g x a b c. is_nat_trans n ��� (n :- f ��� g) ��� x ��� f.dom.obj ��� (a = f@@x) ��� (b = g@@x) ��� (c = g.cod) ���
74   n@+x :- a ��� b -:c`,
75srw_tac [][is_nat_trans_def,nat_trans_axioms_def] >> res_tac);
76
77val nt_eq_thm = Q.store_thm(
78"nt_eq_thm",
79`���n1 n2. is_nat_trans n1 ��� is_nat_trans n2 ���
80    (n1.dom = n2.dom) ��� (n1.cod = n2.cod) ���
81    (���x. x ��� (ntdom n1).obj ��� (n1@+x = n2@+x)) ���
82      (n1 = n2)`,
83srw_tac [][morphism_component_equality,is_nat_trans_def,
84     extensional_nat_trans_def,extensional_def,FUN_EQ_THM] >>
85metis_tac []);
86
87val id_nt_def = Define`
88  id_nt f = mk_nt <| dom := f; cod := f; map := ��x. id (f@@x) -:f.cod |>`;
89
90val id_nt_dom = Q.store_thm(
91"id_nt_dom",
92`���f. (id_nt f).dom = f`,
93srw_tac [][id_nt_def]);
94
95val id_nt_cod = Q.store_thm(
96"id_nt_cod",
97`���f. (id_nt f).cod = f`,
98srw_tac [][id_nt_def]);
99
100val id_nt_at = Q.store_thm(
101"id_nt_at",
102`���f x. x ��� f.dom.obj ��� ((id_nt f)@+x = id (f@@x) -:f.cod)`,
103srw_tac [][id_nt_def,mk_nt_def,restrict_def]);
104
105val _ = export_rewrites ["id_nt_dom","id_nt_cod","id_nt_at"];
106
107val is_nat_trans_id_nt = Q.store_thm(
108"is_nat_trans_id_nt",
109`���f. is_functor f ��� is_nat_trans (id_nt f)`,
110srw_tac [][id_nt_def] >>
111srw_tac [][nat_trans_axioms_def] >- (
112  metis_tac [maps_to_morf,id_mor,morf_id,maps_to_def,
113             is_functor_is_category,id_dom_cod] ) >>
114imp_res_tac is_functor_is_category >>
115qmatch_assum_rename_tac `g :- x ��� y -:f.dom` >>
116`id (f@@y) -:f.cod = f##(id y -:f.dom)` by (
117  match_mp_tac (GSYM morf_id) >> srw_tac [][] >>
118  imp_res_tac maps_to_obj ) >>
119`id (f@@x) -:f.cod = f##(id x -:f.dom)` by (
120  match_mp_tac (GSYM morf_id) >> srw_tac [][] >>
121  imp_res_tac maps_to_obj ) >>
122srw_tac [][] >>
123qspecl_then [`f`,`f.dom`,`f.cod`,`g`,`id y -:f.dom`] mp_tac (GSYM morf_comp) >>
124`g ���> (id y -:f.dom) -:f.dom` by (
125  match_mp_tac maps_to_composable >>
126  metis_tac [id_maps_to,maps_to_obj] ) >>
127srw_tac [][] >>
128qspecl_then [`f`,`f.dom`,`f.cod`,`id x -:f.dom`,`g`] mp_tac (GSYM morf_comp) >>
129`id x -:f.dom ���> g -:f.dom` by (
130  match_mp_tac maps_to_composable >>
131  metis_tac [id_maps_to,maps_to_obj] ) >>
132srw_tac [][] >>
133fsrw_tac [][composable_in_def] >>
134metis_tac [id_comp1,id_comp2,id_dom_cod,maps_to_obj]);
135val _ = export_rewrites["is_nat_trans_id_nt"];
136
137val composable_nts_def = Define`
138  composable_nts f g = is_nat_trans f ��� is_nat_trans g ���
139    (ntdom f = ntdom g) ��� (ntcod f = ntcod g) ��� f ���> g`;
140
141val _ = add_infix("\226\137\136\226\137\136>",450,NONASSOC);
142val _ = overload_on("������>",``composable_nts``);
143
144val nt_comp_def = Define`
145  nt_comp n m = mk_nt (compose (��n m x. m@+x o n@+x -:(ntcod n)) m n)`;
146
147val _ = overload_on("\226\151\142",``nt_comp``);
148
149val nt_comp_at = Q.store_thm(
150"nt_comp_at",
151`���f g x. (f ���> g) ��� x ��� (ntdom f).obj ��� ((g ��� f) @+ x = g@+x o f@+x -:(ntcod f))`,
152srw_tac [][nt_comp_def,mk_nt_def,restrict_def]);
153val _ = export_rewrites["nt_comp_at"];
154
155val is_nat_trans_is_functor = Q.store_thm(
156"is_nat_trans_is_functor",
157`���n. is_nat_trans n ��� is_functor n.dom ��� is_functor n.cod`,
158srw_tac [][is_nat_trans_def,nat_trans_axioms_def]);
159
160val is_nat_trans_is_category = Q.store_thm(
161"is_nat_trans_is_category",
162`���n. is_nat_trans n ��� is_category (ntdom n) ��� is_category (ntcod n)`,
163metis_tac [is_nat_trans_is_functor,is_functor_is_category]);
164
165val is_nat_trans_nt_comp = Q.store_thm(
166"is_nat_trans_nt_comp",
167`���n m. n ������> m ��� is_nat_trans (m ��� n)`,
168srw_tac [][nt_comp_def] >>
169srw_tac [][nat_trans_axioms_def]
170>- fsrw_tac [][composable_nts_def,is_nat_trans_is_functor]
171>- fsrw_tac [][composable_nts_def,is_nat_trans_is_functor]
172>- (fsrw_tac [][composable_nts_def,is_nat_trans_def] >>
173    metis_tac [nat_trans_axioms_def])
174>- (fsrw_tac [][composable_nts_def,is_nat_trans_def] >>
175    metis_tac [nat_trans_axioms_def])
176>- (
177  fsrw_tac [][composable_nts_def,compose_def,restrict_def] >>
178  pop_assum mp_tac >> srw_tac [][] >>
179  match_mp_tac maps_to_comp >>
180  qexists_tac `n.cod@@x` >>
181  imp_res_tac is_nat_trans_is_category >>
182  metis_tac [is_nat_trans_def,nat_trans_axioms_def]) >>
183imp_res_tac composable_nts_def >>
184fsrw_tac [][compose_def,restrict_def] >>
185qabbrev_tac `E = n.dom` >> qabbrev_tac `G = n.cod` >> qabbrev_tac `H = m.cod` >>
186qabbrev_tac `C1 = E.dom` >> qabbrev_tac `C2 = E.cod` >>
187`(G.dom = C1) ��� (G.cod = C2) ��� (H.dom = C1) ��� (H.cod = C2) ���
188 (n@+x :- E@@x ��� G@@x -:C2) ��� (n@+y :- E@@y ��� G@@y -:C2) ���
189 (m@+x :- G@@x ��� H@@x -:C2) ��� (m@+y :- G@@y ��� H@@y -:C2) ���
190 (E##f :- E@@x ��� E@@y -:C2) ��� (m.dom = n.cod) ���
191 (G##f :- G@@x ��� G@@y -:C2) ���
192 (H##f :- H@@x ��� H@@y -:C2)` by (
193  fsrw_tac [][composable_nts_def,is_nat_trans_def,nat_trans_axioms_def,
194              is_functor_def,functor_axioms_def] >>
195  metis_tac [nt_at_maps_to,maps_to_obj] ) >>
196fsrw_tac [][] >>
197imp_res_tac is_nat_trans_is_category >>
198imp_res_tac is_nat_trans_def >>
199metis_tac [comp_assoc,maps_to_composable,nat_trans_axioms_def]);
200val _ = export_rewrites["is_nat_trans_nt_comp"];
201
202val id_nt_comp = Q.store_thm(
203"id_nt_comp",
204`���f. is_nat_trans f ���
205  (f ��� (id_nt f.dom) = f) ���
206  ((id_nt f.cod) ��� f = f)`,
207srw_tac [][id_nt_def,nt_comp_def,mk_nt_def,morphism_component_equality] >- (
208  srw_tac [][restrict_def,FUN_EQ_THM] >> srw_tac [][] >- (
209    `f.dom.cod = f.cod.cod` by (
210      fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
211    srw_tac [][] >>
212    match_mp_tac id_comp1 >>
213    fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def,
214                maps_to_in_def,is_functor_is_category] ) >>
215  fsrw_tac [][is_nat_trans_def,extensional_nat_trans_def,extensional_def] ) >>
216srw_tac [][restrict_def,FUN_EQ_THM] >> srw_tac [][] >- (
217  match_mp_tac id_comp2 >>
218  fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def,
219              maps_to_in_def,is_functor_is_category] )
220>- metis_tac [is_nat_trans_def,nat_trans_axioms_def] >>
221fsrw_tac [][is_nat_trans_def,extensional_nat_trans_def,extensional_def]);
222val _ = export_rewrites["id_nt_comp"];
223
224val composable_nts_composable = Q.store_thm(
225"composable_nts_composable",
226`���n m x. n ������> m ��� x ��� (ntdom n).obj ��� n@+x ���> m@+x -:(ntcod n)`,
227srw_tac [][] >>
228match_mp_tac maps_to_composable >>
229map_every qexists_tac [`n.dom @@ x`,`n.cod @@ x`,`m.cod @@ x`] >>
230imp_res_tac composable_nts_def >>
231imp_res_tac is_nat_trans_def >>
232imp_res_tac nat_trans_axioms_def >>
233fsrw_tac [][]);
234
235val nt_comp_assoc = Q.store_thm(
236"nt_comp_assoc",
237`���f g h. f ������> g ��� g ������> h ��� ((h ��� g) ��� f = h ��� g ��� f)`,
238srw_tac [][] >>
239imp_res_tac composable_nts_def >>
240fsrw_tac [][nt_comp_def,mk_nt_def,restrict_def,FUN_EQ_THM,compose_def] >>
241srw_tac [][] >>
242match_mp_tac comp_assoc >>
243fsrw_tac [][is_nat_trans_is_category] >>
244metis_tac [composable_nts_composable]);
245
246val nt_comp_dom_cod = Q.store_thm(
247"nt_comp_dom_cod",
248`���f g. (f ���> g) ��� (((g ��� f).dom = f.dom) ��� ((g ��� f).cod = g.cod))`,
249srw_tac [][nt_comp_def]);
250val _ = export_rewrites["nt_comp_dom_cod"];
251
252val pre_functor_cat_def = Define`
253  pre_functor_cat c1 c2 =
254    <| obj := {f | is_functor f ��� f :- c1 ��� c2};
255       mor := {n | is_nat_trans n ��� (ntdom n = c1) ��� (ntcod n = c2)};
256       id_map := ��x. (id_nt x).map;
257       comp := (��n m. (nt_comp m n).map) |>`;
258
259val pre_functor_cat_obj = Q.store_thm(
260"pre_functor_cat_obj",
261`���c1 c2. (pre_functor_cat c1 c2).obj = {f | is_functor f ��� f :- c1 ��� c2}`,
262srw_tac [][pre_functor_cat_def]);
263
264val pre_functor_cat_mor = Q.store_thm(
265"pre_functor_cat_mor",
266`���c1 c2. (pre_functor_cat c1 c2).mor = {n | is_nat_trans n ��� (ntdom n = c1) ��� (ntcod n = c2)}`,
267srw_tac [][pre_functor_cat_def]);
268
269val pre_functor_cat_id = Q.store_thm(
270"pre_functor_cat_id",
271`���c1 c2 x. is_functor x ��� (x :- c1 ��� c2) ��� (id x -:(pre_functor_cat c1 c2) = id_nt x)`,
272srw_tac [][pre_functor_cat_def,id_in_def,morphism_component_equality,restrict_def]);
273
274val pre_functor_cat_comp = Q.store_thm(
275"pre_functor_cat_comp",
276`���c1 c2 n m. (pre_functor_cat c1 c2).comp n m = (nt_comp m n).map`,
277srw_tac [][pre_functor_cat_def]);
278
279val pre_functor_cat_composable_in = Q.store_thm(
280"pre_functor_cat_composable_in",
281`���c1 c2 f g. f ���> g -:(pre_functor_cat c1 c2) = f ������> g ��� (ntdom g = c1) ��� (ntcod g = c2)`,
282srw_tac [][composable_nts_def,composable_in_def,pre_functor_cat_mor] >> metis_tac []);
283
284val pre_functor_cat_compose_in = Q.store_thm(
285"pre_functor_cat_compose_in",
286`���c1 c2 f g. g ���> f -:(pre_functor_cat c1 c2) ��� (f o g -:(pre_functor_cat c1 c2) = nt_comp f g)`,
287srw_tac [][compose_in_thm,morphism_component_equality,nt_comp_def] >>
288srw_tac [][compose_def,restrict_def,pre_functor_cat_comp,nt_comp_def] >>
289fsrw_tac [][composable_in_def]);
290
291val pre_functor_cat_maps_to = Q.store_thm(
292"pre_functor_cat_maps_to",
293`���c1 c2 f g x y. f :- x ��� y -:(pre_functor_cat c1 c2) = (f :- x ��� y)
294  ��� is_nat_trans f ��� (ntdom f = c1) ��� (ntcod f = c2)`,
295srw_tac [][maps_to_in_def,pre_functor_cat_mor] >> metis_tac []);
296
297val _ = export_rewrites
298["pre_functor_cat_obj","pre_functor_cat_mor",
299 "pre_functor_cat_id","pre_functor_cat_comp","pre_functor_cat_maps_to",
300 "pre_functor_cat_compose_in","pre_functor_cat_composable_in"];
301
302val _ = add_rule {
303  term_name = "functor_cat",
304  fixity = Closefix,
305  pp_elements = [TOK"[",TM,TOK"\226\134\146",TM,TOK"]"],
306  paren_style = OnlyIfNecessary,
307  block_style = (AroundEachPhrase, (PP.INCONSISTENT,0))};
308
309val functor_cat_def = Define`
310  [c1���c2] = mk_cat (pre_functor_cat c1 c2)`;
311
312val is_category_functor_cat = Q.store_thm(
313"is_category_functor_cat",
314`���c1 c2. is_category c1 ��� is_category c2 ��� is_category [c1���c2]`,
315srw_tac [][functor_cat_def] >>
316fsrw_tac [][category_axioms_def] >>
317conj_tac >- srw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
318conj_tac >- PROVE_TAC [is_nat_trans_def,nat_trans_axioms_def] >>
319conj_tac >- (
320  srw_tac [][] >>
321  imp_res_tac is_nat_trans_def >>
322  imp_res_tac nat_trans_axioms_def >>
323  qmatch_abbrev_tac `f o g -:c = f` >>
324  `g ���> f -:c` by (
325    srw_tac [][composable_nts_def,Abbr`c`,Abbr`g`] ) >>
326  srw_tac [][Abbr`c`,Abbr`g`]) >>
327conj_tac >- (
328  srw_tac [][] >>
329  imp_res_tac is_nat_trans_def >>
330  imp_res_tac nat_trans_axioms_def >>
331  qmatch_abbrev_tac `g o f -:c = f` >>
332  `f ���> g -:c` by (
333    srw_tac [][composable_nts_def,Abbr`c`,Abbr`g`] ) >>
334  srw_tac [][Abbr`c`,Abbr`g`]) >>
335conj_tac >- (
336  srw_tac [][] >>
337  qmatch_abbrev_tac `X = h o g ��� f -:c` >>
338  qunabbrev_tac `X` >>
339  `(g ��� f ���> h -:c) ��� (f ���> (h ��� g) -:c)` by (
340    imp_res_tac composable_nts_def >>
341    fsrw_tac [][Abbr`c`,composable_nts_def] ) >>
342  srw_tac [][nt_comp_assoc,Abbr`c`] ) >>
343rpt gen_tac >> rpt DISCH_TAC >>
344`f ���> g -:pre_functor_cat c1 c2` by (
345  srw_tac [][composable_nts_def] ) >>
346srw_tac [][composable_nts_def]);
347
348val functor_cat_obj = Q.store_thm(
349"functor_cat_obj",
350`���c1 c2. [c1���c2].obj = {f | is_functor f ��� f :- c1 ��� c2}`,
351srw_tac [][functor_cat_def]);
352
353val functor_cat_mor = Q.store_thm(
354"functor_cat_mor",
355`���c1 c2. [c1���c2].mor = {n | is_nat_trans n ��� (ntdom n = c1) ��� (ntcod n = c2)}`,
356srw_tac [][functor_cat_def]);
357
358val functor_cat_id = Q.store_thm(
359"functor_cat_id",
360`���c1 c2 x. x ��� [c1���c2].obj ��� (id x -:[c1���c2] = id_nt x)`,
361srw_tac [][functor_cat_def]);
362
363val functor_cat_comp = Q.store_thm(
364"functor_cat_comp",
365`���c1 c2 n m. n ������> m ��� (ntdom m = c1) ��� (ntcod m = c2) ��� ([c1���c2].comp n m = (nt_comp m n).map)`,
366srw_tac [][functor_cat_def,mk_cat_def,restrict_def]);
367
368val functor_cat_compose_in = Q.store_thm(
369"functor_cat_compose_in",
370`���c1 c2 n m. n ������> m ��� (ntdom m = c1) ��� (ntcod m = c2) ��� (m o n -:[c1���c2] = nt_comp m n)`,
371srw_tac [][functor_cat_def,composable_nts_def]);
372
373val functor_cat_composable_in = Q.store_thm(
374"functor_cat_composable_in",
375`���c1 c2 f g. f ���> g -:[c1���c2] = f ������> g ��� (ntdom g = c1) ��� (ntcod g = c2)`,
376srw_tac [][functor_cat_def]);
377
378val functor_cat_maps_to = Q.store_thm(
379"functor_cat_maps_to",
380`���c1 c2 f g x y. f :- x ��� y -:[c1���c2] = (f :- x ��� y)
381  ��� is_nat_trans f ��� (ntdom f = c1) ��� (ntcod f = c2)`,
382srw_tac [][functor_cat_def]);
383
384val functor_cat_mor_is_nat_trans = Q.store_thm(
385"functor_cat_mor_is_nat_trans",
386`���c1 c2 f. f ��� [c1���c2].mor ��� is_nat_trans f`,
387srw_tac [][functor_cat_def]);
388
389val functor_cat_dist = Q.store_thm(
390"functor_cat_dist",
391`���c1 c2 f g x. f ���> g -:[c1���c2] ��� x ��� c1.obj ���
392   ((g o f -:[c1���c2])@+x = (g@+x) o (f@+x) -:c2)`,
393srw_tac [][] >>
394imp_res_tac functor_cat_composable_in >>
395srw_tac [][functor_cat_compose_in] >>
396imp_res_tac composable_nts_def >>
397srw_tac [][nt_comp_at]);
398
399val _ = export_rewrites[
400"is_category_functor_cat","functor_cat_obj","functor_cat_mor",
401"functor_cat_id","functor_cat_comp","functor_cat_compose_in",
402"functor_cat_composable_in","functor_cat_maps_to","functor_cat_dist",
403"functor_cat_mor_is_nat_trans"];
404
405val functor_cat_iso_pair = Q.store_thm(
406"functor_cat_iso_pair",
407`���n1 n2 c1 c2. n1 <���> n2 -:[c1���c2] = n1 ���> n2 -:[c1���c2] ��� n2 ���> n1 -:[c1���c2] ��� (���x. x ��� c1.obj ��� n1@+x <���> n2@+x -:c2)`,
408srw_tac [][iso_pair_def] >> EQ_TAC >> strip_tac >> fsrw_tac [][] >- (
409  conj_asm1_tac >- (
410    fsrw_tac [][composable_nts_def] >>
411    `(n2 o n1 -:[c1���c2]).cod = (id n1.dom -:[c1���c2]).cod` by srw_tac [][] >>
412    qpat_x_assum `X = id n1.dom -:C` (K ALL_TAC) >>
413    pop_assum mp_tac >> fsrw_tac [][composable_nts_def] >>
414    `n1.dom ��� [c1���c2].obj` by (
415      fsrw_tac [][composable_nts_def,is_nat_trans_is_functor] >>
416      fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
417    srw_tac [][] ) >>
418  qx_gen_tac `x` >> strip_tac >>
419  conj_tac >- (
420    match_mp_tac maps_to_composable >>
421    map_every qexists_tac [`n1.dom@@x`,`n1.cod@@x`,`n2.cod@@x`] >>
422    conj_tac >- (
423      match_mp_tac nt_at_maps_to >>
424      map_every qexists_tac [`n1.dom`,`n1.cod`] >>
425      fsrw_tac [][composable_nts_def] ) >>
426    match_mp_tac nt_at_maps_to >>
427    map_every qexists_tac [`n2.dom`,`n2.cod`] >>
428    fsrw_tac [][composable_nts_def] ) >>
429  reverse conj_tac >- (
430    `(n2 o n1 -:[c1���c2]) @+ x = (id n1.dom -:[c1���c2]) @+ x` by metis_tac [] >>
431    qpat_x_assum `n2 o n1 -:[c1���c2] = X` (K ALL_TAC) >>
432    pop_assum mp_tac >> fsrw_tac [][] >> strip_tac >>
433    `n1.dom ��� [c1���c2].obj` by (
434      fsrw_tac [][composable_nts_def,is_nat_trans_is_functor] >>
435      fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
436    fsrw_tac [][] >>
437    `n1 @+ x :- n1.dom@@x ��� n1.cod@@x -:c2` by (
438      match_mp_tac nt_at_maps_to >>
439      map_every qexists_tac [`n1.dom`,`n1.cod`] >>
440      fsrw_tac [][composable_nts_def] ) >>
441    fsrw_tac [][maps_to_in_def] ) >>
442  `(n1 o n2 -:[c1���c2]) @+ x = (id n2.dom -:[c1���c2]) @+ x` by metis_tac [] >>
443  qpat_x_assum `n1 o n2 -:[c1���c2] = X` (K ALL_TAC) >>
444  pop_assum mp_tac >> fsrw_tac [][] >> strip_tac >>
445  `n2.dom ��� [c1���c2].obj` by(
446    fsrw_tac [][composable_nts_def,is_nat_trans_is_functor] >>
447    fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
448  fsrw_tac [][] >>
449  `n2 @+ x :- n2.dom@@x ��� n2.cod@@x -:c2` by (
450    match_mp_tac nt_at_maps_to >>
451    map_every qexists_tac [`n2.dom`,`n2.cod`] >>
452    fsrw_tac [][composable_nts_def] ) >>
453  fsrw_tac [][maps_to_in_def] ) >>
454`n1.dom ��� [c1���c2].obj ��� n2.dom ��� [c1���c2].obj` by (
455  fsrw_tac [][composable_nts_def,is_nat_trans_is_functor] >>
456  fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
457fsrw_tac [][] >>
458srw_tac [][] >>
459match_mp_tac nt_eq_thm >>
460srw_tac [][] >>
461fsrw_tac [][composable_nts_def] >>
462pop_assum mp_tac >> srw_tac [][] >>
463`n1 @+ x :- n1.dom@@x ��� n1.cod@@x -:n1.dom.cod` by (
464  match_mp_tac nt_at_maps_to >>
465  map_every qexists_tac [`n1.dom`,`n1.cod`] >>
466  fsrw_tac [][] ) >>
467`n2 @+ x :- n2.dom@@x ��� n2.cod@@x -:n2.dom.cod` by (
468  match_mp_tac nt_at_maps_to >>
469  map_every qexists_tac [`n2.dom`,`n2.cod`] >>
470  fsrw_tac [][] ) >>
471fsrw_tac [][maps_to_in_def]);
472
473(*
474val functor_cat_iso_objs = Q.store_thm(
475"functor_cat_iso_objs",
476`���c1 c2 f g. f ��� g -:[c1���c2] = (���h. h ��� c1.mor ��� f##h <���> g##h -:c2)`,
477srw_tac [][iso_objs_def,iso_pair_between_objs_def,functor_cat_iso_pair] >>
478EQ_TAC >> strip_tac >- (
479  qx_gen_tac `k` >>
480  strip_tac >>
481  simp_tac (srw_ss()) [iso_pair_def] >>
482  conj_tac >- (
483    match_mp_tac maps_to_composable >>
484    map_every qexists_tac [`f@@k.dom`,`f@@k.cod`,`g@@k.cod`] >>
485    conj_tac >- (
486      match_mp_tac morf_maps_to >>
487      map_every qexists_tac [`c1`,`k.dom`,`k.cod`] >>
488      fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
489      metis_tac [] ) >>
490    match_mp_tac morf_maps_to >>
491    map_every qexists_tac [`c1`,`k.dom`,`k.cod`] >>
492    fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
493    conj_tac >- metis_tac [] >>
494    conj_tac >- metis_tac [] >>
495    metis_tac []
496*)
497
498val pre_functor_nt_def = Define`
499  pre_functor_nt f n = <|
500    dom := f ��� n.dom;
501    cod := f ��� n.cod;
502    map := ��x. f##(n@+x) |>`;
503
504val pre_functor_nt_components = Q.store_thm(
505"pre_functor_nt_components",
506`���f n. ((pre_functor_nt f n).dom = f ��� n.dom) ���
507       ((pre_functor_nt f n).cod = f ��� n.cod) ���
508       (���x. (pre_functor_nt f n)@+x = f##(n@+x))`,
509srw_tac [][pre_functor_nt_def]);
510val _ = export_rewrites["pre_functor_nt_components"];
511
512val functor_nt_def = Define`
513  functor_nt f n = mk_nt (pre_functor_nt f n)`;
514
515val is_nat_trans_functor_nt = Q.store_thm(
516"is_nat_trans_functor_nt",
517`���f n. is_functor f ��� is_nat_trans n ��� (f.dom = ntcod n) ��� is_nat_trans (functor_nt f n)`,
518srw_tac [][functor_nt_def] >>
519fsrw_tac [][nat_trans_axioms_def] >>
520`is_functor n.dom ��� is_functor n.cod` by srw_tac [][is_nat_trans_is_functor] >>
521`(n.dom.dom = n.cod.dom) ��� (n.dom.cod = n.cod.cod)` by
522  fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
523fsrw_tac [][] >>
524conj_asm1_tac >- (
525  qx_gen_tac `x` >> strip_tac >>
526  metis_tac [morf_maps_to,nt_at_maps_to,maps_to_def] ) >>
527map_every qx_gen_tac [`h`,`x`,`y`] >> strip_tac >>
528`(f ��� n.dom)##h = f##(n.dom##h)` by (
529  match_mp_tac functor_comp_morf >>
530  fsrw_tac [][maps_to_in_def] ) >>
531`(f ��� n.cod)##h = f##(n.cod##h)` by (
532  match_mp_tac functor_comp_morf >>
533  fsrw_tac [][maps_to_in_def] ) >>
534fsrw_tac [][] >>
535`(f##(n@+y)) o (f##(n.dom##h)) -:f.cod = f##((n@+y) o (n.dom##h) -:f.dom)` by (
536  match_mp_tac (GSYM morf_comp) >> srw_tac [][] >>
537  match_mp_tac maps_to_composable >>
538  metis_tac [morf_maps_to,nt_at_maps_to,maps_to_def,maps_to_in_def,is_functor_is_category,maps_to_obj] ) >>
539`(f##(n.cod##h)) o f##(n@+x) -:f.cod = f##((n.cod##h) o n@+x -:f.dom)` by (
540  match_mp_tac (GSYM morf_comp) >> srw_tac [][] >>
541  match_mp_tac maps_to_composable >>
542  metis_tac [morf_maps_to,nt_at_maps_to,maps_to_def,maps_to_in_def,is_functor_is_category,maps_to_obj] ) >>
543fsrw_tac [][] >>
544AP_TERM_TAC >>
545match_mp_tac naturality >>
546srw_tac [][]);
547val _ = export_rewrites["is_nat_trans_functor_nt"];
548
549val functor_nt_dom_cod = Q.store_thm(
550"functor_nt_dom_cod",
551`���f n. ((functor_nt f n).dom = f ��� n.dom) ���
552       ((functor_nt f n).cod = f ��� n.cod)`,
553srw_tac [][functor_nt_def]);
554val _ = export_rewrites["functor_nt_dom_cod"];
555
556val functor_nt_at = Q.store_thm(
557"functor_nt_at",
558`���f n x. is_functor f ��� (f.dom = n.dom.cod) ��� x ��� (ntdom n).obj
559  ��� ((functor_nt f n)@+x = f##(n@+x))`,
560srw_tac [][functor_nt_def] >>
561srw_tac [][mk_nt_def,restrict_def]);
562val _ = export_rewrites["functor_nt_at"];
563
564val functor_nt_id_nt = Q.store_thm(
565"functor_nt_id_nt",
566`���f g. is_functor f ��� is_functor g ��� (g ���> f) ��� (functor_nt f (id_nt g) = id_nt (f ��� g))`,
567rpt strip_tac >>
568match_mp_tac nt_eq_thm >>
569fsrw_tac [][] >>
570qx_gen_tac `x` >> strip_tac >>
571match_mp_tac morf_id >>
572srw_tac [][] >>
573metis_tac [objf_in_obj]);
574val _ = export_rewrites["functor_nt_id_nt"];
575
576val functor_nt_nt_comp = Q.store_thm(
577"functor_nt_nt_comp",
578`���f n1 n2. is_functor f ��� composable_nts n1 n2 ��� (f.dom = ntcod n1) ���
579  (functor_nt f (n2 ��� n1) = functor_nt f n2 ��� functor_nt f n1)`,
580srw_tac [][] >>
581match_mp_tac nt_eq_thm >>
582fsrw_tac [][composable_nts_def] >>
583`n1.dom ���> f` by (
584  fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
585fsrw_tac [][] >>
586conj_tac >- (
587  match_mp_tac is_nat_trans_nt_comp >>
588  fsrw_tac [][composable_nts_def]  ) >>
589qx_gen_tac `x` >> strip_tac >>
590match_mp_tac morf_comp >>
591srw_tac [][] >>
592match_mp_tac maps_to_composable >>
593metis_tac [nt_at_maps_to,maps_to_def]);
594val _ = export_rewrites["functor_nt_nt_comp"];
595
596val functor_nt_id_functor = Q.store_thm(
597"functor_nt_id_functor",
598`���c n. is_nat_trans n ��� (c = ntcod n) ��� (functor_nt (id_functor c) n = n)`,
599srw_tac [][] >>
600match_mp_tac nt_eq_thm >>
601imp_res_tac is_nat_trans_is_category >>
602imp_res_tac is_nat_trans_is_functor >>
603`n.dom.cod = n.cod.cod` by fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
604fsrw_tac [][] >>
605srw_tac [][] >>
606match_mp_tac id_functor_morf >>
607metis_tac [nt_at_maps_to,maps_to_in_def,maps_to_def]);
608val _ = export_rewrites["functor_nt_id_functor"];
609
610val functor_nt_functor_comp = Q.store_thm(
611"functor_nt_functor_comp",
612`���f1 f2 n. is_nat_trans n ��� is_functor f1 ��� is_functor f2 ��� (f1 ���> f2) ��� (f1.dom = ntcod n) ���
613  (functor_nt (f2 ��� f1) n = functor_nt f2 (functor_nt f1 n))`,
614srw_tac [][] >>
615match_mp_tac nt_eq_thm >>
616imp_res_tac is_nat_trans_is_functor >>
617`n.dom.cod = n.cod.cod` by fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
618fsrw_tac [][functor_comp_assoc] >>
619qx_gen_tac `x` >> strip_tac >>
620match_mp_tac functor_comp_morf >>
621srw_tac [][] >>
622metis_tac [nt_at_maps_to,maps_to_in_def,maps_to_def]);
623
624(* would be a morphism in cat_cat if we had a proper cat_cat *)
625(* or could use the fact that [c���d] is an exponential object *)
626val pre_postcomp_functor_def = Define`
627  pre_postcomp_functor b f = <|
628    dom := [b���f.dom];
629    cod := [b���f.cod];
630    map := functor_nt f |>`;
631
632val pre_postcomp_functor_components = Q.store_thm(
633"pre_postcomp_functor_components",
634`���b f. ((pre_postcomp_functor b f).dom = [b���f.dom]) ���
635       ((pre_postcomp_functor b f).cod = [b���f.cod]) ���
636       (���g. (pre_postcomp_functor b f)##g = functor_nt f g)`,
637srw_tac [][pre_postcomp_functor_def,morf_def]);
638val _ = export_rewrites["pre_postcomp_functor_components"];
639
640val pre_postcomp_functor_objf = Q.store_thm(
641"pre_postcomp_functor_objf",
642`���b f g. is_functor f ��� g ��� [b���f.dom].obj ��� ((pre_postcomp_functor b f)@@g = f ��� g)`,
643srw_tac [][objf_def] >>
644SELECT_ELIM_TAC >>
645conj_tac >- (
646  qexists_tac `f���g` >> srw_tac [][] ) >>
647srw_tac [][] >>
648Q.ISPECL_THEN [`[x.dom���x.cod]`,`x`,`f���g`] mp_tac id_inj >>
649fsrw_tac [][is_functor_is_category]);
650val _ = export_rewrites["pre_postcomp_functor_objf"];
651
652val postcomp_functor_def = Define`
653  postcomp_functor b f = mk_functor (pre_postcomp_functor b f)`;
654
655val is_functor_postcomp_functor = Q.store_thm(
656"is_functor_postcomp_functor",
657`���b f. is_category b ��� is_functor f ��� is_functor (postcomp_functor b f)`,
658srw_tac [][postcomp_functor_def] >>
659imp_res_tac is_functor_is_category >>
660fsrw_tac [][functor_axioms_def] >>
661conj_tac >- (
662  qx_gen_tac `n` >> strip_tac >>
663  `n.dom ���> f` by (
664    fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
665  fsrw_tac [][] ) >>
666conj_tac >- (
667  qx_gen_tac `g` >> strip_tac >>
668  qexists_tac `f���g` >>
669  fsrw_tac [][] ) >>
670srw_tac [][composable_nts_def] >>
671match_mp_tac (GSYM functor_cat_compose_in) >>
672fsrw_tac [][composable_nts_def] >>
673fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def]);
674val _ = export_rewrites["is_functor_postcomp_functor"];
675
676val postcomp_functor_dom_cod = Q.store_thm(
677"postcomp_functor_dom_cod",
678`���b f. ((postcomp_functor b f).dom = [b���f.dom]) ���
679       ((postcomp_functor b f).cod = [b���f.cod])`,
680srw_tac [][postcomp_functor_def]);
681val _ = export_rewrites["postcomp_functor_dom_cod"];
682
683val postcomp_functor_morf = Q.store_thm(
684"postcomp_functor_morf",
685`���b f n. is_nat_trans n ��� n ��� [b���f.dom].mor ��� ((postcomp_functor b f)##n = functor_nt f n)`,
686srw_tac [][postcomp_functor_def]);
687
688val postcomp_functor_objf = Q.store_thm(
689"postcomp_functor_objf",
690`���b f g. is_category b ��� is_functor f ��� g ��� [b���f.dom].obj ��� ((postcomp_functor b f)@@g = f ��� g)`,
691srw_tac [][is_functor_is_category,postcomp_functor_def]);
692
693val _ = export_rewrites["postcomp_functor_morf","postcomp_functor_objf"];
694
695val cat_iso_functor_cats = Q.store_thm(
696"cat_iso_functor_cats",
697`���f b. is_category b ��� cat_iso f ��� cat_iso (postcomp_functor b f)`,
698srw_tac [][cat_iso_def] >>
699imp_res_tac cat_iso_pair_sym >>
700qexists_tac `postcomp_functor b g` >>
701fsrw_tac [][cat_iso_pair_def] >>
702imp_res_tac is_functor_is_category >>
703conj_tac >> match_mp_tac functor_eq_thm >>
704fsrw_tac [][] >>
705qx_gen_tac `n` >> strip_tac >>
706qmatch_rename_tac `postcomp_functor b j##(functor_nt k n) = n` >>
707`n.dom ���> k` by (
708  fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
709srw_tac [][GSYM functor_nt_functor_comp]);
710
711val iso_cats_functor_cats = Q.store_thm(
712"iso_cats_functor_cats",
713`���b c1 c2. is_category b ��� iso_cats c1 c2 ��� iso_cats [b���c1] [b���c2]`,
714srw_tac [][iso_cats_def,iso_pair_between_cats_def] >>
715metis_tac [cat_iso_def,cat_iso_functor_cats,postcomp_functor_dom_cod]);
716
717val embedding_functor_cats = Q.store_thm(
718"embedding_functor_cats",
719`���g c. is_category c ��� is_functor g ��� embedding g ��� embedding (postcomp_functor c g)`,
720map_every qx_gen_tac [`g`,`c`] >>
721fsrw_tac [][embedding_def] >>
722strip_tac >>
723conj_tac >- (
724  fsrw_tac [][full_def,faithful_def] >>
725  map_every qx_gen_tac [`h`,`a`,`b`] >>
726  strip_tac >>
727  qpat_x_assum `h.dom = postcomp_functor c g@@a` mp_tac >>
728  qpat_x_assum `h.cod = postcomp_functor c g@@b` mp_tac >>
729  fsrw_tac [][] >> ntac 2 strip_tac >>
730  fsrw_tac [][GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM] >>
731  qexists_tac `mk_nt <| dom := a; cod := b; map := ��x. f (h@+x) (a@@x) (b@@x) |>` >>
732  fsrw_tac [][] >>
733  conj_asm1_tac >- (
734    fsrw_tac [][nat_trans_axioms_def] >>
735    conj_asm1_tac >- (
736      qx_gen_tac `x` >> strip_tac >>
737      `a@@x ��� g.dom.obj` by metis_tac [objf_in_obj] >>
738      `b@@x ��� g.dom.obj` by metis_tac [objf_in_obj] >>
739      `(h@+x) :- (g@@(a@@x)) ��� (g@@(b@@x)) -:g.cod` by (
740        match_mp_tac nt_at_maps_to >>
741        map_every qexists_tac [`h.dom`,`h.cod`] >>
742        fsrw_tac [][] ) >>
743      metis_tac [] ) >>
744    map_every qx_gen_tac [`k`,`x`,`y`] >> strip_tac >>
745    first_x_assum match_mp_tac >>
746    map_every qexists_tac [`a@@x`,`b@@y`] >>
747    `(a@@y) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
748    `(b@@y) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
749    `(h@+y) :- g@@(a@@y) ��� g@@(b@@y) -:g.cod` by (
750      match_mp_tac nt_at_maps_to >>
751      map_every qexists_tac [`h.dom`,`h.cod`] >>
752      imp_res_tac maps_to_obj >> fsrw_tac [][] ) >>
753    `f (h@+y) (a@@y) (b@@y) :- (a@@y) ��� (b@@y) -:g.dom` by metis_tac [] >>
754    `a##k :- a@@x ��� a@@y -:g.dom` by (
755      match_mp_tac morf_maps_to >> metis_tac [maps_to_def] ) >>
756    `(a@@x) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
757    `(b@@x) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
758    `(h@+x) :- g@@(a@@x) ��� g@@(b@@x) -:g.cod` by (
759      match_mp_tac nt_at_maps_to >>
760      map_every qexists_tac [`h.dom`,`h.cod`] >>
761      imp_res_tac maps_to_obj >> fsrw_tac [][] ) >>
762    `f (h@+x) (a@@x) (b@@x) :- (a@@x) ��� (b@@x) -:g.dom` by metis_tac [] >>
763    `b##k :- b@@x ��� b@@y -:g.dom` by (
764      match_mp_tac morf_maps_to >> metis_tac [maps_to_def] ) >>
765    conj_asm1_tac >- (
766      match_mp_tac composable_maps_to >>
767      fsrw_tac [][is_functor_is_category] >>
768      fsrw_tac [][maps_to_in_def,composable_in_def] ) >>
769    conj_asm1_tac >- (
770      match_mp_tac composable_maps_to >>
771      fsrw_tac [][is_functor_is_category] >>
772      fsrw_tac [][maps_to_in_def,composable_in_def] ) >>
773    qmatch_abbrev_tac `g##(g1 o f1 -:g.dom) = g##(g2 o f2 -:g.dom)` >>
774    `f1 ���> g1 -:g.dom` by (
775      match_mp_tac maps_to_composable >>
776      srw_tac [][Abbr`f1`,Abbr`g1`] >>
777      map_every qexists_tac [`a@@x`,`a@@y`,`b@@y`] >>
778      srw_tac [][] ) >>
779    `f2 ���> g2 -:g.dom` by (
780      match_mp_tac maps_to_composable >>
781      srw_tac [][Abbr`f2`,Abbr`g2`] >>
782      map_every qexists_tac [`a@@x`,`b@@x`,`b@@y`] >>
783      srw_tac [][] ) >>
784    qspecl_then [`g`,`g.dom`,`g.cod`,`f1`,`g1`] mp_tac morf_comp >>
785    qspecl_then [`g`,`g.dom`,`g.cod`,`f2`,`g2`] mp_tac morf_comp >>
786    srw_tac [][] >>
787    `g##g1 = h@+y` by metis_tac [] >>
788    `g##f2 = h@+x` by metis_tac [] >>
789    `g##f1 = h.dom##k` by (
790      qpat_x_assum `k :- x ��� y -:(g ��� a).dom` mp_tac >>
791      unabbrev_all_tac >> fsrw_tac [][maps_to_in_def]  ) >>
792    `g##g2 = h.cod##k` by (
793      qpat_x_assum `k :- x ��� y -:(g ��� a).dom` mp_tac >>
794      unabbrev_all_tac >> fsrw_tac [][maps_to_in_def]  ) >>
795    fsrw_tac [][] >>
796    match_mp_tac naturality >>
797    qpat_x_assum `k :- x ��� y -:(g ��� a).dom` mp_tac >>
798    fsrw_tac [][] ) >>
799  fsrw_tac [][] >>
800  match_mp_tac nt_eq_thm >>
801  fsrw_tac [][] >>
802  qx_gen_tac `x` >> strip_tac >>
803  fsrw_tac [][mk_nt_def,restrict_def] >>
804  `(a@@x) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
805  `(b@@x) ��� g.dom.obj` by metis_tac [objf_in_obj,maps_to_obj] >>
806  `(h@+x) :- g@@(a@@x) ��� g@@(b@@x) -:g.cod` by (
807    match_mp_tac nt_at_maps_to >>
808    map_every qexists_tac [`h.dom`,`h.cod`] >>
809    imp_res_tac maps_to_obj >> fsrw_tac [][] ) >>
810  metis_tac []) >>
811fsrw_tac [][full_def,faithful_def] >>
812map_every qx_gen_tac [`n1`,`n2`] >>
813strip_tac >>
814match_mp_tac nt_eq_thm >>
815fsrw_tac [][] >>
816qx_gen_tac `x` >> strip_tac >>
817first_x_assum match_mp_tac >>
818map_every qexists_tac [`n1.dom@@x`,`n1.cod@@x`] >>
819fsrw_tac [][nt_at_maps_to] >>
820qpat_x_assum `postcomp_functor c g##n1 = Y` mp_tac >>
821fsrw_tac [][] >> strip_tac >>
822metis_tac [functor_nt_at,is_nat_trans_def,nat_trans_axioms_def]);
823
824val inj_obj_functor_cats = Q.store_thm(
825"inj_obj_functor_cats",
826`���g c. is_category c ��� is_functor g ��� faithful g ��� inj_obj g ��� inj_obj (postcomp_functor c g)`,
827srw_tac [][inj_obj_def] >>
828pop_assum mp_tac >> srw_tac [][] >>
829match_mp_tac functor_eq_thm >>
830fsrw_tac [][faithful_def] >>
831qx_gen_tac `h` >> strip_tac >>
832first_x_assum match_mp_tac >>
833map_every qexists_tac [`a@@h.dom`,`a@@h.cod`] >>
834conj_tac >- (
835  match_mp_tac morf_maps_to >>
836  srw_tac [][maps_to_in_def] ) >>
837conj_tac >- (
838  match_mp_tac morf_maps_to >>
839  srw_tac [][] >>
840  `���x. x ��� a.dom.obj ��� (a@@x = b@@x)` by (
841    srw_tac [][] >>
842    first_x_assum match_mp_tac >>
843    conj_tac >- metis_tac [objf_in_obj] >>
844    conj_tac >- metis_tac [objf_in_obj] >>
845    metis_tac [functor_comp_objf,composable_def] ) >>
846  metis_tac [mor_obj,maps_to_in_def,maps_to_def] ) >>
847metis_tac [composable_def,functor_comp_morf]);
848
849val pre_eval_functor_def = Define`
850  pre_eval_functor c v p = <|
851    dom := [c���v]; cod := v;
852    map := ��n. n @+ p |>`;
853
854val pre_eval_functor_components = Q.store_thm(
855"pre_eval_functor_components",
856`���c v p. ((pre_eval_functor c v p).dom = [c���v]) ���
857         ((pre_eval_functor c v p).cod = v) ���
858         (���n. (pre_eval_functor c v p)##n = n @+ p)`,
859srw_tac [][pre_eval_functor_def,morf_def]);
860val _ = export_rewrites["pre_eval_functor_components"];
861
862val pre_eval_functor_objf = Q.store_thm(
863"pre_eval_functor_objf",
864`���c v x p. is_category c ��� is_category v ��� p ��� [c���v].obj ��� x ��� c.obj ���
865  ((pre_eval_functor c v x)@@p = p@@x)`,
866srw_tac [][Once objf_def] >>
867SELECT_ELIM_TAC >>
868metis_tac [objf_in_obj,id_inj]);
869
870val eval_functor_def = Define`
871  eval_functor c v p = mk_functor (pre_eval_functor c v p)`;
872
873val is_functor_eval_functor = Q.store_thm(
874"is_functor_eval_functor",
875`���c v p. is_category c ��� is_category v ��� p ��� c.obj ���
876  is_functor (eval_functor c v p)`,
877srw_tac [][eval_functor_def] >>
878srw_tac [][functor_axioms_def] >- (
879  fsrw_tac [][pre_eval_functor_objf] >>
880  match_mp_tac nt_at_maps_to >>
881  metis_tac [maps_to_def] )
882>- metis_tac [objf_in_obj] >>
883fsrw_tac [][composable_nts_def]);
884val _ = export_rewrites["is_functor_eval_functor"];
885
886val eval_functor_dom_cod = Q.store_thm(
887"eval_functor_dom_cod",
888`���c v p. ((eval_functor c v p).dom = [c���v]) ���
889         ((eval_functor c v p).cod = v)`,
890srw_tac [][eval_functor_def]);
891val _ = export_rewrites["eval_functor_dom_cod"];
892
893val eval_functor_morf_objf = Q.store_thm(
894"eval_functor_morf_objf",
895`���c v p. is_category c ��� is_category v ��� p ��� c.obj ���
896  (���x. x ��� [c���v].obj ��� ((eval_functor c v p)@@x = x@@p)) ���
897  (���f. f ��� [c���v].mor ��� ((eval_functor c v p)##f = f @+ p))`,
898srw_tac [][eval_functor_def,pre_eval_functor_objf]);
899val _ = export_rewrites["eval_functor_morf_objf"];
900
901val id_nt_inj = Q.store_thm(
902"id_nt_inj",
903`���f g. is_functor f ��� is_functor g ��� (id_nt f = id_nt g) ��� (f = g)`,
904srw_tac [][] >>
905Q.ISPEC_THEN `[f.dom���f.cod]` assume_tac id_inj >>
906pop_assum match_mp_tac >>
907imp_res_tac is_functor_is_category >>
908imp_res_tac is_category_functor_cat >>
909srw_tac [][] >> fsrw_tac [][id_nt_def,mk_nt_def]);
910
911val K_nt_def = Define`
912  K_nt j c f = mk_nt <| dom := K_functor j c f.dom; cod := K_functor j c f.cod; map := K f |>`;
913
914val is_nat_trans_K_nt = Q.store_thm(
915"is_nat_trans_K_nt",
916`���j c f. is_category j ��� is_category c ��� f ��� c.mor ��� is_nat_trans (K_nt j c f)`,
917srw_tac [][K_nt_def] >>
918`f.dom ��� c.obj ��� f.cod ��� c.obj` by metis_tac [mor_obj] >>
919srw_tac [][nat_trans_axioms_def] >>
920fsrw_tac [][maps_to_in_def]);
921
922val K_nt_dom = Q.store_thm(
923"K_nt_dom",
924`���j c f. (K_nt j c f).dom = K_functor j c f.dom`,
925srw_tac [][K_nt_def]);
926
927val K_nt_cod = Q.store_thm(
928"K_nt_cod",
929`���j c f. (K_nt j c f).cod = K_functor j c f.cod`,
930srw_tac [][K_nt_def]);
931
932val K_nt_at = Q.store_thm(
933"K_nt_at",
934`���c j f x. x ��� j.obj ��� ((K_nt j c f)@+x = f)`,
935srw_tac [][K_nt_def,mk_nt_def,restrict_def]);
936
937val K_nt_id = Q.store_thm(
938"K_nt_id",
939`���j c x. is_category j ��� is_category c ��� x ��� c.obj ��� (K_nt j c (id x -:c) = id_nt (K_functor j c x))`,
940srw_tac [][] >>
941match_mp_tac nt_eq_thm >>
942imp_res_tac id_mor >>
943srw_tac [][id_dom_cod,K_nt_dom,
944           K_nt_cod,K_nt_dom,K_nt_at,is_nat_trans_K_nt] >>
945srw_tac [][id_nt_at]);
946
947val K_nt_maps_to = Q.store_thm(
948"K_nt_maps_to",
949`���j c f x y. is_category j ��� is_category c ��� f :- x ��� y -:c ���
950  (K_nt j c f) :- (K_functor j c x) ��� (K_functor j c y)`,
951srw_tac [][maps_to_in_def,K_nt_dom,K_nt_cod]);
952
953val _ = export_rewrites
954["is_nat_trans_K_nt","K_nt_dom","K_nt_cod","K_nt_at",
955 "K_nt_id","K_nt_maps_to"];
956
957val pre_diagonal_functor_def = Define`
958  pre_diagonal_functor j c = <|
959    dom := c; cod := [j���c]; map := K_nt j c |>`;
960
961val pre_diagonal_functor_dom = Q.store_thm(
962"pre_diagonal_functor_dom",
963`���c j. (pre_diagonal_functor j c).dom = c`,
964srw_tac [][pre_diagonal_functor_def]);
965
966val pre_diagonal_functor_cod = Q.store_thm(
967"pre_diagonal_functor_cod",
968`���c j. (pre_diagonal_functor j c).cod = [j���c]`,
969srw_tac [][pre_diagonal_functor_def]);
970
971val _ = export_rewrites ["pre_diagonal_functor_dom","pre_diagonal_functor_cod"];
972
973val pre_diagonal_functor_objf = Q.store_thm(
974"pre_diagonal_functor_objf",
975`���c j x. is_category c ��� is_category j ��� x ��� c.obj ���
976((pre_diagonal_functor j c)@@x = K_functor j c x)`,
977srw_tac [][objf_def,morf_def] >>
978srw_tac [][pre_diagonal_functor_def] >>
979SELECT_ELIM_TAC >>
980srw_tac [][] >- (
981  qexists_tac `K_functor j c x` >>
982  fsrw_tac [][] ) >>
983pop_assum mp_tac >> srw_tac [][] >>
984fsrw_tac [][morphism_component_equality]);
985val _ = export_rewrites["pre_diagonal_functor_objf"];
986
987val diagonal_functor_def = Define`
988  diagonal_functor j c = mk_functor (pre_diagonal_functor j c)`;
989val _ = overload_on("\226\150\179",``diagonal_functor``);
990
991val is_functor_diagonal_functor = Q.store_thm(
992"is_functor_diagonal_functor",
993`���c j. is_category c ��� is_category j ��� is_functor (��� c j)`,
994srw_tac [][diagonal_functor_def] >>
995srw_tac [][functor_axioms_def] >>
996imp_res_tac maps_to_obj >>
997imp_res_tac maps_to_in_def >>
998fsrw_tac [][morf_def,pre_diagonal_functor_def] >- (
999  qexists_tac `K_functor c j x` >>
1000  srw_tac [][] ) >>
1001imp_res_tac composable_in_def >>
1002`K_nt c j f ������> K_nt c j g` by (
1003  srw_tac [][composable_nts_def] >>
1004  fsrw_tac [][morphism_component_equality] ) >>
1005srw_tac [][] >>
1006imp_res_tac comp_mor_dom_cod >>
1007match_mp_tac nt_eq_thm >>
1008fsrw_tac [][] >>
1009srw_tac [][nt_comp_def,K_functor_def]);
1010
1011val diagonal_functor_dom_cod = Q.store_thm(
1012"diagonal_functor_dom_cod",
1013`���j c. ((diagonal_functor j c).dom = c) ���
1014       ((diagonal_functor j c).cod = [j���c])`,
1015srw_tac [][diagonal_functor_def]);
1016val _ = export_rewrites["diagonal_functor_dom_cod"];
1017
1018val diagonal_functor_morf = Q.store_thm(
1019"diagonal_functor_morf",
1020`���c j f. f ��� c.mor ��� ((diagonal_functor j c)##f = K_nt j c f)`,
1021srw_tac [][diagonal_functor_def,morf_def,pre_diagonal_functor_def,mk_functor_def,restrict_def]);
1022val _ = export_rewrites["diagonal_functor_morf"];
1023
1024val diagonal_functor_objf = Q.store_thm(
1025"diagonal_functor_objf",
1026`���c j x. is_category c ��� is_category j ��� x ��� c.obj ���
1027((diagonal_functor j c)@@x = K_functor j c x)`,
1028srw_tac [][diagonal_functor_def]);
1029val _ = export_rewrites["diagonal_functor_objf"];
1030
1031val pre_itself_functor_def = Define`
1032  pre_itself_functor f =
1033    <| dom := unit_cat; cod := [f.dom���f.cod]; map := K (id_nt f) |>`;
1034
1035val pre_itself_functor_components = Q.store_thm(
1036"pre_itself_functor_components",
1037`���f. ((pre_itself_functor f).dom = unit_cat) ���
1038     ((pre_itself_functor f).cod = [f.dom���f.cod]) ���
1039     ((pre_itself_functor f).map = K (id_nt f))`,
1040srw_tac [][pre_itself_functor_def]);
1041val _ = export_rewrites["pre_itself_functor_components"];
1042
1043val pre_itself_functor_morf = Q.store_thm(
1044"pre_itself_functor_morf",
1045`���f u. (pre_itself_functor f)##u = (id_nt f)`,
1046srw_tac [][morf_def]);
1047
1048val pre_itself_functor_objf = Q.store_thm(
1049"pre_itself_functor_objf",
1050`���f u. is_functor f ��� ((pre_itself_functor f)@@u = f)`,
1051srw_tac [][objf_def,morf_def] >>
1052SELECT_ELIM_TAC >>
1053conj_tac >- (
1054  qexists_tac `f` >>
1055  `f ��� [f.dom���f.cod].obj` by srw_tac [][] >>
1056  srw_tac [][] ) >>
1057qx_gen_tac `g` >> strip_tac >>
1058`g ��� [f.dom���f.cod].obj` by srw_tac [][] >>
1059fsrw_tac [][] >>
1060Q.ISPEC_THEN `[f.dom���f.cod]` (match_mp_tac o GSYM) id_inj >>
1061srw_tac [][is_functor_is_category]);
1062
1063val _ = export_rewrites["pre_itself_functor_morf","pre_itself_functor_objf"];
1064
1065val itself_functor_def = Define`
1066  itself_functor f = mk_functor (pre_itself_functor f)`;
1067
1068val is_functor_itself_functor = Q.store_thm(
1069"is_functor_itself_functor",
1070`���f. is_functor f ��� is_functor (itself_functor f)`,
1071srw_tac [][itself_functor_def] >>
1072srw_tac [][functor_axioms_def] >>
1073srw_tac [][is_functor_is_category] >- (
1074  qexists_tac `f` >> srw_tac [][] ) >>
1075Q.ISPECL_THEN [`[f.dom���f.cod]`,`f`] mp_tac id_comp_id >>
1076asm_simp_tac std_ss
1077[is_functor_is_category,is_category_functor_cat,functor_cat_obj,maps_to_def,functor_cat_id] >>
1078srw_tac [][]);
1079
1080val itself_functor_components = Q.store_thm(
1081"itself_functor_components",
1082`���f. ((itself_functor f).dom = unit_cat) ���
1083     ((itself_functor f).cod = [f.dom���f.cod]) ���
1084     ((itself_functor f).map = K (id_nt f))`,
1085srw_tac [][itself_functor_def,mk_functor_def,restrict_def,FUN_EQ_THM]);
1086val _ = export_rewrites["itself_functor_components"];
1087
1088val itself_functor_morf = Q.store_thm(
1089"itself_functor_morf",
1090`���f u. (itself_functor f)##u = (id_nt f)`,
1091srw_tac [][morf_def]);
1092
1093val itself_functor_objf = Q.store_thm(
1094"itself_functor_objf",
1095`���f u. is_functor f ��� ((itself_functor f)@@u = f)`,
1096srw_tac [][itself_functor_def]);
1097val _ = export_rewrites["itself_functor_morf","itself_functor_objf"];
1098
1099val equivalence_pair_def = Define`
1100  equivalence_pair f g = (f ���> g) ��� (g ���> f) ���
1101    (f ��� g ��� id_functor g.dom -:[g.dom���g.dom]) ���
1102    (g ��� f ��� id_functor f.dom -:[f.dom���f.dom])`;
1103
1104val equivalence_def = Define`
1105  equivalence f = ���g. is_functor g ��� equivalence_pair f g`;
1106
1107(*
1108val equivalence_full_faithful_ess_surj = Q.store_thm(
1109"equivalence_full_faithful_ess_surj", (* Mac Lane pp 91-92 *)
1110`���f. is_functor f ��� (equivalence f = full f ��� faithful f ��� ess_surj_obj f)`,
1111gen_tac >> strip_tac >> EQ_TAC >> strip_tac >- (
1112  fsrw_tac [][equivalence_def,equivalence_pair_def] >>
1113  fsrw_tac [][iso_objs_def,iso_pair_between_objs_def] >>
1114  qmatch_assum_rename_tac `n1.dom = g ��� f` >>
1115  qmatch_assum_abbrev_tac `X = g ��� f` >>
1116  qmatch_assum_rename_tac `n2.dom = f ��� g` >>
1117  qunabbrev_tac `X` >>
1118  `���h x y. h :- x ��� y -:f.dom ��� (n1 @+ y o (g ��� f)##h -:f.dom = ((id_functor f.dom)##h) o n1 @+ x -:f.dom)` by (
1119    rpt gen_tac >> strip_tac >>
1120    match_mp_tac naturality >>
1121    fsrw_tac [][functor_cat_iso_pair,composable_nts_def] ) >>
1122  imp_res_tac is_functor_is_category >>
1123  `���a. a ��� f.dom.obj ��� (n1 @+ a) :- (g ��� f)@@a ��� a -:f.dom` by (
1124    srw_tac [][] >>
1125    match_mp_tac nt_at_maps_to >>
1126    map_every qexists_tac [`n1.dom`,`n1.cod`] >>
1127    fsrw_tac [][functor_cat_iso_pair,composable_nts_def]) >>
1128  `faithful f` by (
1129    simp_tac (srw_ss()) [faithful_def] >>
1130    map_every qx_gen_tac [`k1`,`k2`,`a`,`b`] >>
1131    strip_tac >>
1132    first_assum (qspecl_then [`k1`,`a`,`b`] mp_tac) >>
1133    first_x_assum (qspecl_then [`k2`,`a`,`b`] mp_tac) >>
1134    `k1 ��� f.dom.mor ��� k2 ��� f.dom.mor` by fsrw_tac [][maps_to_in_def] >>
1135    srw_tac [][] >>
1136    `(k1 o n1 @+ a -:f.dom) o (n1 @+ a)����� -:f.dom -:f.dom =
1137     (k2 o n1 @+ a -:f.dom) o (n1 @+ a)����� -:f.dom -:f.dom` by srw_tac [][] >>
1138    pop_assum mp_tac >>
1139    `iso f.dom (n1 @+ a)` by (
1140      metis_tac [iso_def,functor_cat_iso_pair,maps_to_obj] ) >>
1141    qpat_x_assum `k2 o X -:f.dom = k1 o Y -:f.dom` (K ALL_TAC) >>
1142    `(n1 @+ a)�����-:f.dom ���> n1 @+ a -:f.dom` by (
1143      metis_tac [inv_composable,inv_idem] ) >>
1144    `a ��� f.dom.obj` by metis_tac [maps_to_obj] >>
1145    `n1 @+ a ���> k1 -:f.dom` by ( metis_tac [maps_to_composable] ) >>
1146    `n1 @+ a ���> k2 -:f.dom` by ( metis_tac [maps_to_composable] ) >>
1147    fsrw_tac [][comp_inv_id,comp_assoc,maps_to_in_def] ) >>
1148  `���h x y. h :- x ��� y -:g.dom ��� (n2 @+ y o (f ��� g)##h -:g.dom = ((id_functor g.dom)##h) o n2 @+ x -:g.dom)` by (
1149    rpt gen_tac >> strip_tac >>
1150    match_mp_tac naturality >>
1151    fsrw_tac [][functor_cat_iso_pair,composable_nts_def] ) >>
1152  `���a. a ��� g.dom.obj ��� (n2 @+ a) :- (f ��� g)@@a ��� a -:g.dom` by (
1153    srw_tac [][] >>
1154    match_mp_tac nt_at_maps_to >>
1155    map_every qexists_tac [`n2.dom`,`n2.cod`] >>
1156    fsrw_tac [][functor_cat_iso_pair,composable_nts_def]) >>
1157  `faithful g` by (
1158    simp_tac (srw_ss()) [faithful_def] >>
1159    map_every qx_gen_tac [`k1`,`k2`,`a`,`b`] >>
1160    strip_tac >>
1161    first_assum (qspecl_then [`k1`,`a`,`b`] mp_tac) >>
1162    first_x_assum (qspecl_then [`k2`,`a`,`b`] mp_tac) >>
1163    `k1 ��� g.dom.mor ��� k2 ��� g.dom.mor` by fsrw_tac [][maps_to_in_def] >>
1164    srw_tac [][] >>
1165    `(k1 o n2 @+ a -:g.dom) o (n2 @+ a)����� -:g.dom -:g.dom =
1166     (k2 o n2 @+ a -:g.dom) o (n2 @+ a)����� -:g.dom -:g.dom` by srw_tac [][] >>
1167    pop_assum mp_tac >>
1168    `iso g.dom (n2 @+ a)` by (
1169      metis_tac [iso_def,functor_cat_iso_pair,maps_to_obj] ) >>
1170    qpat_x_assum `k2 o X -:g.dom = k1 o Y -:g.dom` (K ALL_TAC) >>
1171    `(n2 @+ a)�����-:g.dom ���> n2 @+ a -:g.dom` by (
1172      metis_tac [inv_composable,inv_idem] ) >>
1173    `a ��� g.dom.obj` by metis_tac [maps_to_obj] >>
1174    `n2 @+ a ���> k1 -:g.dom` by ( metis_tac [maps_to_composable] ) >>
1175    `n2 @+ a ���> k2 -:g.dom` by ( metis_tac [maps_to_composable] ) >>
1176    fsrw_tac [][comp_inv_id,comp_assoc,maps_to_in_def] )
1177  `full f` by (
1178    srw_tac [][full_def] >>
1179    qabbrev_tac `w = n1 @+ b o (g##h) o (n1 @+ a)����� -:f.dom -:f.dom -:f.dom` >>
1180    qexists_tac `w` >>
1181    `n1 @+ a :- (g ��� f)@@a ��� a -:f.dom` by metis_tac [] >>
1182    `(n1 @+ a)����� -: f.dom :- a ��� (g ��� f)@@a -:f.dom` by (
1183      match_mp_tac inv_maps_to >>
1184      fsrw_tac [][maps_to_in_def] >>
1185      srw_tac [][iso_def] >>
1186      fsrw_tac [][functor_cat_iso_pair] >>
1187      metis_tac [] ) >>
1188    conj_asm1_tac >- (
1189      qunabbrev_tac `w` >>
1190      match_mp_tac maps_to_comp >>
1191      qexists_tac `(g ��� f)@@b` >>
1192      conj_tac >- srw_tac [][] >>
1193      conj_tac >- (
1194        match_mp_tac maps_to_comp >>
1195        qexists_tac `(g ��� f)@@a` >>
1196        conj_tac >- srw_tac [][] >>
1197        conj_tac >- srw_tac [][] >>
1198        match_mp_tac morf_maps_to >>
1199        map_every qexists_tac [`g.dom`,`f@@a`,`f@@b`] >>
1200        fsrw_tac [][] ) >>
1201      srw_tac [][] ) >>
1202    `g##h :- g@@(f@@a) ��� g@@(f@@b) -:f.dom` by (
1203      match_mp_tac morf_maps_to >>
1204      fsrw_tac [][] >> metis_tac [] ) >>
1205    qsuff_tac `f##w :- f@@a ��� f@@b -:g.dom ��� (g##(f##w) = g##h)` >-
1206      metis_tac [faithful_def] >>
1207    conj_asm1_tac >- (
1208      match_mp_tac morf_maps_to >>
1209      map_every qexists_tac [`f.dom`,`a`,`b`] >>
1210      fsrw_tac [][] >>
1211      qunabbrev_tac `w` >>
1212      match_mp_tac maps_to_comp >>
1213      qexists_tac `(g ��� f)@@b` >>
1214      fsrw_tac [][] >>
1215      match_mp_tac maps_to_comp >>
1216      qexists_tac `(g ��� f)@@a` >>
1217      fsrw_tac [][] ) >>
1218    first_x_assum (qspecl_then [`w`,`a`,`b`] mp_tac) >>
1219    `w ��� f.dom.mor` by fsrw_tac [][maps_to_in_def] >>
1220    srw_tac [][] >>
1221    `((n1 @+ b)�����-:f.dom) o (n1 @+ b o g##(f##w) -:f.dom) -:f.dom =
1222     ((n1 @+ b)�����-:f.dom) o (w o n1 @+ a -:f.dom) -:f.dom` by srw_tac [][] >>
1223    pop_assum mp_tac >>
1224    qpat_x_assum `n1 @+ b o X -:f.dom = Y` (K ALL_TAC) >>
1225    `g##(f##w) ���> n1 @+ b -:f.dom` by (
1226      match_mp_tac maps_to_composable >>
1227      map_every qexists_tac [`g@@(f@@a)`,`g@@(f@@b)`,`b`] >>
1228      conj_tac >- (
1229        match_mp_tac morf_maps_to >>
1230        map_every qexists_tac [`g.dom`,`f@@a`,`f@@b`] >>
1231        srw_tac [][] ) >>
1232      metis_tac [functor_comp_objf,composable_def] ) >>
1233    `iso f.dom (n1 @+ b)` by (
1234      fsrw_tac [][iso_def,functor_cat_iso_pair] >>
1235      metis_tac [] ) >>
1236    `n1 @+ b ���> (n1 @+ b)�����-:f.dom -:f.dom` by (
1237      metis_tac [inv_composable] ) >>
1238    `g##(f##w) ��� f.dom.mor ��� ((n1 @+ b).dom = (g##(f##w)).cod)` by (
1239      fsrw_tac [][composable_in_def] ) >>
1240    fsrw_tac [][GSYM comp_assoc,comp_inv_id] >>
1241    strip_tac >>
1242    qunabbrev_tac `w` >>
1243    qabbrev_tac `c = f.dom` >>
1244    qmatch_abbrev_tac `(q1�����-:c) o (q1 o gh o (q2�����-:c) -:c -:c) o q2 -:c -:c = gh` >>
1245    `iso c q2` by (
1246      fsrw_tac [][iso_def,functor_cat_iso_pair,Abbr`q2`] >>
1247      metis_tac [] ) >>
1248    `q2 ���> (q2�����-:c) -:c` by fsrw_tac [][inv_composable] >>
1249    `(q2�����-:c) ���> gh -:c` by (
1250      match_mp_tac maps_to_composable >>
1251      metis_tac [functor_comp_objf,composable_def] ) >>
1252    `gh ���> q1 -:c` by (
1253      match_mp_tac maps_to_composable >>
1254      metis_tac [functor_comp_objf,composable_def] ) >>
1255    `q1 ���> (q1�����-:c) -:c` by metis_tac [inv_composable] >>
1256    `gh o q2�����-:c -:c ���> q1 -:c` by metis_tac [composable_comp] >>
1257    `q2 ���> (q1 o gh o q2�����-:c -:c -:c) -:c` by metis_tac [composable_comp] >>
1258    qsuff_tac `((q1�����-:c) o (q1 o gh o q2�����-:c -:c -:c) -:c) o q2 -:c = gh` >-
1259      metis_tac [composable_comp,comp_assoc] >>
1260    qsuff_tac `(((q1�����-:c) o q1 -:c) o (gh o (q2�����-:c) -:c) -:c) o q2 -:c = gh` >-
1261      metis_tac [composable_comp,comp_assoc] >>
1262    qsuff_tac `(((q1�����-:c) o q1 -:c) o gh -:c) o ((q2�����-:c) o q2 -:c) -:c = gh` >-
1263      metis_tac [composable_comp,comp_assoc] >>
1264    fsrw_tac [][comp_inv_id,composable_in_def] >>
1265    match_mp_tac id_comp1 >>
1266    fsrw_tac [][] >>
1267    imp_res_tac maps_to_in_def >>
1268    fsrw_tac [][] ) >>
1269  srw_tac [boolSimps.DNF_ss][ess_surj_obj_def,iso_objs_def,iso_pair_between_objs_def] >>
1270  map_every qexists_tac [`g@@b`,`n2 @+ b`,`(n2 @+ b)�����-:g.dom`] >>
1271  conj_tac >- metis_tac [objf_in_obj] >>
1272  first_x_assum (qspec_then `b` mp_tac) >>
1273  srw_tac [][maps_to_in_def] >>
1274  srw_tac [][inv_in_def] >>
1275  SELECT_ELIM_TAC >>
1276  srw_tac [][] >>
1277  fsrw_tac [][functor_cat_iso_pair] >>
1278  metis_tac [] ) >>
1279*)
1280
1281val _ = export_theory ();
1282