1open HolKernel Parse boolLib boolSimps bossLib pred_setTheory zfset_axiomsTheory zfsetTheory pairTheory categoryTheory limitTheory ens_catTheory functorTheory nat_transTheory hom_functorTheory YonedaTheory; 2 3val _ = new_theory "zfset_cat"; 4val _ = ParseExtras.temp_loose_equality() 5 6val _ = srw_ss() 7val _ = diminish_srw_ss ["NORMEQ_ss"] 8val explode_def = Define` 9 explode z = {x | x In z}`; 10 11val implode_def = Define` 12 implode s = @z. explode z = s`; 13 14val implode_explode = Q.store_thm( 15"implode_explode", 16`���z. implode (explode z) = z`, 17srw_tac [][implode_def] >> 18SELECT_ELIM_TAC >> 19srw_tac [][] >- metis_tac [] >> 20fsrw_tac [][explode_def,EXTENSION] >> 21fsrw_tac [][Extension_ax]); 22val _ = export_rewrites["implode_explode"]; 23 24val explode_inj = Q.store_thm( 25"explode_inj", 26`���x y. (explode x = explode y) ��� (x = y)`, 27srw_tac [][explode_def,EXTENSION] >> 28srw_tac [][Extension_ax]); 29 30val IsSmall_def = Define` 31 IsSmall s = ���f z. INJ f s (explode z)`; 32(* WARNING THIS IS NOT HEREDITARILY SMALL *) 33 34val IsSmall_FINITE = Q.store_thm( 35"IsSmall_FINITE", 36`���s. FINITE s ��� IsSmall s`, 37ho_match_mp_tac FINITE_INDUCT >> 38srw_tac [][IsSmall_def] >> 39map_every qexists_tac [`��x. if x = e then z else f x`,`Suc z`] >> 40fsrw_tac [][INJ_DEF,explode_def,Suc_def,U_def,Singleton_def] >> 41srw_tac [][] >> metis_tac [NotInSelf]); 42 43val IsSmall_IMAGE = Q.store_thm( 44"IsSmall_IMAGE", 45`���s f. IsSmall s ��� IsSmall (IMAGE f s)`, 46srw_tac [][IsSmall_def] >> 47qmatch_assum_rename_tac `INJ g s (explode z)` >> 48map_every qexists_tac [`��x. g (@y. y ��� s ��� (f y = x))`,`z`] >> 49fsrw_tac [DNF_ss][INJ_DEF] >> 50srw_tac [][] >- ( 51 SELECT_ELIM_TAC >> 52 srw_tac [][] >> 53 metis_tac []) >> 54pop_assum mp_tac >> 55SELECT_ELIM_TAC >> 56SELECT_ELIM_TAC >> 57srw_tac [][] >> 58metis_tac []); 59val _ = export_rewrites["IsSmall_IMAGE"]; 60 61val IsSmall_IMAGE_iff = Q.store_thm( 62"IsSmall_IMAGE_iff", 63`���s t f. INJ f s t ��� (IsSmall (IMAGE f s) ��� IsSmall s)`, 64srw_tac [][EQ_IMP_THM] >> 65fsrw_tac [][IsSmall_def] >> 66qmatch_assum_rename_tac `INJ g (IMAGE f s) (explode z)` >> 67map_every qexists_tac [`g o f`,`z`] >> 68fsrw_tac [DNF_ss][INJ_DEF]); 69 70val IsSmall_explode = Q.store_thm( 71"IsSmall_explode", 72`���s. IsSmall s ��� (���z. s = explode z)`, 73srw_tac [][IsSmall_def,explode_def,EQ_IMP_THM] >> 74srw_tac [][EXTENSION] >- ( 75 qexists_tac `Image (LINV f s) (Spec z (��x. ���y. y ��� s ��� (x = f y)))` >> 76 srw_tac [][Spec_def,Image_def] >> 77 srw_tac [][EQ_IMP_THM] >- ( 78 IMP_RES_TAC LINV_DEF >> 79 fsrw_tac [][INJ_DEF] >> 80 metis_tac []) >> 81 metis_tac [LINV_DEF]) >> 82map_every qexists_tac [`I`,`z`] >> 83srw_tac [][INJ_DEF]); 84 85val explode_IsSmall = Q.store_thm( 86"explode_IsSmall", 87`���s. IsSmall (explode s)`, 88metis_tac [IsSmall_explode]); 89val _ = export_rewrites["explode_IsSmall"]; 90 91val In_implode = Q.store_thm( 92"In_implode", 93`���s x. IsSmall s ��� (x In implode s ��� x ��� s)`, 94srw_tac [][] >> 95imp_res_tac IsSmall_explode >> 96srw_tac [][explode_def]); 97val _ = export_rewrites["In_implode"]; 98 99val explode_implode = Q.store_thm( 100"explode_implode", 101`���s. IsSmall s ��� (explode (implode s) = s)`, 102srw_tac [][explode_def]); 103val _ = export_rewrites["explode_implode"]; 104 105val IsSmall_BIJ = Q.store_thm( 106"IsSmall_BIJ", 107`���s. IsSmall s ��� ���b z. BIJ b s (IMAGE SOME (explode z)) ��� 108 ���x. x ��� s ��� (b x = NONE)`, 109srw_tac [][IsSmall_def] >> 110qexists_tac `��x. if x ��� s then SOME (f x) else NONE` >> 111qexists_tac `Spec z (��x. ���y. y ��� s ��� (x = f y))` >> 112fsrw_tac [DNF_ss][BIJ_DEF,INJ_DEF,SURJ_DEF,explode_def,Spec_def] >> 113metis_tac []); 114 115val the_zfrep_def = Define` 116 the_zfrep s = @bz. BIJ (FST bz) s (IMAGE SOME (explode (SND bz))) ��� 117 ���x. x ��� s ��� (FST bz x = NONE)`; 118 119val the_zfrep_inj = Q.store_thm( 120"the_zfrep_inj", 121`���s1 s2. IsSmall s1 ��� IsSmall s2 ��� (the_zfrep s1 = the_zfrep s2) ��� (s1 = s2)`, 122simp_tac std_ss [the_zfrep_def,GSYM AND_IMP_INTRO] >> 123rpt gen_tac >> ntac 2 strip_tac >> 124imp_res_tac IsSmall_BIJ >> 125SELECT_ELIM_TAC >> 126conj_tac >- metis_tac [FST,SND] >> 127SELECT_ELIM_TAC >> 128conj_tac >- metis_tac [FST,SND] >> 129Cases >> srw_tac [][EXTENSION] >> 130srw_tac [][EQ_IMP_THM] >> spose_not_then strip_assume_tac >> 131res_tac >> fsrw_tac [DNF_ss][BIJ_DEF,SURJ_DEF] >> 132res_tac >> fsrw_tac [][]); 133 134val _ = overload_on("zfbij",``��s. FST(the_zfrep s)``); 135val _ = overload_on("zfrep",``��s. SND(the_zfrep s)``); 136 137val zfbij_SOME = Q.store_thm( 138"zfbij_SOME", 139`���s x. IsSmall s ��� (IS_SOME (zfbij s x) ��� x ��� s)`, 140rpt strip_tac >> 141srw_tac [][the_zfrep_def] >> 142SELECT_ELIM_TAC >> 143conj_tac >- metis_tac [FST,SND,IsSmall_BIJ] >> 144Cases >> srw_tac [][] >> 145Cases_on `x ��� s` >> res_tac >> fsrw_tac [][] >> 146fsrw_tac [DNF_ss][BIJ_DEF,SURJ_DEF] >> 147res_tac >> fsrw_tac [][]); 148 149val zfel_def = Define` 150 zfel s x = THE (zfbij s x)`; 151 152val elzf_def = Define` 153 elzf s z = LINV (zfbij s) s (SOME z)`; 154 155val In_zfrep_thm = Q.store_thm( 156"In_zfrep_thm", 157`���s z. IsSmall s ��� (z In zfrep s ��� ���x. x ��� s ��� (z = zfel s x))`, 158srw_tac [][zfel_def] >> 159srw_tac [][the_zfrep_def] >> 160SELECT_ELIM_TAC >> 161conj_tac >- metis_tac [FST,SND,IsSmall_BIJ] >> 162Cases >> srw_tac [][] >> 163fsrw_tac [DNF_ss][BIJ_DEF,SURJ_DEF,INJ_DEF,explode_def] >> 164EQ_TAC >- ( 165 strip_tac >> res_tac >> 166 qexists_tac `y` >> srw_tac [][] ) >> 167srw_tac [][] >> 168qmatch_rename_tac `THE (b x) In z` >> 169Cases_on `b x` >> 170res_tac >> fsrw_tac [][] >> srw_tac [][]); 171 172val elzf_zfel = Q.store_thm( 173"elzf_zfel", 174`���s x. IsSmall s ��� x ��� s ��� (elzf s (zfel s x) = x)`, 175srw_tac[][elzf_def,zfel_def] >> 176imp_res_tac zfbij_SOME >> 177Cases_on `zfbij s x` >> fsrw_tac [][] >> 178pop_assum (assume_tac o SYM) >> fsrw_tac [][] >> 179match_mp_tac (MP_CANON LINV_DEF) >> 180srw_tac [][the_zfrep_def] >> 181SELECT_ELIM_TAC >> 182conj_tac >- metis_tac [FST,SND,IsSmall_BIJ] >> 183metis_tac [BIJ_DEF]); 184 185val zfel_elzf = Q.store_thm( 186"zfel_elzf", 187`���s z. IsSmall s ��� z In zfrep s ��� (zfel s (elzf s z) = z)`, 188srw_tac [][] >> 189`���x. x ��� s ��� (z = zfel s x)` by metis_tac[In_zfrep_thm] >> 190srw_tac [][elzf_zfel]); 191 192val _ = export_rewrites["elzf_zfel","zfel_elzf"]; 193 194val zfrep_empty = Q.store_thm( 195"zfrep_empty", 196`���s. IsSmall s ��� ((zfrep s = {}) = (s = {}))`, 197srw_tac [][EXTENSION,Extension_ax] >> 198metis_tac [Empty_def,In_zfrep_thm]); 199val _ = export_rewrites["zfrep_empty"]; 200 201val IsTypedFn_def = Define` 202 IsTypedFn f = f.map In (f.dom -> f.cod)`; 203 204val TypedGraphFn_def = Define` 205 TypedGraphFn (X,Y) f = <| 206 dom := X; cod := Y; map := GraphFn X f |>`; 207 208val TypedGraphFn_components = Q.store_thm( 209"TypedGraphFn_components", 210`���X Y f. ((TypedGraphFn (X,Y) f).dom = X) ��� 211 ((TypedGraphFn (X,Y) f).cod = Y) ��� 212 ((TypedGraphFn (X,Y) f).map = GraphFn X f)`, 213srw_tac [][TypedGraphFn_def]); 214val _ = export_rewrites["TypedGraphFn_components"]; 215 216val IsTypedFnTypedGraphFn = Q.store_thm( 217"IsTypedFnTypedGraphFn", 218`���f X Y. IsTypedFn (TypedGraphFn (X,Y) f) = HasFnType f X Y`, 219srw_tac [][IsTypedFn_def,TypedGraphFn_def,GraphFnType,EQ_IMP_THM] >> 220srw_tac [][HasFnType_def] >> metis_tac [InFn,GraphFnAp]); 221val _ = export_rewrites["IsTypedFnTypedGraphFn"]; 222 223val ComposeTypedFn_def = Define` 224 ComposeTypedFn = compose (��f g. ComposeFn (f.dom,f.cod,g.cod) g.map f.map)`; 225 226val _ = add_infix("|o|",800,RIGHT); 227val _ = overload_on("|o|",``��g f. ComposeTypedFn f g``); 228 229val ComposeTypedFn_components = Q.store_thm( 230"ComposeTypedFn_components", 231`���f g. (f ���> g) ��� 232 (((g |o| f).dom = f.dom) ��� 233 ((g |o| f).cod = g.cod) ��� 234 ((g |o| f).map = ComposeFn(f.dom,f.cod,g.cod) g.map f.map))`, 235srw_tac [][ComposeTypedFn_def]); 236val _ = export_rewrites["ComposeTypedFn_components"]; 237 238val pre_set_cat_def = Define` 239 pre_set_cat = <| 240 obj := UNIV ; 241 mor := {f | IsTypedFn f} ; 242 id_map := IdFn ; 243 comp := ��f g. (g |o| f).map |>`; 244 245val pre_set_cat_obj_mor = Q.store_thm( 246"pre_set_cat_obj_mor", 247`(���x. x ��� pre_set_cat.obj) ��� 248 (���f. f ��� pre_set_cat.mor = IsTypedFn f)`, 249srw_tac [][pre_set_cat_def]); 250val _ = export_rewrites["pre_set_cat_obj_mor"]; 251 252val pre_set_cat_id = Q.store_thm( 253"pre_set_cat_id", 254`���x. (id x -:pre_set_cat) = TypedGraphFn (x,x) I`, 255srw_tac [][id_in_def,restrict_def,pre_set_cat_def,TypedGraphFn_def,IdFn_eq_GraphFnI]); 256val _ = export_rewrites["pre_set_cat_id"]; 257 258val pre_set_cat_maps_to_in = Q.store_thm( 259"pre_set_cat_maps_to_in", 260`���f x y. f :- x ��� y -:pre_set_cat ��� IsTypedFn f ��� f :- x ��� y`, 261srw_tac [][maps_to_in_def,EQ_IMP_THM]); 262val _ = export_rewrites["pre_set_cat_maps_to_in"]; 263 264val pre_set_cat_composable_in = Q.store_thm( 265"pre_set_cat_composable_in", 266`���f g. f ���> g -:pre_set_cat ��� IsTypedFn f ��� IsTypedFn g ��� f ���> g`, 267srw_tac [][composable_in_def]); 268val _ = export_rewrites["pre_set_cat_composable_in"]; 269 270val pre_set_cat_compose_in = Q.store_thm( 271"pre_set_cat_compose_in", 272`���f g. f ���> g -:pre_set_cat ��� (g o f -:pre_set_cat = g |o| f)`, 273srw_tac [][compose_in_def,restrict_def,pre_set_cat_def] >> 274srw_tac [][morphism_component_equality]); 275val _ = export_rewrites["pre_set_cat_compose_in"]; 276 277val set_cat_def = Define` 278 set_cat = mk_cat pre_set_cat`; 279 280val is_category_set_cat = Q.store_thm( 281"is_category_set_cat", 282`is_category set_cat`, 283srw_tac [][set_cat_def] >> 284srw_tac [][category_axioms_def] >- ( 285 srw_tac [][HasFnType_def] ) 286>- ( 287 qmatch_abbrev_tac `f o g -:pre_set_cat = f` >> 288 match_mp_tac EQ_TRANS >> 289 qexists_tac `f |o| g` >> 290 reverse conj_tac >- ( 291 srw_tac [][Abbr`g`,morphism_component_equality,GSYM IdFn_eq_GraphFnI] >> 292 match_mp_tac ComposeFnId1 >> fsrw_tac [][IsTypedFn_def] ) >> 293 match_mp_tac pre_set_cat_compose_in >> 294 srw_tac [][Abbr`g`,IdFnType,HasFnType_def] ) 295>- ( 296 qmatch_abbrev_tac `g o f -:pre_set_cat = f` >> 297 match_mp_tac EQ_TRANS >> 298 qexists_tac `g |o| f` >> 299 reverse conj_tac >- ( 300 srw_tac [][Abbr`g`,morphism_component_equality,GSYM IdFn_eq_GraphFnI] >> 301 match_mp_tac ComposeFnId2 >> fsrw_tac [][IsTypedFn_def] ) >> 302 match_mp_tac pre_set_cat_compose_in >> 303 srw_tac [][Abbr`g`,IdFnType,HasFnType_def] ) 304>- ( 305 qsuff_tac `f ���> (h |o| g) -:pre_set_cat ��� (g |o| f) ���> h -:pre_set_cat` >- ( 306 srw_tac [][] >> srw_tac [][morphism_component_equality] >> 307 match_mp_tac (GSYM ComposeFnAssoc) >> fsrw_tac [][IsTypedFn_def] ) >> 308 srw_tac [][IsTypedFn_def] >> 309 match_mp_tac ComposeFnType >> 310 fsrw_tac [][IsTypedFn_def] ) >> 311srw_tac [][IsTypedFn_def] >> 312match_mp_tac ComposeFnType >> 313fsrw_tac [][IsTypedFn_def]) 314val _ = export_rewrites["is_category_set_cat"]; 315 316val set_cat_obj = Q.store_thm( 317"set_cat_obj", 318`set_cat.obj = UNIV`, 319srw_tac [][set_cat_def,pre_set_cat_def]); 320 321val set_cat_mor = Q.store_thm( 322"set_cat_mor", 323`set_cat.mor = {f | IsTypedFn f}`, 324srw_tac [][set_cat_def,pre_set_cat_def]); 325 326val set_cat_id = Q.store_thm( 327"set_cat_id", 328`���x. (id x -:set_cat) = TypedGraphFn (x,x) I`, 329srw_tac [][set_cat_def]); 330 331val set_cat_composable_in = Q.store_thm( 332"set_cat_composable_in", 333`���f g. f ���> g -:set_cat ��� IsTypedFn f ��� IsTypedFn g ��� f ���> g`, 334srw_tac [][set_cat_def]); 335 336val set_cat_compose_in = Q.store_thm( 337"set_cat_compose_in", 338`���f g. f ���> g -:set_cat ��� (g o f -:set_cat = g |o| f)`, 339srw_tac [][set_cat_def]); 340 341val set_cat_maps_to_in = Q.store_thm( 342"set_cat_maps_to_in", 343`���f x y. f :- x ��� y -:set_cat ��� IsTypedFn f ��� f :- x ��� y`, 344srw_tac [][set_cat_def]); 345 346val _ = export_rewrites[ 347"set_cat_obj","set_cat_mor","set_cat_id", 348"set_cat_composable_in","set_cat_compose_in", 349"set_cat_maps_to_in"]; 350 351val has_binary_products_set_cat = Q.store_thm( 352"has_binary_products_set_cat", 353`has_binary_products set_cat`, 354srw_tac [][has_binary_products_thm,is_binary_product_thm] >> 355map_every qexists_tac [`TypedGraphFn (Prod a b, a) Fst`,`TypedGraphFn (Prod a b, b) Snd`] >> 356fsrw_tac [][HasFnType_def] >> 357conj_tac >- metis_tac [FstType] >> 358conj_tac >- metis_tac [SndType] >> 359rpt gen_tac >> strip_tac >> 360fsrw_tac [][EXISTS_UNIQUE_THM] >> 361`���m. IsTypedFn m ��� (m.dom = p1.dom) ��� (m.cod = a # b) ��� 362 m ���> TypedGraphFn (a # b,a) Fst -:set_cat ��� 363 m ���> TypedGraphFn (a # b,b) Snd -:set_cat` by ( 364 srw_tac [][HasFnType_def] >> 365 metis_tac [InProd,FstType,SndType,IsTypedFn_def,InFn] ) >> 366conj_tac >- ( 367 qexists_tac `TypedGraphFn (p1.dom, a # b) (��x. (Pair(p1.map ' x)(p2.map ' x)))` >> 368 conj_asm1_tac >- ( 369 srw_tac [][HasFnType_def] >> 370 metis_tac [InFn,IsTypedFn_def,InProd] ) >> 371 conj_tac >> ( 372 qmatch_abbrev_tac `f o g -:set_cat = x` >> 373 `g ���> f -:set_cat` by metis_tac [] >> 374 srw_tac [][] >> 375 unabbrev_all_tac >> 376 srw_tac [][morphism_component_equality] >> 377 fsrw_tac [][ComposeGraphFns] >> 378 qmatch_rename_tac `_ = p.map` >> 379 match_mp_tac FnEqThm >> 380 map_every qexists_tac [`p.dom`,`p.cod`] >> 381 fsrw_tac [][GraphFnAp,HasFnType_def] >> 382 conj_tac >- ( 383 match_mp_tac GraphFnType >> 384 srw_tac [][HasFnType_def] ) >> 385 fsrw_tac [][IsTypedFn_def] >> 386 fsrw_tac [][Fst,Snd] )) >> 387srw_tac [][] >> 388qmatch_rename_tac `m1 = m2` >> 389first_assum (qspec_then `m1` mp_tac) >> 390first_x_assum (qspec_then `m2` mp_tac) >> 391ntac 2 strip_tac >> 392rpt (qpat_x_assum `f o g -:set_cat = h` mp_tac) >> 393ntac 2 (pop_assum mp_tac) >> 394fsrw_tac [][] >> 395srw_tac [][morphism_component_equality] >> 396match_mp_tac FnEqThm >> 397map_every qexists_tac [`p1.dom`,`p1.cod # p2.cod`] >> 398fsrw_tac [][IsTypedFn_def] >> 399srw_tac [][] >> 400`m1.map ' x In (p1.cod # p2.cod)` by metis_tac [InFn] >> 401`m2.map ' x In (p1.cod # p2.cod)` by metis_tac [InFn] >> 402fsrw_tac [][InProdEq] >> 403qmatch_rename_tac `Pair x11 x21 = Pair x12 x22` >> 404qmatch_assum_abbrev_tac `ComposeFn (X,Y,Z) (GraphFn (a#b) P) Q = R` >> 405map_every qunabbrev_tac [`P`,`Q`,`R`,`Z`] >> 406`(ComposeFn (X,Y,a) (GraphFn Y Fst) m1.map) ' x = p1.map ' x` by srw_tac [][] >> 407`(ComposeFn (X,Y,b) (GraphFn Y Snd) m1.map) ' x = p2.map ' x` by srw_tac [][] >> 408`(ComposeFn (X,Y,a) (GraphFn Y Fst) m2.map) ' x = p1.map ' x` by srw_tac [][] >> 409`(ComposeFn (X,Y,b) (GraphFn Y Snd) m2.map) ' x = p2.map ' x` by srw_tac [][] >> 410rpt (qpat_x_assum `ComposeFn (X,Y,Z) (GraphFn Y P) Q = R` (K ALL_TAC)) >> 411ntac 4 (pop_assum mp_tac) >> 412`GraphFn Y Fst In (Y -> a)` by metis_tac [GraphFnType] >> 413`GraphFn Y Snd In (Y -> b)` by metis_tac [GraphFnType] >> 414`Pair x11 x21 In Y` by metis_tac [InProd] >> 415`Pair x12 x22 In Y` by metis_tac [InProd] >> 416fsrw_tac [][ApComposeFn,GraphFnAp] >> 417fsrw_tac [][Fst,Snd]); 418 419val pre_set_to_ens_def = Define` 420 pre_set_to_ens = <| 421 dom := set_cat; 422 cod := ens_cat {s | IsSmall s}; 423 map := ��f. TypedGraphFun (explode f.dom,explode f.cod) (��x. f.map ' x) |>`; 424 425val pre_set_to_ens_components = Q.store_thm( 426"pre_set_to_ens_components", 427`(pre_set_to_ens.dom = set_cat) ��� 428 (pre_set_to_ens.cod = ens_cat {s | IsSmall s}) ��� 429 (���f. pre_set_to_ens##f = TypedGraphFun (explode f.dom,explode f.cod) (��x. f.map ' x))`, 430srw_tac [][pre_set_to_ens_def,morf_def]); 431val _ = export_rewrites["pre_set_to_ens_components"]; 432 433val pre_set_to_ens_objf = Q.store_thm( 434"pre_set_to_ens_objf", 435`���x. pre_set_to_ens@@x = explode x`, 436srw_tac [][objf_def] >> 437SELECT_ELIM_TAC >> 438srw_tac [][] >- ( 439 qexists_tac `explode x` >> srw_tac [][] >> 440 srw_tac [][morphism_component_equality] >> 441 srw_tac [][restrict_def,FUN_EQ_THM] >> 442 srw_tac [][GraphFnAp,explode_def]) >> 443pop_assum mp_tac >> 444srw_tac [][EXTENSION,explode_def,morphism_component_equality]); 445val _ = export_rewrites["pre_set_to_ens_objf"]; 446 447val set_to_ens_def = Define` 448 set_to_ens = mk_functor pre_set_to_ens`; 449 450val is_functor_set_to_ens = Q.store_thm( 451"is_functor_set_to_ens", 452`is_functor set_to_ens`, 453srw_tac [][set_to_ens_def] >> 454srw_tac [][functor_axioms_def] >- ( 455 fsrw_tac [][IsTypedFun_def,IsTypedFn_def, 456 HasFunType_def,explode_def,extensional_def] >> 457 metis_tac [InFn] ) 458>- ( 459 qexists_tac `explode x` >> 460 srw_tac [][morphism_component_equality] >> 461 srw_tac [][FUN_EQ_THM,restrict_def] >> 462 srw_tac [][GraphFnAp,explode_def]) >> 463qmatch_abbrev_tac `gf = pg o pf -:ens_cat u` >> 464`pf ���> pg -:ens_cat u` by ( 465 unabbrev_all_tac >> srw_tac [][] >> 466 fsrw_tac [][explode_def,IsTypedFn_def,extensional_def] >> 467 metis_tac [InFn] ) >> 468unabbrev_all_tac >> 469srw_tac [][morphism_component_equality] >> 470srw_tac [][FUN_EQ_THM] >> 471srw_tac [][pre_set_to_ens_def,morf_def,restrict_def,ComposeFun_def] >> 472fsrw_tac [][IsTypedFn_def,explode_def] >> 473metis_tac [InFn,ApComposeFn]); 474val _ = export_rewrites["is_functor_set_to_ens"]; 475 476val set_to_ens_components = Q.store_thm( 477"set_to_ens_components", 478`(set_to_ens.dom = set_cat) ��� 479 (set_to_ens.cod = ens_cat {s | IsSmall s}) ��� 480 (���f. IsTypedFn f ��� (set_to_ens##f = TypedGraphFun (explode f.dom,explode f.cod) (��x. f.map ' x)))`, 481srw_tac [][set_to_ens_def]) 482val _ = export_rewrites["set_to_ens_components"]; 483 484val set_to_ens_objf = Q.store_thm( 485"set_to_ens_objf", 486`���x. set_to_ens@@x = explode x`, 487srw_tac [][set_to_ens_def]); 488val _ = export_rewrites["set_to_ens_objf"]; 489 490val cat_iso_set_to_ens = Q.store_thm( 491"cat_iso_set_to_ens", 492`cat_iso set_to_ens`, 493srw_tac [][cat_iso_bij] >- ( 494 srw_tac [][BIJ_DEF,INJ_DEF,SURJ_DEF,explode_inj] >> 495 metis_tac [explode_implode] ) >> 496srw_tac [][BIJ_DEF,INJ_DEF,SURJ_DEF] >- ( 497 fsrw_tac [][hom_def] >> 498 fsrw_tac [][explode_def,IsTypedFn_def] >> 499 metis_tac [InFn] ) 500>- ( 501 pop_assum mp_tac >> 502 fsrw_tac [][hom_def] >> 503 srw_tac [][TypedGraphFun_Ext,explode_def] >> 504 srw_tac [][morphism_component_equality] >> 505 fsrw_tac [][IsTypedFn_def] >> 506 metis_tac [ExtFn] ) 507>- ( 508 fsrw_tac [][hom_def] >> 509 fsrw_tac [][explode_def,IsTypedFn_def] >> 510 metis_tac [InFn] ) >> 511fsrw_tac [][hom_def] >> 512fsrw_tac [][] >> srw_tac [][] >> 513qexists_tac `TypedGraphFn (a,b) x.map` >> 514conj_asm1_tac >- ( 515 fsrw_tac [][IsTypedFun_def,HasFunType_def,HasFnType_def] >> 516 fsrw_tac [][explode_def] ) >> 517fsrw_tac [][] >> 518srw_tac [][morphism_component_equality] >> 519srw_tac [][FUN_EQ_THM] >> 520fsrw_tac [][HasFnType_def,explode_def,restrict_def] >> 521fsrw_tac [][IsTypedFun_def,HasFunType_def,extensional_def] >> 522srw_tac [][GraphFnAp]); 523 524val _ = overload_on("ens_to_set",``@f. cat_iso_pair set_to_ens f``); 525 526val ens_to_set_dom_cod = Q.store_thm( 527"ens_to_set_dom_cod", 528`(ens_to_set.dom = ens_cat {s | IsSmall s}) ��� 529 (ens_to_set.cod = set_cat)`, 530SELECT_ELIM_TAC >> 531conj_tac >- metis_tac [cat_iso_set_to_ens,cat_iso_def] >> 532metis_tac [cat_iso_pair_def,cat_iso_pair_sym,composable_def,set_to_ens_components]); 533val _ = export_rewrites["ens_to_set_dom_cod"]; 534 535val is_functor_ens_to_set = Q.store_thm( 536"is_functor_ens_to_set", 537`is_functor ens_to_set`, 538SELECT_ELIM_TAC >> 539conj_tac >- metis_tac [cat_iso_set_to_ens,cat_iso_def] >> 540srw_tac [][cat_iso_pair_def]); 541val _ = export_rewrites["is_functor_ens_to_set"]; 542 543val ens_to_set_morf = Q.store_thm( 544"ens_to_set_morf", 545`���f. f ��� (ens_cat {s | IsSmall s}).mor ��� (ens_to_set##f = TypedGraphFn (implode f.dom, implode f.cod) f.map)`, 546srw_tac [][] >> 547SELECT_ELIM_TAC >> 548conj_tac >- metis_tac [cat_iso_set_to_ens,cat_iso_def] >> 549qx_gen_tac `ets` >> strip_tac >> 550fsrw_tac [][cat_iso_pair_bij] >> 551qpat_x_assum `X = ets.dom` (assume_tac o SYM) >> 552fsrw_tac [][] >> 553first_x_assum (qspecl_then [`implode f.dom`,`implode f.cod`] mp_tac) >> 554fsrw_tac [][] >> 555strip_tac >> 556first_x_assum (qspec_then `f` (mp_tac o GSYM)) >> 557`f ��� ens_cat {s | IsSmall s}|f.dom���f.cod|` by ( 558 srw_tac [][hom_def] ) >> 559srw_tac [][] >> 560`���s. IsSmall s ��� (ets@@s = implode s)` by ( 561 srw_tac [][] >> 562 qsuff_tac `set_to_ens@@(LINV (objf set_to_ens) UNIV s)=set_to_ens@@(implode s)` >- ( 563 fsrw_tac [][BIJ_DEF,INJ_DEF] ) >> 564 qmatch_abbrev_tac `q (LINV q u s) = q (implode s)` >> 565 `q (implode s) = s` by srw_tac [][Abbr`q`] >> 566 pop_assum mp_tac >> simp_tac (srw_ss()) [] >> strip_tac >> 567 match_mp_tac (MP_CANON BIJ_LINV_INV) >> 568 srw_tac [][Abbr`q`,Abbr`u`] >> 569 qexists_tac `{s | IsSmall s}` >> srw_tac [][] ) >> 570`ets##f :- implode f.dom ��� implode f.cod -:set_cat` by ( 571 match_mp_tac morf_maps_to >> 572 map_every qexists_tac [`ets.dom`,`f.dom`,`f.cod`] >> 573 fsrw_tac [][] ) >> 574qmatch_abbrev_tac `a = b` >> 575`a ��� set_cat|implode f.dom���implode f.cod|` by ( 576 fsrw_tac [][hom_def] >> 577 qpat_x_assum `ets##f = a` assume_tac >> 578 fsrw_tac [][] ) >> 579`b ��� set_cat|implode f.dom���implode f.cod|` by ( 580 fsrw_tac [][Abbr`b`,hom_def] >> 581 fsrw_tac [][IsTypedFun_def,HasFunType_def,HasFnType_def] ) >> 582qsuff_tac `set_to_ens##a=set_to_ens##b` >- ( 583 fsrw_tac [][BIJ_DEF,INJ_DEF] ) >> 584unabbrev_all_tac >> 585qmatch_abbrev_tac `q (LINV q h f) = q z` >> 586`q z = f` by ( 587 qunabbrev_tac `q` >> 588 `IsTypedFn z` by ( 589 unabbrev_all_tac >> 590 srw_tac [][] >> 591 srw_tac [][HasFnType_def] >> 592 fsrw_tac [][IsTypedFun_def,HasFunType_def] ) >> 593 srw_tac [][Abbr`z`,morphism_component_equality] >> 594 fsrw_tac [][IsTypedFun_def,HasFunType_def,extensional_def] >> 595 srw_tac [][restrict_def,FUN_EQ_THM] >> 596 srw_tac [][GraphFnAp] ) >> 597fsrw_tac [][] >> 598match_mp_tac (MP_CANON BIJ_LINV_INV) >> 599unabbrev_all_tac >> 600qexists_tac `ens_cat {s | IsSmall s}|f.dom���f.cod|` >> 601srw_tac [][]); 602val _ = export_rewrites["ens_to_set_morf"]; 603 604val ens_to_set_objf = Q.store_thm( 605"ens_to_set_objf", 606`���s. IsSmall s ��� (ens_to_set@@s = implode s)`, 607srw_tac [][objf_def] >> 608SELECT_ELIM_TAC >> 609conj_tac >- ( 610 qexists_tac `implode s` >> 611 srw_tac [][morphism_component_equality] >> 612 match_mp_tac GraphFnExt >> 613 srw_tac [][restrict_def] ) >> 614srw_tac [][morphism_component_equality]); 615val _ = export_rewrites["ens_to_set_objf"]; 616 617val cat_iso_ens_to_set = Q.store_thm( 618"cat_iso_ens_to_set", 619`cat_iso ens_to_set`, 620SELECT_ELIM_TAC >> 621metis_tac [cat_iso_pair_sym,cat_iso_set_to_ens,cat_iso_def]); 622val _ = export_rewrites["cat_iso_ens_to_set"]; 623 624val is_locally_small_def = Define` 625 is_locally_small c = ���s. s ��� homs c ��� IsSmall s`; 626 627val _ = overload_on("is_lscat",``��c. is_category c ��� is_locally_small c``); 628 629val pre_rep_functor_def = Define` 630 pre_rep_functor u = <| 631 dom := ens_cat u ; 632 cod := ens_cat {s | IsSmall s} ; 633 map := ��f. TypedGraphFun (explode (zfrep f.dom), explode (zfrep f.cod)) (��z. zfel f.cod (f.map (elzf f.dom z))) 634 |>`; 635 636val pre_rep_functor_components = Q.store_thm( 637"pre_rep_functor_components", 638`���u. ((pre_rep_functor u).dom = ens_cat u) ��� 639 ((pre_rep_functor u).cod = ens_cat {s | IsSmall s}) ��� 640 (���f. ((pre_rep_functor u)##f = TypedGraphFun (explode (zfrep f.dom), explode (zfrep f.cod)) (��z. zfel f.cod (f.map (elzf f.dom z)))))`, 641srw_tac [][pre_rep_functor_def,morf_def]); 642val _ = export_rewrites["pre_rep_functor_components"]; 643 644val pre_rep_functor_objf = Q.store_thm( 645"pre_rep_functor_objf", 646`���u x. IsSmall x ��� x ��� u ��� ((pre_rep_functor u)@@x = explode (zfrep x))`, 647srw_tac [][objf_def] >> 648SELECT_ELIM_TAC >> 649conj_tac >- ( 650 qexists_tac `explode (zfrep x)` >> 651 fsrw_tac [][] >> 652 fsrw_tac [][TypedGraphFun_Ext] >> 653 srw_tac [][restrict_def,explode_def,zfel_elzf] >> 654 pop_assum mp_tac >> srw_tac [][In_zfrep_thm] >> 655 metis_tac [elzf_zfel] ) >> 656qx_gen_tac `s` >> 657srw_tac [][] >> 658pop_assum mp_tac >> srw_tac [][TypedGraphFun_Ext]); 659val _ = export_rewrites["pre_rep_functor_objf"]; 660 661val rep_functor_def = Define` 662 rep_functor u = mk_functor (pre_rep_functor u)`; 663 664val is_functor_rep_functor = Q.store_thm( 665"is_functor_rep_functor", 666`���u. (���s. s ��� u ��� IsSmall s) ��� is_functor (rep_functor u)`, 667srw_tac [][rep_functor_def] >> 668fsrw_tac [][functor_axioms_def] >> 669conj_tac >- ( 670 fsrw_tac [][explode_def] >> 671 fsrw_tac [DNF_ss][In_zfrep_thm] >> 672 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 673 metis_tac [] ) >> 674conj_tac >- ( 675 qx_gen_tac `s` >> strip_tac >> 676 qexists_tac `explode (zfrep s)` >> 677 fsrw_tac [][TypedGraphFun_Ext] >> 678 fsrw_tac [][explode_def] >> 679 fsrw_tac [DNF_ss][In_zfrep_thm,restrict_def] ) >> 680map_every qx_gen_tac [`f`,`g`] >> strip_tac >> 681qmatch_abbrev_tac `ff = gg o hh -:ens_cat uu` >> 682`hh ���> gg -:ens_cat uu` by ( 683 unabbrev_all_tac >> 684 fsrw_tac [][] >> 685 fsrw_tac [DNF_ss][explode_def,In_zfrep_thm] >> 686 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 687 metis_tac [] >> 688 metis_tac [] ) >> 689srw_tac [][] >> 690unabbrev_all_tac >> 691fsrw_tac [][morphism_component_equality] >> 692fsrw_tac [][ComposeFun_def] >> 693fsrw_tac [][restrict_def,explode_def] >> 694srw_tac [][FUN_EQ_THM] >> 695fsrw_tac [][IsTypedFun_def,HasFunType_def,In_zfrep_thm] >> 696srw_tac [][] >> 697res_tac >> 698fsrw_tac [][In_zfrep_thm]); 699 700val rep_functor_dom_cod = Q.store_thm( 701"rep_functor_dom_cod", 702`���u. ((rep_functor u).dom = ens_cat u) ��� 703 ((rep_functor u).cod = ens_cat {s | IsSmall s})`, 704srw_tac [][rep_functor_def]) 705val _ = export_rewrites["rep_functor_dom_cod"]; 706 707val rep_functor_morf = Q.store_thm( 708"rep_functor_morf", 709`���u f. f ��� (ens_cat u).mor ��� ((rep_functor u)##f = 710TypedGraphFun (explode (zfrep f.dom), explode (zfrep f.cod)) (��z. zfel f.cod (f.map (elzf f.dom z))))`, 711srw_tac [][rep_functor_def]); 712val _ = export_rewrites["rep_functor_morf"]; 713 714val rep_functor_objf = Q.store_thm( 715"rep_functor_objf", 716`���u x. IsSmall x ��� x ��� u ��� (rep_functor u@@x = explode (zfrep x))`, 717srw_tac [][rep_functor_def]); 718val _ = export_rewrites["rep_functor_objf"]; 719 720val rep_functor_embedding = Q.store_thm( 721"rep_functor_embedding", 722`���u. (���s. s ��� u ��� IsSmall s) ��� embedding (rep_functor u)`, 723srw_tac [][embedding_def,full_def,faithful_def] >- ( 724 qmatch_abbrev_tac `X` >> 725 qpat_x_assum `a ��� u` assume_tac >> 726 qpat_x_assum `b ��� u` assume_tac >> 727 res_tac >> fsrw_tac [][] >> 728 qpat_x_assum `IsTypedFun h` mp_tac >> 729 asm_simp_tac (srw_ss()) [IsTypedFun_def] >> 730 asm_simp_tac (srw_ss()++DNF_ss) [HasFunType_def,explode_def,In_zfrep_thm] >> 731 srw_tac [][GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM] >> 732 qunabbrev_tac `X` >> 733 qexists_tac `TypedGraphFun (a,b) f` >> 734 fsrw_tac [][morphism_component_equality] >> 735 srw_tac [][restrict_def] >> 736 srw_tac [][FUN_EQ_THM] >> 737 fsrw_tac [][extensional_def] >> 738 fsrw_tac [][explode_def] >> 739 fsrw_tac [][In_zfrep_thm] >> 740 srw_tac [][] >> fsrw_tac [][] >> 741 metis_tac [elzf_zfel] ) >> 742`g ��� (ens_cat u).mor ��� h ��� (ens_cat u).mor` by ( 743 fsrw_tac [][] ) >> 744fsrw_tac [][TypedGraphFun_Ext,explode_def,IsTypedFun_def,HasFunType_def] >> 745srw_tac [][] >> 746srw_tac [][morphism_component_equality] >> 747fsrw_tac [][extensional_def] >> 748srw_tac [][FUN_EQ_THM] >> 749reverse (Cases_on `x ��� g.dom`) >- metis_tac [] >> 750res_tac >> fsrw_tac [DNF_ss][In_zfrep_thm] >> 751`zfel g.cod (g.map x) = zfel g.cod (h.map (elzf g.dom (zfel g.dom x)))` by metis_tac [] >> 752qpat_x_assum `IsSmall g.dom` assume_tac >> 753qpat_x_assum `x ��� g.dom` assume_tac >> 754fsrw_tac [][elzf_zfel] >> 755`elzf g.cod (zfel g.cod (g.map x)) = elzf g.cod (zfel g.cod (h.map x))` by metis_tac [] >> 756qpat_x_assum `IsSmall g.cod` assume_tac >> 757`g.map x ��� g.cod ��� h.map x ��� g.cod` by metis_tac [] >> 758qpat_x_assum `g.map x ��� g.cod` assume_tac >> 759fsrw_tac [][elzf_zfel]); 760 761(* 762val rep_functor_inj_obj = Q.store_thm( 763"rep_functor_inj_obj", 764`���u. (���s. s ��� u ��� IsSmall s) ��� inj_obj (rep_functor u)`, 765srw_tac [][inj_obj_def] >> 766pop_assum mp_tac >> srw_tac [][] >> 767imp_res_tac explode_inj >> 768match_mp_tac the_zfrep_inj >> 769fsrw_tac [][PAIR_FST_SND_EQ] >> 770srw_tac [][FUN_EQ_THM] >> 771WOULD NEED zfrep TO BE INJECTIVE 772*) 773 774(* 775val rep_functor_not_inj_obj = Q.store_thm( 776"rep_functor_not_inj_obj", 777`let u = POW (UNIV:zfset set) in 778 (���s. s ��� u ��� IsSmall s) ��� 779 ��inj_obj (rep_functor u)`, 780srw_tac [][LET_THM,IN_POW] 781*) 782 783val is_self_hom_def = Define` 784 is_self_hom c h = ���x. x ��� c.obj ��� (h = c|x���x|)`; 785 786val hom_tag_def = Define` 787 hom_tag c h = if is_self_hom c h then {{{}}} else ({{}}:zfset)`; 788 789val the_hom_tag_def = Define` 790 the_hom_tag c h = if is_self_hom c h then {{}} else Empty`; 791 792val hom_tag_not_empty = Q.store_thm( 793"hom_tag_not_empty", 794`���c x. hom_tag c x <> {}`, 795srw_tac [][hom_tag_def] >> 796metis_tac [NotEmpty,InSing]); 797val _ = export_rewrites["hom_tag_not_empty"]; 798 799val the_hom_tag_in_hom_tag = Q.store_thm( 800"the_hom_tag_in_hom_tag", 801`���c h. the_hom_tag c h In hom_tag c h`, 802srw_tac [][hom_tag_def,the_hom_tag_def,InSing]); 803val _ = export_rewrites["the_hom_tag_in_hom_tag"]; 804 805val In_hom_tag = Q.store_thm( 806"In_hom_tag", 807`���x c h. x In hom_tag c h = (x = the_hom_tag c h)`, 808srw_tac [][EQ_IMP_THM] >> 809fsrw_tac [][hom_tag_def,the_hom_tag_def] >> 810Cases_on `is_self_hom c h` >> fsrw_tac [][InSing]); 811val _ = export_rewrites["In_hom_tag"]; 812 813val tagged_homset_def = Define` 814 tagged_homset c h = (hom_tag c h) # (ens_to_set@@((rep_functor (homs c))@@h))`; 815 816val tag_fun_def = Define` 817 tag_fun c f x = Pair (the_hom_tag c f.cod) 818 ((ens_to_set##((rep_functor (homs c))##f)).map ' (Snd x))`; 819 820val HasFnType_tag_fun = Q.store_thm( 821"HasFnType_tag_fun", 822`���c f a b. f ��� (ens_cat (homs c)).mor ��� is_lscat c ��� (a = tagged_homset c f.dom) ��� (b = tagged_homset c f.cod) ��� 823 HasFnType (tag_fun c f) a b`, 824srw_tac [][HasFnType_def] >> 825srw_tac [][tagged_homset_def,InProdEq] >> 826fsrw_tac [][tag_fun_def,PairEq] >> 827`IsSmall f.cod` by ( fsrw_tac [][is_locally_small_def] ) >> 828srw_tac [][In_zfrep_thm] >> 829fsrw_tac [][tagged_homset_def,InProdEq,Snd] >> 830`IsSmall f.dom` by ( fsrw_tac [][is_locally_small_def] ) >> 831qpat_x_assum `x2 In X` mp_tac >> 832srw_tac [][In_zfrep_thm] >> 833qexists_tac `f.map x` >> 834fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 835qmatch_abbrev_tac `(ens_to_set##gg).map ' A = B` >> 836`gg ��� (ens_cat {s | IsSmall s}).mor` by ( 837 srw_tac [][Abbr`gg`] >> 838 pop_assum mp_tac >> 839 fsrw_tac [][explode_def,In_zfrep_thm] >> 840 fsrw_tac [][is_locally_small_def] >> 841 metis_tac [elzf_zfel] ) >> 842srw_tac [][] >> 843`A ��� explode (zfrep f.dom)` by ( 844 srw_tac [][explode_def,In_zfrep_thm,Abbr`A`] >> 845 metis_tac [] ) >> 846`A In (implode gg.dom)` by ( 847 srw_tac [][In_implode,Abbr`gg`] ) >> 848srw_tac [][GraphFnAp] >> 849srw_tac [][Abbr`gg`,restrict_def] >> 850srw_tac [][Abbr`A`,elzf_zfel]); 851 852val tag_fun_comp = Q.store_thm( 853"tag_fun_comp", 854`���c f g x. is_lscat c ��� (f ���> g -:(ens_cat (homs c))) ��� (x In tagged_homset c f.dom) 855��� (tag_fun c (g o f) x = tag_fun c g (tag_fun c f x))`, 856srw_tac [][] >> 857`IsSmall f.dom ��� IsSmall f.cod ��� IsSmall g.dom ��� IsSmall g.cod` by ( 858 fsrw_tac [][is_locally_small_def] ) >> 859full_simp_tac std_ss [tag_fun_def,PairEq,Snd,ComposeTypedFun_components,composable_def] >> 860`ens_to_set##(rep_functor (homs c)##f) ���> ens_to_set##(rep_functor (homs c)##g) -:ens_to_set.cod` by ( 861 match_mp_tac morf_composable >> 862 srw_tac [][] >> 863 pop_assum mp_tac >> 864 srw_tac [][explode_def,In_zfrep_thm] >> 865 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 866 metis_tac [] ) >> 867`(g o f) ��� (ens_cat (homs c)).mor` by ( 868 srw_tac [][] >> fsrw_tac [][IsTypedFun_def] ) >> 869qmatch_abbrev_tac `(ens_to_set##ff).map ' Snd x = (ens_to_set##gg).map ' ((ens_to_set##hh).map ' Snd x)` >> 870`(ff.dom = hh.dom) ��� (ff.cod = gg.cod)` by ( 871 unabbrev_all_tac >> srw_tac [][] ) >> 872`ff ��� (ens_cat {s | IsSmall s}).mor ��� 873 hh ��� (ens_cat {s | IsSmall s}).mor ��� 874 gg ��� (ens_cat {s | IsSmall s}).mor` by ( 875 unabbrev_all_tac >> fsrw_tac [][] >> 876 srw_tac [][explode_def,In_zfrep_thm] >> 877 fsrw_tac [][IsTypedFun_def,HasFunType_def,ComposeFun_def,restrict_def] >> 878 metis_tac [elzf_zfel] ) >> 879`Snd x ��� explode (zfrep f.dom)` by ( 880 fsrw_tac [][tagged_homset_def,InProdEq,Snd] >> 881 qpat_x_assum `f.dom ��� homs c` assume_tac >> 882 fsrw_tac [][] >> 883 srw_tac [][explode_def] ) >> 884`(ens_to_set##gg).map ' ((ens_to_set##hh).map ' Snd x) = 885 ((ens_to_set##gg) |o| (ens_to_set##hh)).map ' Snd x` by ( 886 fsrw_tac [][composable_in_def] >> 887 fsrw_tac [][ComposeGraphFns] >> 888 `Snd x In (implode hh.dom)` by ( 889 srw_tac [][In_implode,Abbr`hh`] ) >> 890 srw_tac [][GraphFnAp] >> 891 `hh.map (Snd x) In (implode gg.dom)` by ( 892 fsrw_tac [][HasFnType_def] >> 893 metis_tac [In_implode] ) >> 894 fsrw_tac [][GraphFnAp] ) >> 895full_simp_tac std_ss [] >> 896AP_THM_TAC >> AP_TERM_TAC >> AP_TERM_TAC >> 897unabbrev_all_tac >> 898qmatch_abbrev_tac `f1##(f2##gof) = (f1##(f2##g)) |o| (f1##(f2##f))` >> 899`f1##(f2##gof) = (f1 ��� f2)##gof` by ( 900 match_mp_tac (GSYM functor_comp_morf) >> 901 unabbrev_all_tac >> srw_tac [][] ) >> 902`f1##(f2##g) = (f1 ��� f2)##g` by ( 903 match_mp_tac (GSYM functor_comp_morf) >> 904 unabbrev_all_tac >> srw_tac [][] ) >> 905`f1##(f2##f) = (f1 ��� f2)##f` by ( 906 match_mp_tac (GSYM functor_comp_morf) >> 907 unabbrev_all_tac >> srw_tac [][] ) >> 908fsrw_tac [][Abbr`gof`] >> 909Q.ISPECL_THEN [`f1 ��� f2`,`(f1 ��� f2).dom`,`(f1 ��� f2).cod`,`f`,`g`] mp_tac morf_comp >> 910fsrw_tac [][] >> 911`is_functor (f1 ��� f2)` by ( 912 unabbrev_all_tac >> 913 match_mp_tac is_functor_comp >> 914 srw_tac [][] >> 915 fsrw_tac [][is_locally_small_def] >> 916 match_mp_tac is_functor_rep_functor >> 917 srw_tac [][] ) >> 918fsrw_tac [][] >> 919`f2 ���> f1` by ( 920 unabbrev_all_tac >> srw_tac [][] ) >> 921fsrw_tac [][] >> 922`f ���> g -:f2.dom` by ( 923 unabbrev_all_tac >> srw_tac [][] ) >> 924fsrw_tac [][] >> 925`g o f -:f2.dom = g o f` by ( 926 unabbrev_all_tac >> srw_tac [][] ) >> 927fsrw_tac [][] >> 928`f1.cod = set_cat` by srw_tac [][Abbr`f1`] >> 929fsrw_tac [][]); 930 931val pre_tag_functor_def = Define` 932 pre_tag_functor c = <| 933 dom := ens_cat (homs c); 934 cod := set_cat ; 935 map := ��f. TypedGraphFn (tagged_homset c f.dom, tagged_homset c f.cod) (tag_fun c f) |>`; 936 937val pre_tag_functor_dom_cod = Q.store_thm( 938"pre_tag_functor_dom_cod", 939`���c. ((pre_tag_functor c).dom = ens_cat (homs c)) ��� 940 ((pre_tag_functor c).cod = set_cat)`, 941srw_tac [][pre_tag_functor_def]); 942val _ = export_rewrites["pre_tag_functor_dom_cod"]; 943 944val pre_tag_functor_morf = Q.store_thm( 945"pre_tag_functor_morf", 946`���c f. (pre_tag_functor c)##f = TypedGraphFn (tagged_homset c f.dom, tagged_homset c f.cod) (tag_fun c f)`, 947srw_tac [][pre_tag_functor_def,morf_def]); 948val _ = export_rewrites["pre_tag_functor_morf"]; 949 950val pre_tag_functor_objf = Q.store_thm( 951"pre_tag_functor_objf", 952`���c x. is_lscat c ��� x ��� homs c ��� ((pre_tag_functor c)@@x = tagged_homset c x)`, 953srw_tac [][objf_def] >> 954SELECT_ELIM_TAC >> 955conj_tac >- ( 956 qexists_tac `tagged_homset c x` >> 957 srw_tac [][morphism_component_equality] >> 958 match_mp_tac GraphFnExt >> 959 fsrw_tac [DNF_ss][tag_fun_def,tagged_homset_def,InProdEq] >> 960 rpt strip_tac >> 961 fsrw_tac [][PairEq] >> 962 fsrw_tac [][Snd] >> 963 qmatch_abbrev_tac `(ens_to_set##f).map ' x2 = x2` >> 964 `IsSmall x` by ( 965 fsrw_tac [][is_locally_small_def] ) >> 966 `f ��� (ens_cat {s | IsSmall s}).mor` by ( 967 srw_tac [][Abbr`f`] >> 968 qpat_x_assum `IsSmall x` assume_tac >> 969 fsrw_tac [][explode_def,In_zfrep_thm] >> 970 srw_tac [][restrict_def] >> 971 metis_tac [] ) >> 972 srw_tac [][] >> 973 qpat_x_assum `x ��� homs c` assume_tac >> 974 `x2 In implode f.dom` by ( 975 fsrw_tac [][Abbr`f`,explode_def] ) >> 976 fsrw_tac [][GraphFnAp,Abbr`f`] >> 977 srw_tac [][restrict_def] >> 978 fsrw_tac [][In_zfrep_thm,explode_def] >> 979 qpat_x_assum `x2 In zfrep x` mp_tac >> 980 srw_tac [][In_zfrep_thm] >> 981 metis_tac [elzf_zfel] ) >> 982srw_tac [][morphism_component_equality]); 983val _ = export_rewrites["pre_tag_functor_objf"]; 984 985val tag_functor_def = Define` 986 tag_functor c = mk_functor (pre_tag_functor c)`; 987 988val is_functor_tag_functor = Q.store_thm( 989"is_functor_tag_functor", 990`���c. is_lscat c ��� is_functor (tag_functor c)`, 991srw_tac [][tag_functor_def] >> 992fsrw_tac [][functor_axioms_def] >> 993conj_tac >- ( 994 srw_tac [][] >> 995 match_mp_tac HasFnType_tag_fun >> 996 srw_tac [][] ) >> 997conj_tac >- ( 998 srw_tac [][morphism_component_equality] >> 999 match_mp_tac GraphFnExt >> 1000 fsrw_tac [DNF_ss][tag_fun_def,tagged_homset_def,InProdEq] >> 1001 rpt strip_tac >> 1002 fsrw_tac [][PairEq] >> 1003 fsrw_tac [][Snd] >> 1004 qmatch_abbrev_tac `(ens_to_set##f).map ' x2 = x2` >> 1005 `IsSmall x` by ( 1006 fsrw_tac [][is_locally_small_def] ) >> 1007 `f ��� (ens_cat {s | IsSmall s}).mor` by ( 1008 srw_tac [][Abbr`f`] >> 1009 qpat_x_assum `IsSmall x` assume_tac >> 1010 fsrw_tac [][explode_def,In_zfrep_thm] >> 1011 srw_tac [][restrict_def] >> 1012 metis_tac [] ) >> 1013 srw_tac [][] >> 1014 qpat_x_assum `x ��� homs c` assume_tac >> 1015 `x2 In implode f.dom` by ( 1016 fsrw_tac [][Abbr`f`,explode_def] ) >> 1017 fsrw_tac [][GraphFnAp,Abbr`f`] >> 1018 srw_tac [][restrict_def] >> 1019 fsrw_tac [][In_zfrep_thm,explode_def] >> 1020 qpat_x_assum `x2 In zfrep x` mp_tac >> 1021 srw_tac [][In_zfrep_thm] >> 1022 metis_tac [elzf_zfel] ) >> 1023srw_tac [][] >> 1024qmatch_abbrev_tac `ff = gg o hh -:set_cat` >> 1025`hh ���> gg -:set_cat` by ( 1026 srw_tac [][Abbr`hh`,Abbr`gg`] >> 1027 srw_tac [][HasFnType_tag_fun] ) >> 1028srw_tac [][Abbr`ff`,Abbr`gg`,Abbr`hh`,morphism_component_equality] >> 1029qmatch_abbrev_tac `ff = ComposeFn (X,Y,Z) (GraphFn Y gg) (GraphFn X hh)` >> 1030`HasFnType hh X Y ��� HasFnType gg Y Z` by ( 1031 srw_tac [][Abbr`gg`,Abbr`hh`,HasFnType_tag_fun] ) >> 1032srw_tac [][ComposeGraphFns,Abbr`ff`] >> 1033match_mp_tac GraphFnExt >> 1034srw_tac [][Abbr`gg`,Abbr`hh`] >> 1035match_mp_tac tag_fun_comp >> 1036unabbrev_all_tac >> 1037srw_tac [][]); 1038val _ = export_rewrites["is_functor_tag_functor"]; 1039 1040val tag_functor_dom_cod = Q.store_thm( 1041"tag_functor_dom_cod", 1042`���c. ((tag_functor c).dom = ens_cat (homs c)) ��� 1043 ((tag_functor c).cod = set_cat)`, 1044srw_tac [][tag_functor_def]); 1045val _ = export_rewrites["tag_functor_dom_cod"]; 1046 1047val tag_functor_morf = Q.store_thm( 1048"tag_functor_morf", 1049`���c f. f ��� (ens_cat (homs c)).mor ��� ((tag_functor c)##f = TypedGraphFn (tagged_homset c f.dom, tagged_homset c f.cod) (tag_fun c f))`, 1050srw_tac [][tag_functor_def]); 1051val _ = export_rewrites["tag_functor_morf"]; 1052 1053val tag_functor_objf = Q.store_thm( 1054"tag_functor_objf", 1055`���c x. is_lscat c ��� x ��� homs c ��� (tag_functor c@@x = tagged_homset c x)`, 1056srw_tac [][tag_functor_def]); 1057val _ = export_rewrites["tag_functor_objf"]; 1058 1059val tag_functor_embedding = Q.store_thm( 1060"tag_functor_embedding", 1061`���c. is_lscat c ��� embedding (tag_functor c)`, 1062srw_tac [][] >> 1063`embedding (ens_to_set ��� (rep_functor (homs c)))` by ( 1064 match_mp_tac embedding_functor_comp >> 1065 fsrw_tac [][is_locally_small_def] >> 1066 conj_tac >- ( 1067 match_mp_tac is_functor_rep_functor >> 1068 srw_tac [][] ) >> 1069 match_mp_tac rep_functor_embedding >> 1070 srw_tac [][]) >> 1071fsrw_tac [][embedding_def] >> 1072conj_tac >- ( 1073 fsrw_tac [][full_def] >> 1074 map_every qx_gen_tac [`h`,`a`,`b`] >> 1075 strip_tac >> 1076 rpt (qpat_x_assum `X = tag_functor c@@Y` mp_tac) >> 1077 srw_tac [][] >> 1078 qabbrev_tac `hhdom = (ens_to_set ��� rep_functor (homs c))@@a` >> 1079 qabbrev_tac `hhcod = (ens_to_set ��� rep_functor (homs c))@@b` >> 1080 qabbrev_tac `hh = TypedGraphFn (hhdom,hhcod) (��x. Snd (h.map ' (Pair (the_hom_tag c a) x)))` >> 1081 `IsSmall a ��� IsSmall b` by fsrw_tac [][is_locally_small_def] >> 1082 `is_functor (rep_functor (homs c))` by ( 1083 match_mp_tac is_functor_rep_functor >> 1084 fsrw_tac [][is_locally_small_def] ) >> 1085 `IsTypedFn hh` by ( 1086 srw_tac [][Abbr`hh`] >> 1087 rpt (qpat_x_assum `xxx = tagged_homset c yyy` mp_tac) >> 1088 fsrw_tac [][IsTypedFn_def,tagged_homset_def] >> 1089 fsrw_tac [][HasFnType_def,Abbr`hhdom`,Abbr`hhcod`] >> 1090 srw_tac [][] >> 1091 `h.map ' Pair (the_hom_tag c a) x In ((hom_tag c b) # (zfrep b))` by ( 1092 match_mp_tac InFn >> 1093 qexists_tac `h.dom` >> 1094 fsrw_tac [][] >> 1095 srw_tac [][GSYM InProd] ) >> 1096 fsrw_tac [][InProdEq,Snd] ) >> 1097 first_x_assum (qspecl_then [`hh`,`a`,`b`] mp_tac) >> 1098 fsrw_tac [][Abbr`hh`] >> 1099 strip_tac >> 1100 qexists_tac `g` >> 1101 srw_tac [][morphism_component_equality] >> 1102 pop_assum mp_tac >> srw_tac [][] >> 1103 qmatch_assum_abbrev_tac `(ens_to_set##ff=yy)` >> 1104 `ff ��� (ens_cat {s | IsSmall s}).mor` by ( 1105 srw_tac [][Abbr`ff`] >> 1106 fsrw_tac [][explode_def,Abbr`hhdom`,Abbr`hhcod`] >> 1107 pop_assum mp_tac >> 1108 srw_tac [][In_zfrep_thm] >> 1109 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 1110 metis_tac [] ) >> 1111 fsrw_tac [][] >> 1112 unabbrev_all_tac >> 1113 fsrw_tac [][morphism_component_equality] >> 1114 match_mp_tac FnEqThm >> 1115 map_every qexists_tac [`h.dom`,`h.cod`] >> 1116 fsrw_tac [][IsTypedFn_def] >> 1117 conj_tac >- ( 1118 match_mp_tac GraphFnType >> 1119 match_mp_tac HasFnType_tag_fun >> 1120 fsrw_tac [][] ) >> 1121 srw_tac [][tagged_homset_def,GraphFnAp] >> 1122 srw_tac [][tag_fun_def] >> 1123 `h.map ' x In tagged_homset c g.cod` by ( 1124 match_mp_tac InFn >> 1125 fsrw_tac [][tagged_homset_def] >> 1126 metis_tac [] ) >> 1127 pop_assum mp_tac >> 1128 srw_tac [][InProdEq,tagged_homset_def] >> 1129 fsrw_tac [][PairEq] >> 1130 fsrw_tac [][InProdEq,Snd] >> 1131 srw_tac [][GraphFnAp,Snd] ) >> 1132fsrw_tac [][faithful_def] >> 1133srw_tac [][] >> 1134first_x_assum match_mp_tac >> 1135srw_tac [][] >> 1136qmatch_abbrev_tac `ens_to_set##f1 = ens_to_set##f2` >> 1137`IsSmall g.dom ��� IsSmall g.cod` by fsrw_tac [][is_locally_small_def] >> 1138`f1 ��� (ens_cat {s | IsSmall s}).mor` by ( 1139 srw_tac [][Abbr`f1`] >> 1140 rpt (qpat_x_assum `IsSmall X` mp_tac) >> 1141 rpt strip_tac >> 1142 fsrw_tac [][explode_def,In_zfrep_thm] >> 1143 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 1144 metis_tac [] ) >> 1145`f2 ��� (ens_cat {s | IsSmall s}).mor` by ( 1146 srw_tac [][Abbr`f2`] >> 1147 rpt (qpat_x_assum `IsSmall X` mp_tac) >> 1148 rpt strip_tac >> 1149 fsrw_tac [][explode_def,In_zfrep_thm] >> 1150 fsrw_tac [][IsTypedFun_def,HasFunType_def] >> 1151 metis_tac [] ) >> 1152srw_tac [][] >> 1153srw_tac [][Abbr`f1`,Abbr`f2`,morphism_component_equality] >> 1154match_mp_tac GraphFnExt >> 1155srw_tac [][In_zfrep_thm] >> 1156srw_tac [][restrict_def] >> 1157`g ��� (ens_cat (homs c)).mor` by srw_tac [][] >> 1158`h ��� (ens_cat (homs c)).mor` by srw_tac [][] >> 1159fsrw_tac [][morphism_component_equality] >> 1160qmatch_rename_tac `zfel g.cod (g.map z) = zfel g.cod (h.map z)` >> 1161`GraphFn (tagged_homset c g.dom) (tag_fun c g) ' (Pair (the_hom_tag c g.dom) (zfel g.dom z)) = 1162 GraphFn (tagged_homset c h.dom) (tag_fun c h) ' (Pair (the_hom_tag c h.dom) (zfel h.dom z))` 1163by metis_tac [] >> 1164qpat_x_assum `GraphFn X Y = Z` (K ALL_TAC) >> 1165qmatch_assum_abbrev_tac `GraphFn X f1 ' p1 = GraphFn X2 f2 ' p2` >> 1166`p1 In X` by ( 1167 unabbrev_all_tac >> 1168 srw_tac [][tagged_homset_def,InProdEq,In_zfrep_thm,PairEq] >> 1169 metis_tac [] ) >> 1170`p2 In X2` by ( 1171 unabbrev_all_tac >> 1172 srw_tac [][tagged_homset_def,InProdEq,In_zfrep_thm,PairEq] >> 1173 metis_tac [] ) >> 1174fsrw_tac [][GraphFnAp] >> 1175unabbrev_all_tac >> 1176fsrw_tac [][tag_fun_def,PairEq,Snd] >> 1177qpat_x_assum `X ' w = Y ' w2` mp_tac >> 1178fsrw_tac [][] >> 1179`zfel g.dom z In zfrep g.dom` by ( 1180 fsrw_tac [][explode_def,In_zfrep_thm] ) >> 1181fsrw_tac [][GraphFnAp,restrict_def]) 1182val _ = export_rewrites["tag_functor_embedding"]; 1183 1184val zYfunctor_def = Define` 1185 zYfunctor c = (postcomp_functor (c��) (tag_functor c)) ��� Yfunctor c` 1186 1187val is_functor_zYfunctor = Q.store_thm( 1188"is_functor_zYfunctor", 1189`���c. is_lscat c ��� is_functor (zYfunctor c)`, 1190srw_tac [][] >> 1191fsrw_tac [][zYfunctor_def] >> 1192match_mp_tac is_functor_comp >> 1193conj_tac >- srw_tac [][is_functor_Yfunctor] >> 1194conj_tac >- ( 1195 match_mp_tac is_functor_postcomp_functor >> 1196 srw_tac [][] ) >> 1197srw_tac [][]); 1198val _ = export_rewrites["is_functor_zYfunctor"]; 1199 1200val zYfunctor_dom_cod = Q.store_thm( 1201"zYfunctor_dom_cod", 1202`���c. ((zYfunctor c).dom = c) ��� 1203 ((zYfunctor c).cod = [(c��)���set_cat])`, 1204srw_tac [][zYfunctor_def]); 1205val _ = export_rewrites["zYfunctor_dom_cod"]; 1206 1207val zYfunctorEmbedding = Q.store_thm( 1208"zYfunctorEmbedding", 1209`���c. is_lscat c ��� embedding (zYfunctor c)`, 1210srw_tac [][zYfunctor_def] >> 1211match_mp_tac embedding_functor_comp >> 1212fsrw_tac [][is_functor_Yfunctor,YonedaEmbedding] >> 1213match_mp_tac embedding_functor_cats >> 1214srw_tac [][]); 1215 1216val zYfunctorInjObj = Q.store_thm( 1217"zYfunctorInjObj", 1218`���c. is_lscat c ��� inj_obj (zYfunctor c)`, 1219srw_tac [][zYfunctor_def] >> 1220srw_tac [][inj_obj_def] >> 1221qmatch_assum_abbrev_tac `(f ��� g)@@a = (f ��� g)@@b` >> 1222`is_functor f ��� is_functor g ��� (g ���> f) ��� a ��� g.dom.obj ��� b ��� g.dom.obj` by ( 1223 unabbrev_all_tac >> fsrw_tac [][is_functor_Yfunctor] ) >> 1224qpat_x_assum `is_category c` assume_tac >> 1225fsrw_tac [][Abbr`g`,Yfunctor_objf] >> 1226`(c|_���a|) ��� [(c��)���(tag_functor c).dom].obj` by ( 1227 srw_tac [][] ) >> 1228`(c|_���b|) ��� [(c��)���(tag_functor c).dom].obj` by ( 1229 srw_tac [][] ) >> 1230`is_functor (tag_functor c)` by srw_tac [][] >> 1231full_simp_tac std_ss [Abbr`f`,is_category_op_cat,postcomp_functor_objf] >> 1232`(tag_functor c ��� (c|_���a|))@@a = (tag_functor c ��� (c|_���b|))@@a` by metis_tac [] >> 1233qpat_x_assum `tag_functor c ��� X = Y` (K ALL_TAC) >> 1234pop_assum mp_tac >> srw_tac [][tagged_homset_def,ProdEq] >- ( 1235 fsrw_tac [][ProdEmpty] >> 1236 rpt (qpat_x_assum `X = {}` mp_tac) >> 1237 `IsSmall (c|a���a|) ��� (c|a���a|) ��� homs c` by ( 1238 fsrw_tac [][homs_def,is_locally_small_def,LET_THM] >> 1239 metis_tac [] ) >> 1240 fsrw_tac [][hom_def,EXTENSION] >> 1241 metis_tac [id_maps_to] ) >> 1242qpat_x_assum `hom_tag c X = Y` mp_tac >> 1243fsrw_tac [][hom_tag_def] >> 1244`is_self_hom c (c|a���a|)` by ( 1245 srw_tac [][is_self_hom_def] >> 1246 metis_tac [] ) >> 1247`{{{}}} <> {Empty}` by ( 1248 srw_tac [][Extension_ax,InSing,Empty_def] >> 1249 metis_tac [Empty_def] ) >> 1250srw_tac [][] >> 1251fsrw_tac [][is_self_hom_def] >> 1252fsrw_tac [][hom_def,EXTENSION] >> 1253qmatch_assum_rename_tac `!x. x :- a ��� b -:c = x :- z ��� z -:c` >> 1254`id z -: c :- z ��� z -:c` by metis_tac [id_maps_to] >> 1255`id z -: c :- a ��� b -:c` by metis_tac [] >> 1256fsrw_tac [][maps_to_in_def]); 1257 1258val _ = export_theory (); 1259