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