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