Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge commit 'f1620e3' into HOL-Omega

Conflicts:
	src/parse/Absyn.sig
	src/postkernel/Theory.sig
	src/prekernel/FinalTheory-sig.sml
	src/prekernel/Holmakefile

Fixed a bug in src/HolSmt/HolSmtScript.sml where the parser was
given ... term : type ' term ... which confused the parser.
Added parentheses around (term : type).
  • Loading branch information...
commit 4ccab513f9d6abfe4a78a3d8eab3880bf2e8ad76 2 parents a50fa84 + f1620e3
homeier homeier authored
Showing with 3,791 additions and 2,296 deletions.
  1. +533 −0 examples/category/YonedaScript.sml
  2. +106 −10 examples/category/categoryScript.sml
  3. +107 −825 examples/category/ens_catScript.sml
  4. +339 −15 examples/category/functorScript.sml
  5. +412 −0 examples/category/hom_functorScript.sml
  6. +55 −15 examples/category/limitScript.sml
  7. +354 −3 examples/category/nat_transScript.sml
  8. +974 −1,032 examples/category/zfset_catScript.sml
  9. +1 −1  examples/lambda/barendregt/chap11_1Script.sml
  10. +10 −11 examples/lambda/barendregt/chap2Script.sml
  11. +20 −20 examples/lambda/barendregt/chap3Script.sml
  12. +39 −43 examples/lambda/barendregt/finite_developmentsScript.sml
  13. +2 −0  examples/lambda/barendregt/head_reductionScript.sml
  14. +6 −7 examples/lambda/barendregt/preltermScript.sml
  15. +6 −3 examples/lambda/barendregt/standardisationScript.sml
  16. +12 −15 examples/lambda/barendregt/term_posnsScript.sml
  17. +30 −9 examples/lambda/basics/binderLib.sml
  18. +356 −127 examples/lambda/basics/termScript.sml
  19. +1 −0  examples/lambda/other-models/Holmakefile
  20. +2 −0  examples/lambda/other-models/MPlambdaScript.sml
  21. +13 −13 examples/lambda/other-models/diagsScript.sml
  22. +2 −0  examples/lambda/other-models/pure_dBScript.sml
  23. +1 −1  examples/lambda/typing/sttScript.sml
  24. +2 −2 examples/lambda/typing/sttVariantsScript.sml
  25. +36 −0 examples/zfset/zfsetScript.sml
  26. +1 −0  help/src-sml/Asynt.sml
  27. +3 −0  help/src-sml/Parser.grm
  28. +3 −3 help/src-sml/Parsspec.sml
  29. +6 −4 src/HolSmt/HolSmtScript.sml
  30. +38 −1 src/HolSmt/Library.sml
  31. +45 −21 src/HolSmt/SmtLib.sml
  32. +8 −4 src/HolSmt/Yices.sml
  33. +12 −7 src/HolSmt/selftest.sml
  34. +13 −0 src/list/src/listScript.sml
  35. +2 −0  src/n-bit/wordsLib.sig
  36. +53 −0 src/n-bit/wordsLib.sml
  37. +78 −0 src/n-bit/wordsScript.sml
  38. +1 −0  src/parse/Absyn.sig
  39. +0 −8 src/postkernel/Holmakefile
  40. +85 −4 src/postkernel/Theory.sig
  41. +0 −89 src/prekernel/FinalTheory-sig.sml
  42. +0 −3  src/prekernel/Holmakefile
  43. +9 −0 src/quotient/src/quotient.sml
  44. +8 −0 src/quotient/src/selftest.sml
  45. +5 −0 src/tfl/src/Defn.sml
  46. +2 −0  src/tfl/src/selftest.sml
533 examples/category/YonedaScript.sml
View
@@ -0,0 +1,533 @@
+open HolKernel Parse boolLib bossLib SatisfySimps pred_setTheory categoryTheory functorTheory nat_transTheory hom_functorTheory ens_catTheory lcsymtacs;
+
+val _ = new_theory "Yoneda";
+
+val YfunctorNT_def = Define`
+ YfunctorNT c f = mk_nt <|
+ dom := c|_→f.dom|; cod := c|_→f.cod|;
+ map := λx. (c|x→_|##f) |>`
+
+val YfunctorNT_dom_cod = Q.store_thm(
+"YfunctorNT_dom_cod",
+`∀c f. ((YfunctorNT c f).dom = c|_→f.dom|) ∧
+ ((YfunctorNT c f).cod = c|_→f.cod|)`,
+srw_tac [][YfunctorNT_def]);
+val _ = export_rewrites["YfunctorNT_dom_cod"];
+
+val ntdom_YfunctorNT = Q.store_thm(
+"ntdom_YfunctorNT",
+`∀c f. ntdom (YfunctorNT c f) = c°`,
+srw_tac [][YfunctorNT_def,mk_nt_def]);
+
+val ntcod_YfunctorNT = Q.store_thm(
+"ntcod_YfunctorNT",
+`∀c f. ntcod (YfunctorNT c f) = (ens_cat (homs c))`,
+srw_tac [][YfunctorNT_def,mk_nt_def]);
+
+val YfunctorNT_at = Q.store_thm(
+"YfunctorNT_at",
+`∀c f x. x ∈ c.obj ⇒
+ ((YfunctorNT c f)@+x = (c|x→_|##f))`,
+srw_tac [][YfunctorNT_def,mk_nt_def,restrict_def]);
+
+val _ = export_rewrites ["ntdom_YfunctorNT","ntcod_YfunctorNT","YfunctorNT_at"];
+
+(*
+val HasFunType_postcomp = Q.store_thm(
+"HasFunType_postcomp",
+`∀c f w x y z. is_category c ∧ f :- x → y -:c ∧ (w = z)
+ ⇒ HasFunType (λg. g o f -:c) (c|y→z|) (c|x→w|)`,
+
+Problem: (λg. g o f -:c) has a dependent type.
+The type is ∀z. c|y→z| c|x→z|
+It is extensional on the union over all z of c|y→z|
+but depending on which element of the union you came from, the result type can be constrained
+*)
+
+val is_nat_trans_YfunctorNT = Q.store_thm(
+"is_nat_trans_YfunctorNT",
+`∀c f. is_category c ∧ f ∈ c.mor ⇒ is_nat_trans (YfunctorNT c f)`,
+srw_tac [][YfunctorNT_def] >>
+srw_tac [][nat_trans_axioms_def] >- (
+ imp_res_tac mor_obj >>
+ fsrw_tac [][hom_def] >>
+ match_mp_tac maps_to_comp >>
+ metis_tac [maps_to_in_def,maps_to_def] ) >>
+qmatch_assum_rename_tac `g° :- y → x -:c` [] >>
+imp_res_tac maps_to_in_def >>
+fsrw_tac [][] >> srw_tac [][] >>
+imp_res_tac mor_obj >> srw_tac [][] >>
+qmatch_abbrev_tac
+ `(TypedGraphFun (t2,t3) f2) o (TypedGraphFun (t1,t2) f1) -:ens_cat U =
+ (TypedGraphFun (t4,t3) f1) o (TypedGraphFun (t1,t4) f2) -:ens_cat U` >>
+`(∀x. x ∈ t1 ⇒ f1 x ∈ t2) ∧
+ (∀x. x ∈ t4 ⇒ f1 x ∈ t3) ∧
+ (∀x. x ∈ t2 ⇒ f2 x ∈ t3) ∧
+ (∀x. x ∈ t1 ⇒ f2 x ∈ t4)` by (
+ unabbrev_all_tac >>
+ fsrw_tac [][hom_def] >>
+ srw_tac [][] >>
+ match_mp_tac maps_to_comp >>
+ metis_tac []) >>
+qmatch_abbrev_tac `x o w -:ens_cat U = v o u -:ens_cat U` >>
+`IsTypedFun u ∧ IsTypedFun v ∧ IsTypedFun w ∧ IsTypedFun x` by
+ metis_tac [IsTypedFunTypedGraphFun] >>
+`IsTypedFunIn U u ∧ IsTypedFunIn U v ∧ IsTypedFunIn U w ∧ IsTypedFunIn U x` by (
+ unabbrev_all_tac >> fsrw_tac [][] ) >>
+`u ∈ (ens_cat U).mor ∧ v ∈ (ens_cat U).mor ∧ w ∈ (ens_cat U).mor ∧ x ∈ (ens_cat U).mor` by
+ metis_tac [ens_cat_mor] >>
+`u ≈> v -:(ens_cat U)` by (
+ srw_tac [][composable_def,Abbr`v`,Abbr`u`,Abbr`U`]) >>
+`w ≈> x -:ens_cat U` by (
+ srw_tac [][composable_def,Abbr`x`,Abbr`w`,Abbr`U`]) >>
+srw_tac [][] >>
+map_every qunabbrev_tac [`u`,`v`,`w`,`x`] >>
+srw_tac [][ComposeTypedFun_def,TypedGraphFun_def] >>
+srw_tac [][ComposeFun_def] >>
+srw_tac [][restrict_def] >>
+srw_tac [][FUN_EQ_THM] >>
+srw_tac [][Abbr`f1`,Abbr`f2`] >>
+match_mp_tac (GSYM comp_assoc) >>
+qunabbrev_tac `t1` >>
+fsrw_tac [][hom_def] >>
+imp_res_tac maps_to_composable >>
+srw_tac [][]);
+val _ = export_rewrites["is_nat_trans_YfunctorNT"];
+
+val YfunctorNT_maps_to = Q.store_thm(
+"YfunctorNT_maps_to",
+`∀c f. is_category c ∧ f ∈ c.mor ⇒
+ (YfunctorNT c f) :- (c|_→f.dom|) → (c|_→f.cod|) -:[(c°)→ens_cat (homs c)]`,
+srw_tac [][maps_to_in_def]);
+val _ = export_rewrites["YfunctorNT_maps_to"];
+
+val YfunctorNT_composable = Q.store_thm(
+"YfunctorNT_composable",
+`∀c f g. is_category c ∧ f ≈> g -:c ⇒
+ (YfunctorNT c f) ≈> (YfunctorNT c g) -:[(c°)→ens_cat (homs c)]`,
+srw_tac [][composable_nts_def] >> fsrw_tac [][composable_in_def]);
+val _ = export_rewrites["YfunctorNT_composable"];
+
+val YfunctorNT_id = Q.store_thm(
+"YfunctorNT_id",
+`∀c x. is_category c ∧ x ∈ c.obj ⇒ (YfunctorNT c (id x -:c) = id_nt (c|_→x|))`,
+srw_tac [][] >> match_mp_tac nt_eq_thm >>
+srw_tac [][id_mor] >>
+srw_tac [][TypedGraphFun_def,restrict_def] >>
+srw_tac [][FUN_EQ_THM] >> srw_tac [][] >>
+fsrw_tac [][hom_def,maps_to_in_def]);
+val _ = export_rewrites["YfunctorNT_id"];
+
+val is_category_presheaf_cat = Q.store_thm(
+"is_category_presheaf_cat",
+`∀c. is_category c ⇒ is_category [(c°)→ens_cat (homs c)]`,
+metis_tac [is_category_functor_cat,is_category_ens_cat,is_category_op_cat])
+val _ = export_rewrites["is_category_presheaf_cat"];
+
+val pre_Yfunctor_def = Define`
+ pre_Yfunctor c = <|
+ dom := c; cod := [(c°)→ens_cat (homs c)];
+ map := λf. YfunctorNT c f |>`;
+
+val pre_Yfunctor_components = Q.store_thm(
+"pre_Yfunctor_components",
+`∀c. ((pre_Yfunctor c).dom = c) ∧
+ ((pre_Yfunctor c).cod = [(c°)→ens_cat (homs c)]) ∧
+ ((pre_Yfunctor c).map = λf. YfunctorNT c f) ∧
+ (∀f. (pre_Yfunctor c)##f = YfunctorNT c f)`,
+srw_tac [][pre_Yfunctor_def,morf_def]);
+val _ = export_rewrites["pre_Yfunctor_components"];
+
+val pre_Yfunctor_objf = Q.store_thm(
+"pre_Yfunctor_objf",
+`∀c x. is_category c ∧ x ∈ c.obj
+ ⇒ ((pre_Yfunctor c)@@x = c|_→x|)`,
+srw_tac [][objf_def] >>
+SELECT_ELIM_TAC >> srw_tac [][] >- (
+ qexists_tac `c|_→x|` >> srw_tac [][] ) >>
+pop_assum mp_tac >>
+srw_tac [][id_in_def] >>
+Q.ISPEC_THEN `[(c°)→ens_cat (homs c)]` match_mp_tac id_inj >>
+srw_tac [][]);
+val _ = export_rewrites["pre_Yfunctor_objf"];
+
+val Yfunctor_def = Define`
+ Yfunctor c = mk_functor (pre_Yfunctor c)`;
+
+val is_functor_Yfunctor = Q.store_thm(
+"is_functor_Yfunctor",
+`∀c. is_category c ⇒ is_functor (Yfunctor c)`,
+srw_tac [][Yfunctor_def] >>
+srw_tac [][functor_axioms_def,morf_def]
+>- (imp_res_tac maps_to_obj >> fsrw_tac [][morf_def,maps_to_in_def])
+>- (imp_res_tac maps_to_obj >> fsrw_tac [][morf_def,maps_to_in_def])
+>- fsrw_tac [][maps_to_in_def]
+>- (qexists_tac `c|_→x|` >> srw_tac [][]) >>
+qspecl_then [`c`,`f`,`g`,`f.dom`,`g.cod`] mp_tac composable_maps_to >>
+srw_tac [][] >>
+imp_res_tac maps_to_in_def >>
+imp_res_tac YfunctorNT_composable >>
+match_mp_tac nt_eq_thm >> fsrw_tac [][] >>
+conj_tac >- ( fsrw_tac [][nt_comp_def,compose_def,mk_nt_def,restrict_def,YfunctorNT_def,composable_in_def]) >>
+conj_tac >- ( fsrw_tac [][nt_comp_def,compose_def,mk_nt_def,restrict_def,YfunctorNT_def,composable_in_def]) >>
+`f ∈ c.mor ∧ g ∈ c.mor` by (
+ imp_res_tac composable_in_def >> srw_tac [][]) >>
+srw_tac [][] >>
+qmatch_abbrev_tac
+ `h = TypedGraphFun (i,j) k o TypedGraphFun (l,m) n -:ens_cat (homs c)` >>
+`(∀x. x ∈ i ⇒ k x ∈ j) ∧ (∀x. x ∈ l ⇒ n x ∈ m)` by (
+ unabbrev_all_tac >>
+ srw_tac [][hom_def] >>
+ match_mp_tac maps_to_comp >>
+ metis_tac [maps_to_in_def,maps_to_def] ) >>
+imp_res_tac IsTypedFunTypedGraphFun >>
+imp_res_tac ens_cat_mor >>
+ntac 2 (pop_assum (qspec_then `(homs c)` mp_tac)) >>
+`m = i` by (
+ fsrw_tac [][composable_in_def,Abbr`m`,Abbr`i`] ) >>
+`l ∈ homs c ∧ i ∈ homs c ∧ j ∈ homs c` by (
+ unabbrev_all_tac >> srw_tac [][] ) >>
+`(TypedGraphFun (l,m) n) ≈> (TypedGraphFun (i,j) k) -:ens_cat (homs c)` by (
+ srw_tac [][]) >>
+srw_tac [][Abbr`h`] >>
+srw_tac [][TypedGraphFun_def,ComposeTypedFun_def] >>
+srw_tac [][ComposeFun_def] >>
+srw_tac [][restrict_def] >>
+srw_tac [][FUN_EQ_THM] >>
+unabbrev_all_tac >>
+srw_tac [][] >>
+`g.dom = f.cod` by (
+ fsrw_tac [][composable_in_def] ) >>
+match_mp_tac comp_assoc >>
+fsrw_tac [][hom_def] >>
+match_mp_tac maps_to_composable >>
+map_every qexists_tac [`x`,`f.dom`,`f.cod`] >>
+srw_tac [][]);
+
+val Yfunctor_dom = Q.store_thm(
+"Yfunctor_dom",
+`∀c. (Yfunctor c).dom = c`,
+srw_tac [][Yfunctor_def]);
+
+val Yfunctor_cod = Q.store_thm(
+"Yfunctor_cod",
+`∀c. (Yfunctor c).cod = [(c°)→ens_cat (homs c)]`,
+srw_tac [][Yfunctor_def]);
+
+val Yfunctor_objf = Q.store_thm(
+"Yfunctor_objf",
+`∀c x. is_category c ∧ x ∈ c.obj ⇒
+ ((Yfunctor c)@@x = c|_→x|)`,
+srw_tac [][Yfunctor_def,mk_functor_objf]);
+
+val Yfunctor_morf = Q.store_thm(
+"Yfunctor_morf",
+`∀c f. is_category c ∧ f ∈ c.mor ⇒
+ ((Yfunctor c)##f = YfunctorNT c f)`,
+srw_tac [][Yfunctor_def,morf_def]);
+
+val _ = export_rewrites["Yfunctor_dom","Yfunctor_cod","Yfunctor_objf","Yfunctor_morf"];
+
+val YMap_def = Define`
+ YMap c x n = (n@+x).map (id x-:c)`;
+
+val YMapImage = Q.store_thm(
+"YMapImage",
+`∀c x n f. is_category c ∧ is_functor f ∧ is_nat_trans n ∧
+ (f :- c° → ens_cat (homs c)) ∧ x ∈ c.obj ∧
+ (n :- ((Yfunctor c)@@x) → f) ⇒
+ (YMap c x n) ∈ (f@@x)`,
+srw_tac [][YMap_def] >>
+`(n @+ x) :- (n.dom @@ x) → (n.cod @@ x) -: n.dom.cod` by (
+ fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
+pop_assum mp_tac >> srw_tac [][] >>
+ntac 4 (pop_assum mp_tac) >> srw_tac [][] >>
+fsrw_tac [][IsTypedFun_def] >>
+fsrw_tac [][HasFunType_def] >>
+first_x_assum match_mp_tac >>
+srw_tac [][hom_def,id_maps_to]);
+
+val YMapInv_def = Define`
+ YMapInv c x f y = mk_nt <|
+ dom := (Yfunctor c)@@x;
+ cod := f;
+ map := λz. TypedGraphFun ((c|z→x|), f@@z)
+ (λg. (f##(g°)).map y) |>`;
+
+val YMapInv_at = Q.store_thm(
+"YMapInv_at",
+`∀c x f y z. is_category c ∧ x ∈ c.obj ∧ z ∈ c.obj ⇒
+ ((YMapInv c x f y) @+ z =
+ TypedGraphFun ((c|z→x|), f@@z)
+ (λg. (f##g°).map y))`,
+srw_tac [][YMapInv_def,mk_nt_def,restrict_def]);
+val _ = export_rewrites["YMapInv_at"];
+
+val is_nat_trans_YMapInv = Q.store_thm(
+"is_nat_trans_YMapInv",
+`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat (homs c)) ∧
+ x ∈ c.obj ∧ y ∈ (f@@x)
+ ⇒ is_nat_trans (YMapInv c x f y)`,
+srw_tac [][YMapInv_def] >>
+srw_tac [][nat_trans_axioms_def]
+>- metis_tac [objf_in_obj,op_cat_obj,ens_cat_obj]
+>- (
+ qmatch_assum_rename_tac `g ∈ c|u→x|` [] >>
+ `g° :- x → u -:(c°)` by fsrw_tac [][hom_def] >>
+ `f##g° :- (f@@x) → (f@@u) -:ens_cat (homs c)` by (
+ match_mp_tac morf_maps_to >>
+ map_every qexists_tac [`f.dom`,`x`,`u`] >>
+ srw_tac [][] ) >>
+ fsrw_tac [][IsTypedFun_def,HasFunType_def] >>
+ fsrw_tac [][]) >>
+qmatch_assum_rename_tac `g° :- u → v -:c` [] >>
+imp_res_tac maps_to_in_def >>
+fsrw_tac [][] >>
+qmatch_abbrev_tac
+`(TypedGraphFun (i,j) k) o (TypedGraphFun (l,i) n) -:ens_cat (homs c) =
+ q o (TypedGraphFun (l,s) h) -:ens_cat (homs c)` >>
+`(∀x. x ∈ i ⇒ k x ∈ j) ∧ (∀x. x ∈ l ⇒ h x ∈ s)` by (
+ unabbrev_all_tac >> srw_tac [][] >>
+ qmatch_assum_abbrev_tac `z ∈ (c|q→x|)` >>
+ `f##(z)° :- f@@x → f@@q -:ens_cat (homs c)` by (
+ match_mp_tac morf_maps_to >>
+ fsrw_tac [][hom_def] ) >>
+ fsrw_tac [][maps_to_in_def,IsTypedFun_def,HasFunType_def] >>
+ fsrw_tac [][]) >>
+`∀x. x ∈ l ⇒ n x ∈ i` by (
+ srw_tac [][Abbr`n`,Abbr`i`,Abbr`l`,hom_def] >>
+ match_mp_tac maps_to_comp >>
+ qexists_tac `g.dom` >>
+ srw_tac [SATISFY_ss][]) >>
+`q :- s → j -:ens_cat (homs c)` by (
+ map_every qunabbrev_tac [`q`,`s`,`j`] >>
+ match_mp_tac morf_maps_to >>
+ map_every qexists_tac [`f.dom`,`g.dom`,`g.cod`] >>
+ srw_tac [][] ) >>
+`IsTypedFun q` by fsrw_tac [][maps_to_in_def] >>
+imp_res_tac maps_to_in_def >>
+srw_tac [][Abbr`k`] >>
+imp_res_tac IsTypedFunTypedGraphFun >>
+`l ∈ homs c ∧ i ∈ homs c ∧ j ∈ homs c` by (
+ unabbrev_all_tac >>
+ srw_tac [][] >> TRY (
+ match_mp_tac hom_in_homs >>
+ imp_res_tac mor_obj >> fsrw_tac [][] >>
+ NO_TAC ) >>
+ metis_tac [objf_in_obj,ens_cat_obj,maps_to_obj,op_cat_obj] ) >>
+`TypedGraphFun (l,s) h ≈> q -: ens_cat (homs c)` by (
+ fsrw_tac [][Abbr`q`,Abbr`s`,maps_to_in_def] ) >>
+srw_tac [][] >>
+`TypedGraphFun (l,i) n ≈> TypedGraphFun (i,j) h -:ens_cat (homs c)` by (
+ srw_tac [][] ) >>
+unabbrev_all_tac >>
+fsrw_tac [][ComposeTypedFun_def,compose_def,restrict_def] >>
+srw_tac [][ComposeFun_def] >>
+srw_tac [][restrict_def] >>
+srw_tac [][FUN_EQ_THM] >>
+srw_tac [][hom_def] >>
+Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`g`] mp_tac morf_comp >>
+`e° ≈> g -:c°` by (
+ srw_tac [][composable_in_def] >>
+ fsrw_tac [][maps_to_in_def] ) >>
+fsrw_tac [][op_cat_compose_in] >>
+Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`g`] mp_tac morf_composable >>
+srw_tac [][ComposeFun_def,restrict_def] >- (
+ fsrw_tac [][hom_def] >> metis_tac [] ) >>
+Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`e.cod`,`e.dom`] mp_tac morf_maps_to >>
+fsrw_tac [][maps_to_in_def] >> srw_tac [][] >>
+fsrw_tac [][]);
+val _ = export_rewrites["is_nat_trans_YMapInv"];
+
+val YMapInvImage = Q.store_thm(
+"YMapInvImage",
+`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat (homs c)) ∧
+ x ∈ c.obj ∧ y ∈ (f@@x) ⇒
+ is_nat_trans (YMapInv c x f y) ∧
+ ((YMapInv c x f y) :- (Yfunctor c)@@x → f)`,
+srw_tac [][YMapInv_def]);
+
+val YMap1 = Q.store_thm(
+"YMap1",
+`∀c f x n. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat (homs c)) ∧
+ x ∈ c.obj ∧ is_nat_trans n ∧ (n :- ((Yfunctor c)@@x) → f) ⇒
+ (YMapInv c x f (YMap c x n) = n)`,
+rpt strip_tac >>
+match_mp_tac nt_eq_thm >>
+imp_res_tac YMapImage >>
+imp_res_tac is_nat_trans_YMapInv >>
+srw_tac [][]
+>- fsrw_tac [][YMapInv_def]
+>- fsrw_tac [][YMapInv_def] >>
+qmatch_rename_tac `X = n @+ z` ["X"] >>
+`z ∈ c.obj` by (
+ pop_assum mp_tac >> srw_tac [][YMapInv_def] ) >>
+srw_tac [][] >>
+fsrw_tac [][] >>
+qpat_assum `X = (Yfunctor c)@@x` mp_tac >> srw_tac [][] >>
+`∀z. z ∈ c.obj ⇒ n @+ z :- c|z→x| → (n.cod@@z) -:n.cod.cod` by (
+ fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
+ metis_tac [contra_hom_functor_objf] ) >>
+first_assum (qspec_then `z` mp_tac) >>
+first_x_assum (qspec_then `x` mp_tac) >>
+srw_tac [][] >>
+srw_tac [][TypedGraphFun_def,morphism_component_equality] >>
+srw_tac [][restrict_def] >>
+srw_tac [][FUN_EQ_THM] >>
+fsrw_tac [][IsTypedFun_def,HasFunType_def,extensional_def] >>
+srw_tac [][YMap_def] >>
+qmatch_assum_rename_tac `f ∈ c|z→x|` [] >>
+Q.ISPECL_THEN [`n`,`c|_→x|`,`n.cod` ,`n.cod.cod` ,`f°`,`x`,`z`]
+ mp_tac naturality >>
+fsrw_tac [][hom_def] >>
+qmatch_abbrev_tac `(f1 o f2 -:ens_cat (homs c) = f3 o f4 -:ens_cat (homs c)) ⇒ X` >>
+`IsTypedFun f2` by (
+ srw_tac [][Abbr`f2`] >>
+ imp_res_tac maps_to_in_def >>
+ srw_tac [][hom_def] >>
+ match_mp_tac maps_to_comp >>
+ qexists_tac `x` >>
+ fsrw_tac [][maps_to_in_def]) >>
+`f1 :- f1.dom → f1.cod -:ens_cat (homs c)` by (
+ qunabbrev_tac `f1` >>
+ match_mp_tac nt_at_maps_to >>
+ srw_tac [][hom_def] ) >>
+`f4 :- f4.dom → f4.cod -:ens_cat (homs c)` by (
+ qunabbrev_tac `f4` >>
+ match_mp_tac nt_at_maps_to >>
+ srw_tac [][hom_def] ) >>
+`(n.cod##f°) :- n.cod@@x → n.cod@@z -:n.cod.cod` by (
+ match_mp_tac morf_maps_to >>
+ fsrw_tac [][] >>
+ map_every qexists_tac [`x`,`z`] >>
+ srw_tac [][] ) >>
+`f3 :- f3.dom → f3.cod -:ens_cat (homs c)` by (
+ qunabbrev_tac `f3` >>
+ match_mp_tac morf_maps_to >>
+ srw_tac [][] >>
+ map_every qexists_tac [`x`,`z`] >>
+ srw_tac [][] >>
+ fsrw_tac [][maps_to_in_def] ) >>
+imp_res_tac maps_to_in_def >>
+`f2 ≈> f1 -:ens_cat (homs c)` by (
+ fsrw_tac [][Abbr`f2`,hom_def] >>
+ srw_tac [][] >>
+ match_mp_tac maps_to_comp >>
+ srw_tac [SATISFY_ss][] ) >>
+`f4 ≈> f3 -:ens_cat (homs c)` by (
+ fsrw_tac [][Abbr`f3`] ) >>
+`n.cod@@z = f3.cod` by (
+ fsrw_tac [][maps_to_in_def,Abbr`f3`] ) >>
+`f2.dom = f4.dom` by (
+ fsrw_tac [][Abbr`f4`,Abbr`f2`,hom_def] ) >>
+`f2.map (id f.cod -:c) = f` by (
+ srw_tac [][Abbr`f2`] >>
+ srw_tac [][restrict_def,hom_def] >>
+ fsrw_tac [][] >> srw_tac [][] >>
+ pop_assum mp_tac >> srw_tac [][id_maps_to] ) >>
+fsrw_tac [][ComposeTypedFun_def,compose_def,restrict_def,ComposeFun_def] >>
+srw_tac [][FUN_EQ_THM] >>
+pop_assum (qspec_then `id f.cod -:c` mp_tac) >>
+fsrw_tac [][id_maps_to]);
+
+val YMap2 = Q.store_thm(
+"YMap2",
+`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat (homs c)) ∧
+ x ∈ c.obj ∧ y ∈ (f@@x) ⇒
+ (YMap c x (YMapInv c x f y) = y)`,
+srw_tac [][YMap_def] >>
+srw_tac [][restrict_def,hom_def] >>
+`f##(id x -:(c°)) = id (f@@x) -: ens_cat (homs c)` by srw_tac [][morf_id] >>
+fsrw_tac [][] >>
+`f@@x ∈ homs c` by (
+ metis_tac [objf_in_obj,op_cat_obj,ens_cat_obj] ) >>
+srw_tac [][restrict_def]);
+
+val YfunctorNT_YMapInv = Q.store_thm(
+"YfunctorNT_YMapInv",
+`∀c f x y. is_category c ∧ f :- x → y -:c ⇒
+ (YfunctorNT c f = YMapInv c x (c|_→y|) f)`,
+srw_tac [][] >>
+match_mp_tac nt_eq_thm >>
+imp_res_tac maps_to_in_def >>
+imp_res_tac maps_to_obj >>
+fsrw_tac [][] >>
+conj_tac >- (
+ match_mp_tac is_nat_trans_YMapInv >>
+ srw_tac [][hom_def] ) >>
+conj_tac >- srw_tac [][YfunctorNT_def,YMapInv_def] >>
+conj_tac >- srw_tac [][YfunctorNT_def,YMapInv_def] >>
+srw_tac [][TypedGraphFun_def] >>
+srw_tac [][restrict_def] >>
+srw_tac [][FUN_EQ_THM] >>
+srw_tac [][hom_def] >>
+imp_res_tac maps_to_in_def >>
+srw_tac [][restrict_def] >>
+fsrw_tac [][hom_def,maps_to_in_def] >>
+fsrw_tac [][]);
+
+val YMapYoneda = Q.store_thm(
+"YMapYoneda",
+`∀c f x y. is_category c ∧ f :- x → y -:c ⇒
+ ((Yfunctor c)##f = YMapInv c x ((Yfunctor c)@@y) f)`,
+srw_tac [][] >>
+imp_res_tac maps_to_in_def >>
+imp_res_tac maps_to_obj >>
+srw_tac [][YfunctorNT_YMapInv]);
+
+val YonedaFull = Q.store_thm(
+"YonedaFull",
+`∀c. is_category c ⇒ full (Yfunctor c)`,
+srw_tac [][full_def] >>
+qexists_tac `YMap c a h` >>
+`YMap c a h ∈ (c|_→b|)@@a` by (
+ match_mp_tac YMapImage >>
+ imp_res_tac Yfunctor_objf >>
+ fsrw_tac [][] ) >>
+pop_assum mp_tac >> srw_tac [][contra_hom_functor_objf,hom_def] >>
+match_mp_tac EQ_TRANS >>
+qexists_tac `YMapInv c a (Yfunctor c@@b) (YMap c a h)` >>
+conj_tac >- srw_tac [][YMapYoneda] >>
+match_mp_tac YMap1 >>
+fsrw_tac [][]);
+
+val YonedaFaithful = Q.store_thm(
+"YonedaFaithful",
+`∀c. is_category c ⇒ faithful (Yfunctor c)`,
+srw_tac [][faithful_def] >>
+`YMap c a (YMapInv c a (c|_→b|) g) =
+ YMap c a (YMapInv c a (c|_→b|) h)`
+ by metis_tac [maps_to_in_def,Yfunctor_morf,YfunctorNT_YMapInv] >>
+match_mp_tac EQ_TRANS >>
+qexists_tac `YMap c a (YMapInv c a (c|_→b|) g)` >>
+conj_tac >- (
+ match_mp_tac EQ_SYM >>
+ match_mp_tac YMap2 >>
+ imp_res_tac maps_to_obj >>
+ fsrw_tac [][hom_def] ) >>
+srw_tac [][] >>
+match_mp_tac YMap2 >>
+imp_res_tac maps_to_obj >>
+fsrw_tac [][hom_def]);
+
+val YonedaEmbedding = Q.store_thm(
+"YonedaEmbedding",
+`∀c. is_category c ⇒ embedding (Yfunctor c)`,
+srw_tac [][embedding_def,YonedaFaithful,YonedaFull]);
+
+val YonedaInjObj = Q.store_thm(
+"YonedaInjObj",
+`∀c. is_category c ⇒ inj_obj (Yfunctor c)`,
+srw_tac [][inj_obj_def] >>
+srw_tac [][] >> pop_assum mp_tac >> srw_tac [][] >>
+`(c|_→a|)@@a = (c|_→b|)@@a` by asm_simp_tac std_ss [] >>
+pop_assum mp_tac >>
+pop_assum (K ALL_TAC) >>
+srw_tac [][EXTENSION] >>
+pop_assum (qspec_then `id a -:c` mp_tac) >>
+srw_tac [][hom_def,id_maps_to] >>
+fsrw_tac [][maps_to_in_def] >>
+imp_res_tac id_maps_to >>
+fsrw_tac [][maps_to_in_def]);
+
+val _ = export_theory ();
116 examples/category/categoryScript.sml
View
@@ -29,7 +29,7 @@ srw_tac [][EQ_IMP_THM] >- (
metis_tac [extensional_restrict]);
val _ = Hol_datatype`morphism = <|
- dom : 'a; cod : 'b; map : 'c |>`;
+ dom : α; cod : β; map : γ |>`;
val morphism_component_equality = DB.theorem"morphism_component_equality";
@@ -46,7 +46,7 @@ val _ = add_rule {
val composable_def = Define`f ≈> g = (f.cod = g.dom)`;
val compose_def = Define`
- compose (c:('a,'b,'c) morphism -> ('b,'d,'e) morphism -> 'f) =
+ compose (c:(α,β,γ) morphism -> (β,δ,ε) morphism -> ζ) =
CURRY (restrict
(λ(f,g). <| dom := f.dom; cod := g.cod; map := c f g |>)
{(f,g) | f ≈> g})`;
@@ -61,13 +61,13 @@ val _ = add_rule {
val maps_to_def = Define`f :- x → y = (f.dom = x) ∧ (f.cod = y)`;
-val _ = type_abbrev("mor",``:('a,'a,'b) morphism``);
+val _ = type_abbrev("mor",``:(α,α,β) morphism``);
val _ = Hol_datatype `category =
- <| obj : 'a set ;
- mor : ('a,'b) mor set ;
- id_map : 'a -> 'b;
- comp : ('a,'b) mor -> ('a,'b) mor -> 'b |>`;
+ <| obj : α set ;
+ mor : (α,β) mor set ;
+ id_map : α -> β;
+ comp : (α,β) mor -> (α,β) mor -> β |>`;
val category_component_equality = DB.theorem "category_component_equality";
@@ -174,7 +174,7 @@ srw_tac [][compose_def,restrict_def]);
val _ = export_rewrites["composable_def","maps_to_def","compose_thm"];
val mk_cat_def = Define`
- mk_cat (c:('a,'b) category) = <|
+ mk_cat (c:(α,β) category) = <|
obj := c.obj;
mor := c.mor;
id_map := restrict c.id_map c.obj;
@@ -481,7 +481,7 @@ val _ = overload_on("inv_in_syntax",``λf c. inv_in c f``);
val inv_elim_thm = Q.store_thm(
"inv_elim_thm",
-`∀P (c:('a,'b) category) f g. is_category c ∧ f <≃> g -:c ∧ P g ⇒ P f⁻¹-:c`,
+`∀P (c:(α,β) category) f g. is_category c ∧ f <≃> g -:c ∧ P g ⇒ P f⁻¹-:c`,
srw_tac [][inv_in_def] >>
SELECT_ELIM_TAC >>
srw_tac [SATISFY_ss][] >>
@@ -493,7 +493,7 @@ fun is_inv_in tm = let
val (inv_in,[c,f]) = strip_comb tm
val ("inv_in",ty) = dest_const inv_in
in
- can (match_type ``:('a,'b) category -> ('a,'b) mor -> ('a,'b) mor``) ty
+ can (match_type ``:(α,β) category -> (α,β) mor -> (α,β) mor``) ty
end handle HOL_ERR _ => false | Bind => false;
fun inv_elim_tac (g as (_, w)) = let
@@ -826,6 +826,52 @@ srw_tac [][composable_in_def] >>
srw_tac [][pred_setTheory.EXTENSION] >>
fsrw_tac [][oneTheory.one,morphism_component_equality,FUN_EQ_THM]);
+val indiscrete_cat_def = Define`
+ indiscrete_cat s = mk_cat <|
+ obj := s; mor := { <|dom := x; cod := y; map := ()|> | x ∈ s ∧ y ∈ s };
+ id_map := K ();
+ comp := λf g. f.map |>`;
+
+val is_category_indiscrete_cat = Q.store_thm(
+"is_category_indiscrete_cat",
+`∀s. is_category (indiscrete_cat s)`,
+srw_tac [][indiscrete_cat_def] >>
+fsrw_tac [DNF_ss]
+[category_axioms_def,maps_to_in_def,compose_in_def,
+ id_in_def,composable_in_def,restrict_def]);
+val _ = export_rewrites["is_category_indiscrete_cat"];
+
+val indiscrete_cat_obj_mor = Q.store_thm(
+"indiscrete_cat_obj_mor",
+`∀s. ((indiscrete_cat s).obj = s) ∧
+ ((indiscrete_cat s).mor = {f | f.dom ∈ s ∧ f.cod ∈ s })`,
+srw_tac [][indiscrete_cat_def,morphism_component_equality,oneTheory.one,EXTENSION]);
+val _ = export_rewrites["indiscrete_cat_obj_mor"];
+
+val indiscrete_cat_id = Q.store_thm(
+"indiscrete_cat_id",
+`∀s x. x ∈ s ⇒ (id x -:(indiscrete_cat s) = <|dom := x; cod := x; map := ()|>)`,
+srw_tac [][id_in_def,restrict_def,morphism_component_equality,oneTheory.one]);
+val _ = export_rewrites["indiscrete_cat_id"];
+
+val indiscrete_cat_maps_to = Q.store_thm(
+"indiscrete_cat_maps_to",
+`∀f x y s. f :- x → y -:(indiscrete_cat s) = (f :- x → y) ∧ x ∈ s ∧ y ∈ s`,
+srw_tac [][maps_to_in_def,EQ_IMP_THM] >> srw_tac [][]);
+val _ = export_rewrites["indiscrete_cat_maps_to"];
+
+val indiscrete_cat_composable = Q.store_thm(
+"indiscrete_cat_composable",
+`∀s f g. f ≈> g -:indiscrete_cat s = (f ≈> g) ∧ f ∈ (indiscrete_cat s).mor ∧ g ∈ (indiscrete_cat s).mor`,
+srw_tac [][composable_in_def,morphism_component_equality,EQ_IMP_THM]);
+val _ = export_rewrites["indiscrete_cat_composable"];
+
+val indiscrete_cat_compose_in = Q.store_thm(
+"indiscrete_cat_compose_in",
+`∀s f g. f ≈> g -:indiscrete_cat s ⇒ ((g o f -:indiscrete_cat s) = compose (K (K ())) f g)`,
+fsrw_tac [][compose_in_def,restrict_def,oneTheory.one]);
+val _ = export_rewrites["indiscrete_cat_compose_in"];
+
val _ = add_rule {
term_name = "op_syntax",
fixity = Suffix 2100,
@@ -1049,6 +1095,56 @@ srw_tac [][uiso_objs_def,op_cat_iso_pair_between_objs] >>
fsrw_tac [][EXISTS_UNIQUE_THM,EXISTS_PROD,FORALL_PROD] >>
metis_tac [iso_pair_between_objs_sym,op_mor_idem]);
+val category_eq_thm = Q.store_thm(
+"category_eq_thm",
+`∀c1 c2. is_category c1 ∧ is_category c2 ∧
+ (c1.obj = c2.obj) ∧ (c1.mor = c2.mor) ∧
+ (∀x. x ∈ c1.obj ⇒ (id x -:c1 = id x -:c2)) ∧
+ (∀f g. f ≈> g -:c1 ⇒ (g o f -:c1 = g o f-:c2))
+⇒ (c1 = c2)`,
+srw_tac [][category_component_equality] >>
+srw_tac [][FUN_EQ_THM] >- (
+ qmatch_rename_tac `c1.id_map x = c2.id_map x` [] >>
+ Cases_on `x ∈ c1.obj` >- (
+ first_x_assum (qspec_then `x` mp_tac) >>
+ srw_tac [][id_in_def,restrict_def] >>
+ metis_tac [] ) >>
+ fsrw_tac [][is_category_def,extensional_category_def,extensional_def] >>
+ metis_tac [] ) >>
+qmatch_rename_tac `c1.comp f g = c2.comp f g` [] >>
+Cases_on `f ≈> g-:c1` >- (
+ first_x_assum (qspecl_then [`f`,`g`] mp_tac) >>
+ srw_tac [][compose_in_def,restrict_def,compose_def,composable_in_def] >>
+ fsrw_tac [][composable_in_def] >>
+ metis_tac [] ) >>
+fsrw_tac [][is_category_def,extensional_category_def,extensional_def,FORALL_PROD] >>
+fsrw_tac [][composable_in_def] >> metis_tac []);
+
+val op_discrete_cat = Q.store_thm(
+"op_discrete_cat",
+`∀s. (discrete_cat s)° = discrete_cat s`,
+srw_tac [][] >> match_mp_tac category_eq_thm >>
+srw_tac [][] >- (
+ srw_tac [DNF_ss][morphism_component_equality,EXTENSION] >>
+ metis_tac [] ) >>
+fsrw_tac [][compose_in_def,restrict_def,compose_def,op_cat_comp] >>
+srw_tac [][] >> fsrw_tac [][morphism_component_equality] >>
+srw_tac [][] >> metis_tac []);
+val _ = export_rewrites["op_discrete_cat"];
+
+val op_indiscrete_cat = Q.store_thm(
+"op_indiscrete_cat",
+`∀s. (indiscrete_cat s)° = indiscrete_cat s`,
+srw_tac [][] >> match_mp_tac category_eq_thm >>
+srw_tac [][] >- (
+ srw_tac [DNF_ss][morphism_component_equality,EXTENSION] >>
+ srw_tac [][EQ_IMP_THM] >>
+ fsrw_tac [][oneTheory.one] >>
+ qexists_tac `op_mor x` >>
+ srw_tac [][] ) >>
+srw_tac [][compose_in_def,restrict_def,oneTheory.one]);
+val _ = export_rewrites["op_indiscrete_cat"];
+
val product_mor_def = Define`
product_mor (f,g) =
<| dom := (f.dom,g.dom); cod := (f.cod,g.cod); map := (f.map,g.map) |>`;
932 examples/category/ens_catScript.sml
View
@@ -1,4 +1,4 @@
-open HolKernel Parse boolLib bossLib boolSimps pred_setTheory pairTheory categoryTheory functorTheory nat_transTheory lcsymtacs SatisfySimps;
+open HolKernel Parse boolLib boolSimps bossLib SatisfySimps categoryTheory functorTheory pred_setTheory limitTheory lcsymtacs;
val _ = new_theory "ens_cat";
@@ -8,6 +8,16 @@ val HasFunType_def = Define`
val IsTypedFun_def = Define`
IsTypedFun f = HasFunType f.map f.dom f.cod`;
+val TypedFun_ext = Q.store_thm(
+"TypedFun_ext",
+`∀f g. IsTypedFun f ∧ IsTypedFun g ⇒
+ ((f = g) = ((f.dom = g.dom) ∧ (f.cod = g.cod) ∧ (∀x. x ∈ f.dom ⇒ (f.map x = g.map x))))`,
+srw_tac [][morphism_component_equality,IsTypedFun_def,HasFunType_def,extensional_def] >>
+srw_tac [][EQ_IMP_THM] >>
+srw_tac [][FUN_EQ_THM] >>
+Cases_on `x ∈ f.dom` >> srw_tac [][] >>
+pop_assum mp_tac >> srw_tac [][]);
+
val TypedGraphFun_def = Define`
TypedGraphFun (X,Y) f = <|
dom := X; cod := Y; map := restrict f X |>`;
@@ -167,841 +177,113 @@ val _ = export_rewrites[
"ens_cat_composable_in","ens_cat_comp",
"ens_cat_compose_in","ens_cat_maps_to_in"];
-val pre_hom_functor_def = Define`
- (pre_hom_functor c x : ('a,'b,('a,'b) mor set, ('a,'b) mor -> ('a,'b) mor) functor) = <|
- dom := c ; cod := ens_cat UNIV;
- map := λf. TypedGraphFun ((c|x→f.dom|),(c|x→f.cod|)) (λg. f o g -:c)
- |>`;
-
-val pre_hom_functor_dom = Q.store_thm(
-"pre_hom_functor_dom",
-`∀c x. (pre_hom_functor c x).dom = c`,
-srw_tac [][pre_hom_functor_def]);
-
-val pre_hom_functor_cod = Q.store_thm(
-"pre_hom_functor_cod",
-`∀c x. (pre_hom_functor c x).cod = ens_cat UNIV`,
-srw_tac [][pre_hom_functor_def]);
-
-val _ = export_rewrites["pre_hom_functor_cod","pre_hom_functor_dom"];
-
-val pre_hom_functor_morf_dom_cod = Q.store_thm(
-"pre_hom_functor_morf_dom_cod",
-`∀c x f. (((pre_hom_functor c x)##f).dom = c|x→f.dom|) ∧
- (((pre_hom_functor c x)##f).cod = c|x→f.cod|)`,
-srw_tac [][pre_hom_functor_def,morf_def,TypedGraphFun_def]);
-val _ = export_rewrites ["pre_hom_functor_morf_dom_cod"];
-
-val pre_hom_functor_morf = Q.store_thm(
-"pre_hom_functor_morf",
-`∀c x f. (pre_hom_functor c x)##f =
- TypedGraphFun ((c|x→f.dom|), c|x→f.cod|) (λg. f o g -:c)`,
-srw_tac [][pre_hom_functor_def,morf_def]);
-val _ = export_rewrites["pre_hom_functor_morf"];
-
-val pre_hom_functor_objf = Q.store_thm(
-"pre_hom_functor_objf",
-`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj
- ⇒ ((pre_hom_functor c x)@@y = c|x→y|)`,
-srw_tac [][objf_def,pre_hom_functor_def] >>
-imp_res_tac id_dom_cod >>
-SELECT_ELIM_TAC >>
-srw_tac [][] >- (
- qexists_tac `c|x→y|` >>
- srw_tac [][morphism_component_equality,TypedGraphFun_def] >>
- srw_tac [][restrict_def,FUN_EQ_THM] >> srw_tac [][] >>
- fsrw_tac [][hom_def,maps_to_in_def] ) >>
-fsrw_tac [][TypedGraphFun_def,ens_cat_def]);
-val _ = export_rewrites ["pre_hom_functor_objf"];
-
-val _ = add_rule{
- term_name = "hom_functor",
- fixity=Suffix 620,
- pp_elements=[TOK"|",TM,TOK"\226\134\146_|"],
- paren_style=OnlyIfNecessary,
- block_style=(AroundEachPhrase,(PP.INCONSISTENT,0))};
-
-val hom_functor_def = Define`
- c|x→_| = mk_functor (pre_hom_functor c x)`;
-
-val hom_functor_objf = Q.store_thm(
-"hom_functor_objf",
-`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj
- ⇒ (objf (hom_functor c x) y = c|x→y|)`,
-srw_tac [][hom_functor_def]);
-
-val hom_functor_morf = Q.store_thm(
-"hom_functor_morf",
-`∀c x f. f ∈ c.mor ⇒
-((c|x→_|)##f =
- TypedGraphFun ((c|x→f.dom|), c|x→f.cod|) (λg. f o g -:c))`,
-srw_tac [][hom_functor_def,pre_hom_functor_def,mk_functor_def,restrict_def,morf_def]);
-
-val _ = export_rewrites["hom_functor_objf","hom_functor_morf"];
-
-val is_functor_hom_functor = Q.store_thm(
-"is_functor_hom_functor",
-`∀c x. is_category c ∧ x ∈ c.obj ⇒ is_functor (c|x→_|)`,
-srw_tac [][hom_functor_def] >>
-srw_tac [][functor_axioms_def]
->- (
- srw_tac [][hom_def] >>
- match_mp_tac maps_to_comp >>
- qexists_tac `f.dom` >>
- fsrw_tac [][hom_def,maps_to_in_def] )
->- (
- imp_res_tac maps_to_obj >>
- fsrw_tac [][maps_to_in_def] )
->- (
- imp_res_tac maps_to_obj >>
- fsrw_tac [][maps_to_in_def] )
->- (
- srw_tac [][TypedGraphFun_def] >>
- srw_tac [][FUN_EQ_THM,restrict_def] >>
+val ens_cat_empty_terminal = Q.store_thm(
+"ens_cat_empty_terminal",
+`∀U. is_terminal (ens_cat U) ∅ = ∅ ∈ U ∧ ∀x. x ∈ U ⇒ (x = ∅)`,
+srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >- (
+ first_x_assum (qspec_then `x` mp_tac) >>
srw_tac [][] >>
- fsrw_tac [][hom_def,maps_to_in_def] ) >>
-qmatch_abbrev_tac `hh = gg o ff -:(ens_cat U)` >>
-`ff ≈> gg -:(ens_cat U)` by (
- srw_tac [][Abbr`ff`,Abbr`gg`,Abbr`U`,TypedGraphFun_def] >>
- imp_res_tac composable_in_def >> fsrw_tac [][] >>
- fsrw_tac [][hom_def] >>
- metis_tac [maps_to_comp,maps_to_in_dom_cod] ) >>
-srw_tac [][] >>
-`(ff ≈> gg) ∧ f ≈> g` by (
- imp_res_tac composable_in_def >>
+ fsrw_tac [][IsTypedFun_def,HasFunType_def,EXTENSION] )
+>- (
+ qexists_tac `TypedGraphFun (∅,∅) ARB` >>
srw_tac [][] ) >>
-srw_tac [][Abbr`ff`,Abbr`gg`,Abbr`hh`] >>
-srw_tac [][morphism_component_equality] >>
-TRY ( srw_tac [][hom_def,compose_in_def,restrict_def] >> NO_TAC) >>
-srw_tac [][ComposeFun_def] >>
-srw_tac [][restrict_def,FUN_EQ_THM] >>
-srw_tac [][] >- (
- match_mp_tac comp_assoc >>
- fsrw_tac [][hom_def,composable_in_def,maps_to_in_def] ) >>
-qsuff_tac `F` >- srw_tac [][] >>
-qpat_assum `X ∉ Y` mp_tac >> srw_tac [][] >>
-fsrw_tac [][hom_def,comp_mor_dom_cod] >>
-pop_assum mp_tac >> srw_tac [][comp_mor_dom_cod]);
-val _ = export_rewrites["is_functor_hom_functor"];
-
-val hom_functor_dom = Q.store_thm(
-"hom_functor_dom",
-`∀c x. (hom_functor c x).dom = c`,
-srw_tac [][hom_functor_def]);
-
-val hom_functor_cod = Q.store_thm(
-"hom_functor_cod",
-`∀c x. (hom_functor c x).cod = (ens_cat UNIV)`,
-srw_tac [][hom_functor_def]);
-
-val _ = export_rewrites["hom_functor_cod","hom_functor_dom"];
-
-val hom_op_cat = Q.store_thm(
-"hom_op_cat",
-`∀c x y. (c° |x→y|) = IMAGE op_mor (c|y→x|)`,
-srw_tac [][hom_def,EXTENSION] >>
-metis_tac [op_cat_maps_to_in,op_mor_map,op_mor_idem]);
-val _ = export_rewrites["hom_op_cat"];
+srw_tac [][TypedFun_ext]);
-(*
-val contra_functor_def = Define`
- contra_functor G = <| dom := G.dom°; cod := G.cod; map := G.map o op_mor |>`;
-
-val contra_functor_components = Q.store_thm(
-"contra_functor_components",
-`∀G. ((contra_functor G).dom = G.dom°) ∧
- ((contra_functor G).cod = G.cod) ∧
- ((contra_functor G).map = G.map o op_mor)`,
-srw_tac [][contra_functor_def]);
-val _ = export_rewrites["contra_functor_components"];
-
-val contra_functor_morf = Q.store_thm(
-"contra_functor_morf",
-`∀G f. (contra_functor G)##f = G##(f°)`,
-srw_tac [][contra_functor_def,morf_def]);
-
-val contra_functor_objf = Q.store_thm(
-"contra_functor_objf",
-`∀G x. is_category G.dom ∧ x ∈ G.dom.obj ⇒ ((contra_functor G)@@x = G@@x)`,
-srw_tac [][objf_def,contra_functor_def]);
-
-val _ = export_rewrites["contra_functor_morf","contra_functor_objf"];
-
-val extensional_functor_contra_functor = Q.store_thm(
-"extensional_functor_contra_functor",
-`∀G. extensional_functor (contra_functor G) ⇔ extensional_functor G`,
-srw_tac [DNF_ss][extensional_functor_def,extensional_def,EQ_IMP_THM] >- (
- first_x_assum (qspec_then `e°` mp_tac) >>
- srw_tac [][] ) >>
-first_x_assum match_mp_tac >>
-first_x_assum (qspec_then `e°` mp_tac) >>
-srw_tac [][] );
-
-val functor_axioms_contra_functor = Q.store_thm(
-"functor_axioms_contra_functor",
-`∀G. functor_axioms (contra_functor G) ⇔ functor_axioms G`,
-srw_tac [][functor_axioms_def] >> EQ_TAC >> strip_tac >> fsrw_tac [][] >- (
- conj_tac >- (
+val ens_cat_terminal_objects = Q.store_thm(
+"ens_cat_terminal_objects",
+`∀U t. (∃s. s ∈ U ∧ s ≠ ∅) ⇒
+ (is_terminal (ens_cat U) t = ∃x. (t = {x}) ∧ t ∈ U)`,
+srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >>
+srw_tac [][] >- (
+ srw_tac [][EXTENSION] >>
+ Cases_on `t = {}` >- (
+ first_x_assum (qspec_then `s` mp_tac) >>
srw_tac [][] >>
- first_x_assum (qspecl_then [`f°`,`x`,`y`] mp_tac) >>
- imp_res_tac maps_to_obj >>
- srw_tac [][]
-
-val is_functor_contra_functor = Q.store_thm(
-"is_functor_contra_functor",
-`∀G. is_functor (contra_functor G) ⇔ is_functor G`,
-srw_tac [][is_functor_def,extensional_functor_contra_functor,functor_axioms_contra_functor]);
-val _ = export_rewrites["is_functor_contra_functor"];
-*)
-
-val pre_op_mor_functor_def = Define`
- pre_op_mor_functor U = <| dom := ens_cat U; cod := ens_cat U;
- map := λf. TypedGraphFun
- (IMAGE op_mor f.dom, IMAGE op_mor f.cod)
- (op_mor o f.map o op_mor) |>`;
-
-val pre_op_mor_functor_components = Q.store_thm(
-"pre_op_mor_functor_components",
-`∀U. ((pre_op_mor_functor U).dom = ens_cat U) ∧
- ((pre_op_mor_functor U).cod = ens_cat U) ∧
- ((pre_op_mor_functor U).map = λf. TypedGraphFun
- (IMAGE op_mor f.dom, IMAGE op_mor f.cod)
- (op_mor o f.map o op_mor))`,
-srw_tac [][pre_op_mor_functor_def]);
-val _ = export_rewrites["pre_op_mor_functor_components"];
-
-val pre_op_mor_functor_morf = Q.store_thm(
-"pre_op_mor_functor_morf",
-`∀U f. (pre_op_mor_functor U)##f =
- TypedGraphFun (IMAGE op_mor f.dom, IMAGE op_mor f.cod) (op_mor o f.map o op_mor)`,
-srw_tac [][morf_def]);
-val _ = export_rewrites["pre_op_mor_functor_morf"];
-
-val pre_op_mor_functor_objf = Q.store_thm(
-"pre_op_mor_functor_objf",
-`∀U x. x ∈ U ∧ IMAGE op_mor x ∈ U ⇒ ((pre_op_mor_functor U)@@x = IMAGE op_mor x)`,
-srw_tac [][objf_def] >>
-SELECT_ELIM_TAC >>
-conj_tac >- (
- qexists_tac `IMAGE op_mor x` >>
+ disj1_tac >>
+ srw_tac [][] >>
+ Cases_on `f.dom = s` >> srw_tac [][] >>
+ Cases_on `f.cod = ∅` >> srw_tac [][] >>
+ srw_tac [][IsTypedFun_def,HasFunType_def,MEMBER_NOT_EMPTY] ) >>
+ qexists_tac `CHOICE t` >>
+ srw_tac [][EQ_IMP_THM,CHOICE_DEF] >>
+ first_x_assum (qspec_then `t` mp_tac) >>
srw_tac [][] >>
- srw_tac [][morphism_component_equality] >>
- srw_tac [][restrict_def,FUN_EQ_THM] >>
- srw_tac [][] >> fsrw_tac [][] ) >>
-srw_tac [][] >>
-fsrw_tac [][morphism_component_equality]);
-val _ = export_rewrites["pre_op_mor_functor_objf"];
-
-val op_mor_functor_def = Define`
- op_mor_functor U = mk_functor (pre_op_mor_functor U)`;
-
-val is_functor_op_mor_functor = Q.store_thm(
-"is_functor_op_mor_functor",
-`∀U. (∀x. x ∈ U ⇒ IMAGE op_mor x ∈ U) ⇒ is_functor (op_mor_functor U)`,
-srw_tac [][op_mor_functor_def] >>
-srw_tac [][functor_axioms_def] >>
-srw_tac [][] >- fsrw_tac [][IsTypedFun_def,HasFunType_def]
+ qmatch_assum_rename_tac `x ∈ f.cod` [] >>
+ first_x_assum (qspecl_then [`TypedGraphFun (f.dom,f.cod) (K x)`,`TypedGraphFun (f.dom,f.cod) (K (CHOICE f.cod))`] mp_tac) >>
+ srw_tac [][CHOICE_DEF] >>
+ fsrw_tac [][morphism_component_equality,restrict_def] >>
+ qmatch_assum_abbrev_tac `ff = gg` >>
+ `ff x = gg x` by srw_tac [][] >>
+ pop_assum mp_tac >>
+ unabbrev_all_tac >>
+ qpat_assum `x ∈ f.cod` mp_tac >>
+ simp_tac std_ss [] )
>- (
- qexists_tac `IMAGE op_mor x` >>
- srw_tac [][morphism_component_equality] >>
- srw_tac [][restrict_def,FUN_EQ_THM] >>
- srw_tac [][] >> fsrw_tac [][] ) >>
-qmatch_abbrev_tac `hh = gg o ff -: ens_cat U` >>
-`ff ≈> gg -:ens_cat U` by (
- srw_tac [][Abbr`ff`,Abbr`gg`] >>
- fsrw_tac [][IsTypedFun_def,HasFunType_def] ) >>
-srw_tac [][] >>
-srw_tac [][Abbr`gg`,Abbr`ff`,Abbr`hh`,morphism_component_equality] >>
-srw_tac [][ComposeFun_def] >>
-srw_tac [][restrict_def,FUN_EQ_THM] >>
-srw_tac [][] >>
-fsrw_tac [][IsTypedFun_def,HasFunType_def] >>
-metis_tac []);
-val _ = export_rewrites["is_functor_op_mor_functor"];
-
-val op_mor_functor_dom_cod = Q.store_thm(
-"op_mor_functor_dom_cod",
-`∀U. ((op_mor_functor U).dom = ens_cat U) ∧
- ((op_mor_functor U).cod = ens_cat U)`,
-srw_tac [][op_mor_functor_def]);
-val _ = export_rewrites["op_mor_functor_dom_cod"];
-
-val op_mor_functor_morf = Q.store_thm(
-"op_mor_functor_morf",
-`∀U f. IsTypedFunIn U f ⇒ ((op_mor_functor U)##f =
- TypedGraphFun (IMAGE op_mor f.dom, IMAGE op_mor f.cod) (op_mor o f.map o op_mor))`,
-srw_tac [][op_mor_functor_def,mk_functor_def,morphism_component_equality,morf_def,
- restrict_def]);
-val _ = export_rewrites["op_mor_functor_morf"];
-
-val op_mor_functor_objf = Q.store_thm(
-"op_mor_functor_objf",
-`∀U x. x ∈ U ∧ IMAGE op_mor x ∈ U ⇒ ((op_mor_functor U)@@x = IMAGE op_mor x)`,
-srw_tac [][op_mor_functor_def]);
-val _ = export_rewrites["op_mor_functor_objf"];
-
-val _ = add_rule{
- term_name = "contra_hom_functor",
- fixity=Suffix 620,
- pp_elements=[TOK"|_\226\134\146",TM,TOK"|"],
- paren_style=OnlyIfNecessary,
- block_style=(AroundEachPhrase,(PP.INCONSISTENT,0))};
-
-val _ = overload_on("contra_hom_functor",``λc x. (op_mor_functor UNIV) ◎ (hom_functor c° x)``);
-
-val contra_hom_functor_objf = Q.store_thm(
-"contra_hom_functor_objf",
-`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj ⇒ ((c|_→y|)@@x = (c|x→y|))`,
-srw_tac [][] >> srw_tac [DNF_ss][EXTENSION]);
-
-val contra_hom_functor_morf = Q.store_thm(
-"contra_hom_functor_morf",
-`∀c x f. is_category c ∧ f° ∈ c.mor ∧ x ∈ c.obj ⇒
- ((c|_→x|)##f = TypedGraphFun ((c|f.dom→x|), (c|f.cod→x|)) (λg. g o f° -:c))`,
-srw_tac [][] >>
-qabbrev_tac `ff = f° °` >>
-`f = ff` by srw_tac [][Abbr`ff`] >>
-`ff ∈ c°.mor` by (
- srw_tac [][Abbr`ff`] >>
- qexists_tac `f°` >> srw_tac [][] ) >>
-fsrw_tac [][] >> srw_tac [][] >>
-qmatch_abbrev_tac `(op_mor_functor UNIV)##f = g` >>
-`IsTypedFun f` by (
- srw_tac [][Abbr`f`,Abbr`g`] >>
- qmatch_assum_rename_tac `f ∈ (c|g.cod→x|)` [] >>
- qexists_tac `f° ° o g° ° -:c` >>
- `g° ° ≈> f° ° -:c` by (
- match_mp_tac maps_to_composable >>
- srw_tac [][] >> fsrw_tac [][hom_def,maps_to_in_def] ) >>
- conj_tac >- (
- match_mp_tac op_cat_compose_in >>
- srw_tac [][] ) >>
- imp_res_tac composable_maps_to >>
- fsrw_tac [][hom_def] >>
- fsrw_tac [][maps_to_in_def] ) >>
-srw_tac [][Abbr`g`,Abbr`f`,morphism_component_equality] >>
-TRY (srw_tac [DNF_ss][EXTENSION] >> NO_TAC) >>
-srw_tac [][restrict_def,FUN_EQ_THM] >>
-srw_tac [][] >> fsrw_tac [DNF_ss][] >- (
- qmatch_rename_tac `(g° o f° -:c°)° = f o g -:c` [] >>
- qspecl_then [`f`,`g`,`c°`] mp_tac op_cat_compose_in >>
- srw_tac [][] >> pop_assum (match_mp_tac o GSYM) >>
- match_mp_tac maps_to_composable >>
- fsrw_tac [][hom_def,maps_to_in_def] ) >>
-metis_tac [op_mor_idem]);
-val _ = export_rewrites["contra_hom_functor_objf","contra_hom_functor_morf"];
-
-val YfunctorNT_def = Define`
- YfunctorNT c f = mk_nt <|
- dom := c|_→f.dom|; cod := c|_→f.cod|;
- map := λx. (c|x→_|##f) |>`
-
-val YfunctorNT_dom_cod = Q.store_thm(
-"YfunctorNT_dom_cod",
-`∀c f. ((YfunctorNT c f).dom = c|_→f.dom|) ∧
- ((YfunctorNT c f).cod = c|_→f.cod|)`,
-srw_tac [][YfunctorNT_def]);
-val _ = export_rewrites["YfunctorNT_dom_cod"];
-
-val ntdom_YfunctorNT = Q.store_thm(
-"ntdom_YfunctorNT",
-`∀c f. ntdom (YfunctorNT c f) = c°`,
-srw_tac [][YfunctorNT_def,mk_nt_def]);
-
-val ntcod_YfunctorNT = Q.store_thm(
-"ntcod_YfunctorNT",
-`∀c f. ntcod (YfunctorNT c f) = (ens_cat UNIV)`,
-srw_tac [][YfunctorNT_def,mk_nt_def]);
-
-val YfunctorNT_at = Q.store_thm(
-"YfunctorNT_at",
-`∀c f x. x ∈ c.obj ⇒
- ((YfunctorNT c f)@+x = (c|x→_|##f))`,
-srw_tac [][YfunctorNT_def,mk_nt_def,restrict_def]);
-
-val _ = export_rewrites ["ntdom_YfunctorNT","ntcod_YfunctorNT","YfunctorNT_at"];
+ qmatch_assum_rename_tac `y ∈ U` [] >>
+ qexists_tac `TypedGraphFun (y,{x}) (K x)` >>
+ srw_tac [][] ) >>
+srw_tac [][TypedFun_ext] >>
+rpt (qpat_assum `IsTypedFun X` mp_tac) >>
+fsrw_tac [][IsTypedFun_def,HasFunType_def]);
(*
-val HasFunType_postcomp = Q.store_thm(
-"HasFunType_postcomp",
-`∀c f w x y z. is_category c ∧ f :- x → y -:c ∧ (w = z)
- ⇒ HasFunType (λg. g o f -:c) (c|y→z|) (c|x→w|)`,
-
-Problem: (λg. g o f -:c) has a dependent type.
-The type is ∀z. c|y→z| c|x→z|
-It is extensional on the union over all z of c|y→z|
-but depending on which element of the union you came from, the result type can be constrained
+val ens_cat_has_binary_products = Q.store_thm(
+"ens_cat_has_binary_products",
+`∀U J. (INJ J {{(x,y) | x ∈ a ∧ y ∈ b} | a ∈ U ∧ b ∈ U} U) ⇒ has_binary_products (ens_cat U)`,
+srw_tac [][has_binary_products_thm,is_binary_product_thm] >>
+`J {(x,y) | x ∈ a ∧ y ∈ b} ∈ U` by fsrw_tac [DNF_ss][INJ_DEF] >>
+qmatch_assum_abbrev_tac `J axb ∈ U` >>
+qmatch_assum_abbrev_tac `INJ J UU U` >>
+qexists_tac `TypedGraphFun (J axb, a) (λp. (LINV J UU axb)` >>
+LINV_DEF
+srw_tac [][]
+``TypedGraphFun ((J:('a # 'a set -> 'a set)) (a,b), a)``
+``(LINV (J:(('a # 'a) set -> 'a set)) UU)``
+type_of it
*)
-val is_nat_trans_YfunctorNT = Q.store_thm(
-"is_nat_trans_YfunctorNT",
-`∀c f. is_category c ∧ f ∈ c.mor ⇒ is_nat_trans (YfunctorNT c f)`,
-srw_tac [][YfunctorNT_def] >>
-srw_tac [][nat_trans_axioms_def] >- (
- imp_res_tac mor_obj >>
- fsrw_tac [][hom_def] >>
- match_mp_tac maps_to_comp >>
- metis_tac [maps_to_in_def,maps_to_def] ) >>
-qmatch_assum_rename_tac `g° :- y → x -:c` [] >>
-imp_res_tac maps_to_in_def >>
-fsrw_tac [][] >> srw_tac [][] >>
-imp_res_tac mor_obj >> srw_tac [][] >>
-qmatch_abbrev_tac
- `(TypedGraphFun (t2,t3) f2) o (TypedGraphFun (t1,t2) f1) -:ens_cat U =
- (TypedGraphFun (t4,t3) f1) o (TypedGraphFun (t1,t4) f2) -:ens_cat U` >>
-`(∀x. x ∈ t1 ⇒ f1 x ∈ t2) ∧
- (∀x. x ∈ t4 ⇒ f1 x ∈ t3) ∧
- (∀x. x ∈ t2 ⇒ f2 x ∈ t3) ∧
- (∀x. x ∈ t1 ⇒ f2 x ∈ t4)` by (
- unabbrev_all_tac >>
- fsrw_tac [][hom_def] >>
- srw_tac [][] >>
- match_mp_tac maps_to_comp >>
- metis_tac []) >>
-qmatch_abbrev_tac `x o w -:ens_cat U = v o u -:ens_cat U` >>
-`IsTypedFun u ∧ IsTypedFun v ∧ IsTypedFun w ∧ IsTypedFun x` by
- metis_tac [IsTypedFunTypedGraphFun] >>
-`u ∈ (ens_cat U).mor ∧ v ∈ (ens_cat U).mor ∧ w ∈ (ens_cat U).mor ∧ x ∈ (ens_cat U).mor` by
- metis_tac [ens_cat_mor,IN_UNIV] >>
-`u ≈> v -:(ens_cat U)` by (
- srw_tac [][composable_def,Abbr`v`,Abbr`u`,Abbr`U`]) >>
-`w ≈> x -:ens_cat U` by (
- srw_tac [][composable_def,Abbr`x`,Abbr`w`,Abbr`U`]) >>
+val pre_inclusion_functor_def = Define`
+ pre_inclusion_functor u1 u2 = <|
+ dom := ens_cat u1;
+ cod := ens_cat u2;
+ map := I|>`;
+
+val pre_inclusion_functor_components = Q.store_thm(
+"pre_inclusion_functor_components",
+`∀u1 u2. ((pre_inclusion_functor u1 u2).dom = ens_cat u1) ∧
+ ((pre_inclusion_functor u1 u2).cod = ens_cat u2) ∧
+ (∀f. f ∈ (ens_cat u1).mor ⇒ ((pre_inclusion_functor u1 u2)##f = f)) ∧
+ (∀x. x ∈ u1 ∧ x ∈ u2 ⇒ ((pre_inclusion_functor u1 u2)@@x = x))`,
+srw_tac [][pre_inclusion_functor_def,morf_def,objf_def] >>
+SELECT_ELIM_TAC >>
+conj_tac >- ( qexists_tac `x` >> srw_tac [][] ) >>
srw_tac [][] >>
-map_every qunabbrev_tac [`u`,`v`,`w`,`x`] >>
-srw_tac [][ComposeTypedFun_def,TypedGraphFun_def] >>
-srw_tac [][ComposeFun_def] >>
-srw_tac [][restrict_def] >>
-srw_tac [][FUN_EQ_THM] >>
-srw_tac [][Abbr`f1`,Abbr`f2`] >>
-match_mp_tac (GSYM comp_assoc) >>
-qunabbrev_tac `t1` >>
-fsrw_tac [][hom_def] >>
-imp_res_tac maps_to_composable >>
-srw_tac [][]);
-val _ = export_rewrites["is_nat_trans_YfunctorNT"];
-
-val YfunctorNT_maps_to = Q.store_thm(
-"YfunctorNT_maps_to",
-`∀c f. is_category c ∧ f ∈ c.mor ⇒
- (YfunctorNT c f) :- (c|_→f.dom|) → (c|_→f.cod|) -:[(c°)→ens_cat UNIV]`,
-srw_tac [][maps_to_in_def]);
-val _ = export_rewrites["YfunctorNT_maps_to"];
-
-val YfunctorNT_composable = Q.store_thm(
-"YfunctorNT_composable",
-`∀c f g. is_category c ∧ f ≈> g -:c ⇒
- (YfunctorNT c f) ≈> (YfunctorNT c g) -:[(c°)→ens_cat UNIV]`,
-srw_tac [][composable_nts_def] >> fsrw_tac [][composable_in_def]);
-val _ = export_rewrites["YfunctorNT_composable"];
-
-val YfunctorNT_id = Q.store_thm(
-"YfunctorNT_id",
-`∀c x. is_category c ∧ x ∈ c.obj ⇒ (YfunctorNT c (id x -:c) = id_nt (c|_→x|))`,
-srw_tac [][] >> match_mp_tac nt_eq_thm >>
-srw_tac [][id_mor] >>
-srw_tac [][TypedGraphFun_def,restrict_def] >>
-srw_tac [][FUN_EQ_THM] >> srw_tac [][] >>
-fsrw_tac [][hom_def,maps_to_in_def]);
-val _ = export_rewrites["YfunctorNT_id"];
-
-val is_category_presheaf_cat = Q.store_thm(
-"is_category_presheaf_cat",
-`∀c. is_category c ⇒ is_category [(c°)→ens_cat UNIV]`,
-metis_tac [is_category_functor_cat,is_category_ens_cat,is_category_op_cat])
-val _ = export_rewrites["is_category_presheaf_cat"];
-
-val pre_Yfunctor_def = Define`
- pre_Yfunctor c = <|
- dom := c; cod := [(c°)→ens_cat UNIV];
- map := λf. YfunctorNT c f |>`;
-
-val pre_Yfunctor_components = Q.store_thm(
-"pre_Yfunctor_components",
-`∀c. ((pre_Yfunctor c).dom = c) ∧
- ((pre_Yfunctor c).cod = [(c°)→ens_cat UNIV]) ∧
- ((pre_Yfunctor c).map = λf. YfunctorNT c f) ∧
- (∀f. (pre_Yfunctor c)##f = YfunctorNT c f)`,
-srw_tac [][pre_Yfunctor_def,morf_def]);
-val _ = export_rewrites["pre_Yfunctor_components"];
-
-val pre_Yfunctor_objf = Q.store_thm(
-"pre_Yfunctor_objf",
-`∀c x. is_category c ∧ x ∈ c.obj
- ⇒ ((pre_Yfunctor c)@@x = c|_→x|)`,
-srw_tac [][objf_def] >>
-SELECT_ELIM_TAC >> srw_tac [][] >- (
- qexists_tac `c|_→x|` >> srw_tac [][] ) >>
pop_assum mp_tac >>
-srw_tac [][id_in_def] >>
-Q.ISPEC_THEN `[(c°)→ens_cat UNIV]` match_mp_tac id_inj >>
-srw_tac [][]);
-val _ = export_rewrites["pre_Yfunctor_objf"];
-
-val Yfunctor_def = Define`
- Yfunctor c = mk_functor (pre_Yfunctor c)`;
-
-val is_functor_Yfunctor = Q.store_thm(
-"is_functor_Yfunctor",
-`∀c. is_category c ⇒ is_functor (Yfunctor c)`,
-srw_tac [][Yfunctor_def] >>
-srw_tac [][functor_axioms_def,morf_def]
->- (imp_res_tac maps_to_obj >> fsrw_tac [][morf_def,maps_to_in_def])
->- (imp_res_tac maps_to_obj >> fsrw_tac [][morf_def,maps_to_in_def])
->- fsrw_tac [][maps_to_in_def]
->- (qexists_tac `c|_→x|` >> srw_tac [][]) >>
-qspecl_then [`c`,`f`,`g`,`f.dom`,`g.cod`] mp_tac composable_maps_to >>
-srw_tac [][] >>
-imp_res_tac maps_to_in_def >>
-imp_res_tac YfunctorNT_composable >>
-match_mp_tac nt_eq_thm >> fsrw_tac [][] >>
-conj_tac >- ( fsrw_tac [][nt_comp_def,compose_def,mk_nt_def,restrict_def,YfunctorNT_def,composable_in_def]) >>
-conj_tac >- ( fsrw_tac [][nt_comp_def,compose_def,mk_nt_def,restrict_def,YfunctorNT_def,composable_in_def]) >>
-`f ∈ c.mor ∧ g ∈ c.mor` by (
- imp_res_tac composable_in_def >> srw_tac [][]) >>
-srw_tac [][] >>
-qmatch_abbrev_tac
- `h = TypedGraphFun (i,j) k o TypedGraphFun (l,m) n -:ens_cat UNIV` >>
-`(∀x. x ∈ i ⇒ k x ∈ j) ∧ (∀x. x ∈ l ⇒ n x ∈ m)` by (
- unabbrev_all_tac >>
- srw_tac [][hom_def] >>
- match_mp_tac maps_to_comp >>
- metis_tac [maps_to_in_def,maps_to_def] ) >>
-imp_res_tac IsTypedFunTypedGraphFun >>
-imp_res_tac ens_cat_mor >>
-ntac 2 (pop_assum (qspec_then `UNIV` mp_tac)) >>
-`m = i` by (
- fsrw_tac [][composable_in_def,Abbr`m`,Abbr`i`] ) >>
-`(TypedGraphFun (l,m) n) ≈> (TypedGraphFun (i,j) k) -:ens_cat UNIV` by (
- srw_tac [][]) >>
-srw_tac [][Abbr`h`] >>
-srw_tac [][TypedGraphFun_def,ComposeTypedFun_def] >>
-srw_tac [][ComposeFun_def] >>
-srw_tac [][restrict_def] >>
-srw_tac [][FUN_EQ_THM] >>
-unabbrev_all_tac >>
-srw_tac [][] >>
-`g.dom = f.cod` by (
- fsrw_tac [][composable_in_def] ) >>
-match_mp_tac comp_assoc >>
-fsrw_tac [][hom_def] >>
-match_mp_tac maps_to_composable >>
-map_every qexists_tac [`x`,`f.dom`,`f.cod`] >>
+fsrw_tac [][morphism_component_equality]);
+val _ = export_rewrites["pre_inclusion_functor_components"];
+
+val inclusion_functor_def = Define`
+ inclusion_functor u1 u2 = mk_functor (pre_inclusion_functor u1 u2)`;
+
+val inclusion_functor_components = Q.store_thm(
+"inclusion_functor_components",
+`∀u1 u2. ((inclusion_functor u1 u2).dom = ens_cat u1) ∧
+ ((inclusion_functor u1 u2).cod = ens_cat u2) ∧
+ (∀f. f ∈ (ens_cat u1).mor ⇒ ((inclusion_functor u1 u2)##f = f)) ∧
+ (∀x. x ∈ u1 ∧ x ∈ u2 ⇒ ((inclusion_functor u1 u2)@@x = x))`,
+srw_tac [][inclusion_functor_def]);
+val _ = export_rewrites["inclusion_functor_components"];
+
+val is_functor_inclusion_functor = Q.store_thm(
+"is_functor_inclusion_functor",
+`∀u1 u2. u1 ⊆ u2 ⇒ is_functor (inclusion_functor u1 u2)`,
+srw_tac [][inclusion_functor_def] >>
+srw_tac [][functor_axioms_def] >>
+fsrw_tac [][SUBSET_DEF] >- (
+ qexists_tac `x` >> srw_tac [][] ) >>
+`(g o f) ∈ (ens_cat u1).mor` by (
+ srw_tac [][] >> fsrw_tac [][IsTypedFun_def] ) >>
srw_tac [][]);
+val _ = export_rewrites["is_functor_inclusion_functor"];
-val Yfunctor_dom = Q.store_thm(
-"Yfunctor_dom",
-`∀c. (Yfunctor c).dom = c`,
-srw_tac [][Yfunctor_def]);
-
-val Yfunctor_cod = Q.store_thm(
-"Yfunctor_cod",
-`∀c. (Yfunctor c).cod = [(c°)→ens_cat UNIV]`,
-srw_tac [][Yfunctor_def]);
-
-val Yfunctor_objf = Q.store_thm(
-"Yfunctor_objf",
-`∀c x. is_category c ∧ x ∈ c.obj ⇒
- ((Yfunctor c)@@x = c|_→x|)`,
-srw_tac [][Yfunctor_def,mk_functor_objf]);
-
-val Yfunctor_morf = Q.store_thm(
-"Yfunctor_morf",
-`∀c f. is_category c ∧ f ∈ c.mor ⇒
- ((Yfunctor c)##f = YfunctorNT c f)`,
-srw_tac [][Yfunctor_def,morf_def]);
-
-val _ = export_rewrites["Yfunctor_dom","Yfunctor_cod","Yfunctor_objf","Yfunctor_morf"];
-
-val YMap_def = Define`
- YMap c x n = (n@+x).map (id x-:c)`;
-
-val YMapImage = Q.store_thm(
-"YMapImage",
-`∀c x n f. is_category c ∧ is_functor f ∧ is_nat_trans n ∧
- (f :- c° → ens_cat UNIV) ∧ x ∈ c.obj ∧
- (n :- ((Yfunctor c)@@x) → f) ⇒
- (YMap c x n) ∈ (f@@x)`,
-srw_tac [][YMap_def] >>
-`(n @+ x) :- (n.dom @@ x) → (n.cod @@ x) -: n.dom.cod` by (
- fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] ) >>
-pop_assum mp_tac >> srw_tac [][] >>
-ntac 4 (pop_assum mp_tac) >> srw_tac [][] >>
-fsrw_tac [][IsTypedFun_def] >>
-fsrw_tac [][HasFunType_def] >>
-first_x_assum match_mp_tac >>
-srw_tac [][hom_def,id_maps_to]);
-
-val YMapInv_def = Define`
- YMapInv c x f y = mk_nt <|
- dom := (Yfunctor c)@@x;
- cod := f;
- map := λz. TypedGraphFun ((c|z→x|), f@@z)
- (λg. (f##(g°)).map y) |>`;
-
-val YMapInv_at = Q.store_thm(
-"YMapInv_at",
-`∀c x f y z. is_category c ∧ x ∈ c.obj ∧ z ∈ c.obj ⇒
- ((YMapInv c x f y) @+ z =
- TypedGraphFun ((c|z→x|), f@@z)
- (λg. (f##g°).map y))`,
-srw_tac [][YMapInv_def,mk_nt_def,restrict_def]);
-val _ = export_rewrites["YMapInv_at"];
-
-val is_nat_trans_YMapInv = Q.store_thm(
-"is_nat_trans_YMapInv",
-`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat UNIV) ∧
- x ∈ c.obj ∧ y ∈ (f@@x)
- ⇒ is_nat_trans (YMapInv c x f y)`,
-srw_tac [][YMapInv_def] >>
-srw_tac [][nat_trans_axioms_def]
->- (
- qmatch_assum_rename_tac `g ∈ c|u→x|` [] >>
- `g° :- x → u -:(c°)` by fsrw_tac [][hom_def] >>
- `f##g° :- (f@@x) → (f@@u) -:ens_cat UNIV` by (
- match_mp_tac morf_maps_to >>
- map_every qexists_tac [`f.dom`,`x`,`u`] >>
- srw_tac [][] ) >>
- fsrw_tac [][IsTypedFun_def,HasFunType_def] >>
- fsrw_tac [][]) >>
-qmatch_assum_rename_tac `g° :- u → v -:c` [] >>
-imp_res_tac maps_to_in_def >>
-fsrw_tac [][] >>
-qmatch_abbrev_tac
-`(TypedGraphFun (i,j) k) o (TypedGraphFun (l,i) n) -:ens_cat UNIV =
- q o (TypedGraphFun (l,s) h) -:ens_cat UNIV` >>
-`(∀x. x ∈ i ⇒ k x ∈ j) ∧ (∀x. x ∈ l ⇒ h x ∈ s)` by (
- unabbrev_all_tac >> srw_tac [][] >>
- qmatch_assum_abbrev_tac `z ∈ (c|q→x|)` >>
- `f##(z)° :- f@@x → f@@q -:ens_cat UNIV` by (
- match_mp_tac morf_maps_to >>
- fsrw_tac [][hom_def] ) >>
- fsrw_tac [][maps_to_in_def,IsTypedFun_def,HasFunType_def] >>
- fsrw_tac [][]) >>
-`∀x. x ∈ l ⇒ n x ∈ i` by (
- srw_tac [][Abbr`n`,Abbr`i`,Abbr`l`,hom_def] >>
- match_mp_tac maps_to_comp >>
- qexists_tac `g.dom` >>
- srw_tac [SATISFY_ss][]) >>
-`q :- s → j -:ens_cat UNIV` by (
- map_every qunabbrev_tac [`q`,`s`,`j`] >>
- match_mp_tac morf_maps_to >>
- map_every qexists_tac [`f.dom`,`g.dom`,`g.cod`] >>
- srw_tac [][] ) >>
-`IsTypedFun q` by fsrw_tac [][maps_to_in_def] >>
-imp_res_tac maps_to_in_def >>
-srw_tac [][Abbr`k`] >>
-imp_res_tac IsTypedFunTypedGraphFun >>
-`TypedGraphFun (l,s) h ≈> q -: ens_cat UNIV` by (
- fsrw_tac [][Abbr`q`,Abbr`s`,maps_to_in_def] ) >>
-srw_tac [][] >>
-unabbrev_all_tac >>
-fsrw_tac [][ComposeTypedFun_def,compose_def,restrict_def] >>
-srw_tac [][ComposeFun_def] >>
-srw_tac [][restrict_def] >>
-srw_tac [][FUN_EQ_THM] >>
-srw_tac [][hom_def] >>
-Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`g`] mp_tac morf_comp >>
-`e° ≈> g -:c°` by (
- srw_tac [][composable_in_def] >>
- fsrw_tac [][maps_to_in_def] ) >>
-fsrw_tac [][op_cat_compose_in] >>
-Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`g`] mp_tac morf_composable >>
-srw_tac [][ComposeFun_def,restrict_def] >- (
- fsrw_tac [][hom_def] >> metis_tac [] ) >>
-Q.ISPECL_THEN [`f`,`f.dom`,`f.cod`,`e°`,`e.cod`,`e.dom`] mp_tac morf_maps_to >>
-fsrw_tac [][maps_to_in_def] >> srw_tac [][] >>
-fsrw_tac [][]);
-val _ = export_rewrites["is_nat_trans_YMapInv"];
-
-val YMapInvImage = Q.store_thm(
-"YMapInvImage",
-`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat UNIV) ∧
- x ∈ c.obj ∧ y ∈ (f@@x) ⇒
- is_nat_trans (YMapInv c x f y) ∧
- ((YMapInv c x f y) :- (Yfunctor c)@@x → f)`,
-srw_tac [][YMapInv_def]);
-
-val YMap1 = Q.store_thm(
-"YMap1",
-`∀c f x n. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat UNIV) ∧
- x ∈ c.obj ∧ is_nat_trans n ∧ (n :- ((Yfunctor c)@@x) → f) ⇒
- (YMapInv c x f (YMap c x n) = n)`,
-rpt strip_tac >>
-match_mp_tac nt_eq_thm >>
-imp_res_tac YMapImage >>
-imp_res_tac is_nat_trans_YMapInv >>
-srw_tac [][]
->- fsrw_tac [][YMapInv_def]
->- fsrw_tac [][YMapInv_def] >>
-qmatch_rename_tac `X = n @+ z` ["X"] >>
-`z ∈ c.obj` by (
- pop_assum mp_tac >> srw_tac [][YMapInv_def] ) >>
-srw_tac [][] >>
-fsrw_tac [][] >>
-qpat_assum `X = (Yfunctor c)@@x` mp_tac >> srw_tac [][] >>
-`∀z. z ∈ c.obj ⇒ n @+ z :- c|z→x| → (n.cod@@z) -:n.cod.cod` by (
- fsrw_tac [][is_nat_trans_def,nat_trans_axioms_def] >>
- metis_tac [contra_hom_functor_objf] ) >>
-first_assum (qspec_then `z` mp_tac) >>
-first_x_assum (qspec_then `x` mp_tac) >>
-srw_tac [][] >>
-srw_tac [][TypedGraphFun_def,morphism_component_equality] >>
-srw_tac [][restrict_def] >>
-srw_tac [][FUN_EQ_THM] >>
-fsrw_tac [][IsTypedFun_def,HasFunType_def,extensional_def] >>
-srw_tac [][YMap_def] >>
-qmatch_assum_rename_tac `f ∈ c|z→x|` [] >>
-Q.ISPECL_THEN [`n`,`c|_→x|`,`n.cod` ,`n.cod.cod` ,`f°`,`x`,`z`]
- mp_tac naturality >>
-fsrw_tac [][hom_def] >>
-qmatch_abbrev_tac `(f1 o f2 -:ens_cat UNIV = f3 o f4 -:ens_cat UNIV) ⇒ X` >>
-`IsTypedFun f2` by (
- srw_tac [][Abbr`f2`] >>
- imp_res_tac maps_to_in_def >>
- srw_tac [][hom_def] >>
- match_mp_tac maps_to_comp >>
- qexists_tac `x` >>
- fsrw_tac [][maps_to_in_def]) >>
-`f1 :- f1.dom → f1.cod -:ens_cat UNIV` by (
- qunabbrev_tac `f1` >>
- match_mp_tac nt_at_maps_to >>
- srw_tac [][hom_def] ) >>
-`f4 :- f4.dom → f4.cod -:ens_cat UNIV` by (
- qunabbrev_tac `f4` >>
- match_mp_tac nt_at_maps_to >>
- srw_tac [][hom_def] ) >>
-`(n.cod##f°) :- n.cod@@x → n.cod@@z -:n.cod.cod` by (
- match_mp_tac morf_maps_to >>
- fsrw_tac [][] >>
- map_every qexists_tac [`x`,`z`] >>
- srw_tac [][] ) >>
-`f3 :- f3.dom → f3.cod -:ens_cat UNIV` by (
- qunabbrev_tac `f3` >>
- match_mp_tac morf_maps_to >>
- srw_tac [][] >>
- map_every qexists_tac [`x`,`z`] >>
- srw_tac [][] >>
- fsrw_tac [][maps_to_in_def] ) >>
-imp_res_tac maps_to_in_def >>
-`f2 ≈> f1 -:ens_cat UNIV` by (
- fsrw_tac [][Abbr`f2`,hom_def] >>
- srw_tac [][] >>
- match_mp_tac maps_to_comp >>
- srw_tac [SATISFY_ss][] ) >>
-`f4 ≈> f3 -:ens_cat UNIV` by (
- fsrw_tac [][Abbr`f3`] ) >>
-`n.cod@@z = f3.cod` by (
- fsrw_tac [][maps_to_in_def,Abbr`f3`] ) >>
-`f2.dom = f4.dom` by (
- fsrw_tac [][Abbr`f4`,Abbr`f2`,hom_def] ) >>
-`f2.map (id f.cod -:c) = f` by (
- srw_tac [][Abbr`f2`] >>
- srw_tac [][restrict_def,hom_def] >>
- fsrw_tac [][] >> srw_tac [][] >>
- pop_assum mp_tac >> srw_tac [][id_maps_to] ) >>
-fsrw_tac [][ComposeTypedFun_def,compose_def,restrict_def,ComposeFun_def] >>
-srw_tac [][FUN_EQ_THM] >>
-pop_assum (qspec_then `id f.cod -:c` mp_tac) >>
-fsrw_tac [][id_maps_to]);
-
-val YMap2 = Q.store_thm(
-"YMap2",
-`∀c x f y. is_category c ∧ is_functor f ∧ (f :- c° → ens_cat UNIV) ∧
- x ∈ c.obj ∧ y ∈ (f@@x) ⇒
- (YMap c x (YMapInv c x f y) = y)`,
-srw_tac [][YMap_def] >>
-srw_tac [][restrict_def,hom_def] >>
-pop_assum mp_tac >> srw_tac [][id_maps_to] >>
-`f##(id x -:(c°)) = id (f@@x) -: ens_cat UNIV` by srw_tac [][morf_id] >>
-fsrw_tac [][] >>
-srw_tac [][restrict_def]);
-
-val YfunctorNT_YMapInv = Q.store_thm(
-"YfunctorNT_YMapInv",
-`∀c f x y. is_category c ∧ f :- x → y -:c ⇒
- (YfunctorNT c f = YMapInv c x (c|_→y|) f)`,
-srw_tac [][] >>
-match_mp_tac nt_eq_thm >>
-imp_res_tac maps_to_in_def >>
-imp_res_tac maps_to_obj >>
-fsrw_tac [][] >>
-conj_tac >- (
- match_mp_tac is_nat_trans_YMapInv >>
- srw_tac [][hom_def] ) >>
-conj_tac >- srw_tac [][YfunctorNT_def,YMapInv_def] >>
-conj_tac >- srw_tac [][YfunctorNT_def,YMapInv_def] >>
-srw_tac [][TypedGraphFun_def] >>
-srw_tac [][restrict_def] >>
-srw_tac [][FUN_EQ_THM] >>
-srw_tac [][hom_def] >>
-imp_res_tac maps_to_in_def >>
-srw_tac [][restrict_def] >>
-fsrw_tac [][hom_def,maps_to_in_def] >>
-fsrw_tac [][]);
-
-val YMapYoneda = Q.store_thm(
-"YMapYoneda",
-`∀c f x y. is_category c ∧ f :- x → y -:c ⇒
- ((Yfunctor c)##f = YMapInv c x ((Yfunctor c)@@y) f)`,
-srw_tac [][] >>
-imp_res_tac maps_to_in_def >>
-imp_res_tac maps_to_obj >>
-srw_tac [][YfunctorNT_YMapInv]);
-
-val YonedaFull = Q.store_thm(
-"YonedaFull",
-`∀c. is_category c ⇒ full (Yfunctor c)`,
-srw_tac [][full_def] >>
-qexists_tac `YMap c a h` >>
-`YMap c a h ∈ (c|_→b|)@@a` by (
- match_mp_tac YMapImage >>
- imp_res_tac Yfunctor_objf >>
- fsrw_tac [][] ) >>
-pop_assum mp_tac >> srw_tac [][contra_hom_functor_objf,hom_def] >>
-match_mp_tac EQ_TRANS >>
-qexists_tac `YMapInv c a (Yfunctor c@@b) (YMap c a h)` >>
-conj_tac >- srw_tac [][YMapYoneda] >>
-match_mp_tac YMap1 >>
-fsrw_tac [][]);
-
-val YonedaFaithful = Q.store_thm(
-"YonedaFaithful",
-`∀c. is_category c ⇒ faithful (Yfunctor c)`,
-srw_tac [][faithful_def] >>
-`YMap c a (YMapInv c a (c|_→b|) g) =
- YMap c a (YMapInv c a (c|_→b|) h)`
- by metis_tac [maps_to_in_def,Yfunctor_morf,YfunctorNT_YMapInv] >>
-match_mp_tac EQ_TRANS >>
-qexists_tac `YMap c a (YMapInv c a (c|_→b|) g)` >>
-conj_tac >- (
- match_mp_tac EQ_SYM >>
- match_mp_tac YMap2 >>
- imp_res_tac maps_to_obj >>
- fsrw_tac [][hom_def] ) >>
-srw_tac [][] >>
-match_mp_tac YMap2 >>
-imp_res_tac maps_to_obj >>
-fsrw_tac [][hom_def]);
-
-val YonedaEmbedding = Q.store_thm(
-"YonedaEmbedding",
-`∀c. is_category c ⇒ embedding (Yfunctor c)`,
-srw_tac [][embedding_def,YonedaFaithful,YonedaFull]);
-
-val YonedaInjObj = Q.store_thm(
-"YonedaInjObj",
-`∀c. is_category c ⇒ inj_obj (Yfunctor c)`,
-srw_tac [][inj_obj_def] >>
-srw_tac [][] >> pop_assum mp_tac >> srw_tac [][] >>
-`(c|_→a|)@@a = (c|_→b|)@@a` by asm_simp_tac std_ss [] >>
-pop_assum mp_tac >>
-pop_assum (K ALL_TAC) >>
-srw_tac [][EXTENSION] >>
-pop_assum (qspec_then `id a -:c` mp_tac) >>
-srw_tac [][hom_def,id_maps_to] >>
-fsrw_tac [][maps_to_in_def] >>
-imp_res_tac id_maps_to >>
-fsrw_tac [][maps_to_in_def]);
-
-val _ = export_theory ();
+val _ = export_theory();
354 examples/category/functorScript.sml
View
@@ -1,9 +1,9 @@
-open HolKernel Parse boolLib bossLib lcsymtacs categoryTheory;
+open HolKernel Parse boolLib bossLib pred_setTheory categoryTheory lcsymtacs;
val _ = new_theory "functor";
val _ = type_abbrev("functor",
-``:(('a,'b) category, ('c,'d) category, ('a,'b) mor -> ('c,'d) mor)
+``:((α,β) category, (γ,δ) category, (α,β) mor -> (γ,δ) mor)
morphism``)
val _ = add_rule {
@@ -39,7 +39,7 @@ val extensional_functor_def = Define`
extensional_functor f = extensional f.map f.dom.mor`;
val mk_functor_def = Define`
- mk_functor (f:('a,'b,'c,'d) functor) =
+ mk_functor (f:(α,β,γ,δ) functor) =
<| dom := f.dom; cod := f.cod; map := restrict f.map f.dom.mor |>`;
val is_functor_def = Define`
@@ -285,7 +285,7 @@ SELECT_ELIM_TAC >>
fsrw_tac [][morf_def]);
val functor_comp_def = Define`
- functor_comp (f:('c,'d,'e,'f) functor) (g:('a,'b,'c,'d) functor) =
+ functor_comp (f:(γ,δ,ε,ζ) functor) (g:(α,β,γ,δ) functor) =
mk_functor (compose (λf g. g.map o f.map) g f)`;
val _ = set_fixity "\226\151\142" (Infixr 800);
@@ -408,10 +408,19 @@ match_mp_tac morf_composable >>
metis_tac [maps_to_def]);
val _ = export_rewrites["is_functor_comp"];
-val functor_comp_id_functor = Q.store_thm(
-"functor_comp_id_functor",
-`∀f c. (is_functor f ∧ (c = f.dom) ⇒ (f ◎ id_functor c = f)) ∧
- (is_functor f ∧ (c = f.cod) ⇒ (id_functor c ◎ f = f))`,
+val functor_comp_id_functor1 = Q.store_thm(
+"functor_comp_id_functor1",
+`∀f c. (is_functor f ∧ (c = f.dom) ⇒ (f ◎ id_functor c = f))`,
+srw_tac [][morphism_component_equality] >>
+srw_tac [][functor_comp_def,mk_functor_def,restrict_def] >>
+srw_tac [][FUN_EQ_THM] >> srw_tac [][] >>
+imp_res_tac is_functor_def >>
+imp_res_tac extensional_functor_def >>
+fsrw_tac [][extensional_def]);
+
+val functor_comp_id_functor2 = Q.store_thm(
+"functor_comp_id_functor2",
+`∀f c. (is_functor f ∧ (c = f.cod) ⇒ (id_functor c ◎ f = f))`,
srw_tac [][morphism_component_equality] >>
srw_tac [][functor_comp_def,mk_functor_def,restrict_def] >>
srw_tac [][FUN_EQ_THM] >> srw_tac [][] >>
@@ -433,6 +442,9 @@ qmatch_assum_rename_tac `x ∈ h.dom.mor` [] >>
Q.ISPECL_THEN [`h`,`h.dom`,`h.cod`,`x`,`x.dom`,`x.cod`,`h@@x.dom`,`h@@x.cod`] mp_tac morf_maps_to >>
srw_tac [][maps_to_in_def]);
+val _ = export_rewrites[
+"functor_comp_id_functor1","functor_comp_id_functor2","functor_comp_assoc"];
+
val functor_preserves_iso_pair = Q.store_thm(
"functor_preserves_iso_pair",
`∀G f g c1 c2. is_functor G ∧ (G :- c1 → c2) ∧ iso_pair c1 f g ⇒ iso_pair c2 (G##f) (G##g)`,
@@ -475,17 +487,22 @@ val full_def = Define`
(f##g = h)`;
val faithful_def = Define`
- faithful (f:('a,'b,'c,'d)functor) =
+ faithful (f:(α,β,γ,δ)functor) =
∀g h a b. g :- a → b -:f.dom ∧ h :- a → b -:f.dom ∧
(f##g = f##h) ⇒ (g = h)`;
val embedding_def = Define`
- embedding (f:('a,'b,'c,'d)functor) = full f ∧ faithful f`;
+ embedding (f:(α,β,γ,δ)functor) = full f ∧ faithful f`;
val inj_obj_def = Define`
inj_obj f = ∀a b. a ∈ f.dom.obj ∧ b ∈ f.dom.obj ∧
(f@@a = f@@b) ⇒ (a = b)`;
+val inj_obj_INJ = Q.store_thm(
+"inj_obj_INJ",
+`∀f. is_functor f ⇒ (inj_obj f = INJ (objf f) f.dom.obj f.cod.obj)`,
+srw_tac [][INJ_DEF,inj_obj_def,objf_in_obj] >> metis_tac []);
+
val ess_inj_obj_def = Define`
ess_inj_obj f = ∀a b. a ∈ f.dom.obj ∧ b ∈ f.dom.obj ∧
(f@@a = f@@b) ⇒ (a ≅ b -:f.dom)`;
@@ -535,6 +552,305 @@ qspecl_then [`f`,`f.dom`,`f.cod`,`ab`,`ba`] mp_tac morf_comp >>
qspecl_then [`f`,`f.dom`,`f.cod`,`a`] mp_tac morf_id >>
fsrw_tac [][objf_in_obj]);
+val full_functor_comp = Q.store_thm(
+"full_functor_comp",
+`∀f g. is_functor f ∧ is_functor g ∧ (f ≈> g) ∧ full f ∧ full g ⇒ full (g ◎ f)`,
+srw_tac [][full_def] >>
+metis_tac [composable_def,functor_comp_morf,maps_to_in_def,objf_in_obj,functor_comp_objf]);
+
+val faithful_functor_comp = Q.store_thm(
+"faithful_functor_comp",
+`∀f g. is_functor f ∧ is_functor g ∧ (f ≈> g) ∧ faithful f ∧ faithful g ⇒ faithful (g ◎ f)`,
+srw_tac [][faithful_def] >>
+qmatch_rename_tac `h1 = h2` [] >>
+pop_assum mp_tac >> fsrw_tac [][maps_to_in_def] >> strip_tac >>
+first_x_assum match_mp_tac >> fsrw_tac [][] >>
+first_x_assum match_mp_tac >> fsrw_tac [][] >>
+`f##h1 :- f@@a → f@@b -:f.cod` by (
+ match_mp_tac morf_maps_to >>
+ metis_tac [maps_to_in_def,maps_to_def] ) >>
+`f##h2 :- f@@a → f@@b -:f.cod` by (
+ match_mp_tac morf_maps_to >>
+ metis_tac [maps_to_in_def,maps_to_def] ) >>
+metis_tac [maps_to_in_def,maps_to_def]);
+
+val embedding_functor_comp = Q.store_thm(
+"embedding_functor_comp",
+`∀f g. is_functor f ∧ is_functor g ∧ (f ≈> g) ∧ embedding f ∧ embedding g ⇒ embedding (g ◎ f)`,
+metis_tac [embedding_def,full_functor_comp,faithful_functor_comp]);
+
+val inj_obj_functor_comp = Q.store_thm(
+"inj_obj_functor_comp",
+`∀f g. is_functor f ∧ is_functor g ∧ (f ≈> g) ∧ inj_obj f ∧ inj_obj g ⇒ inj_obj (g ◎ f)`,
+srw_tac [][inj_obj_def] >>
+pop_assum mp_tac >> srw_tac [][] >>
+metis_tac [objf_in_obj]);
+
+(* Wish we could define a category where this was just iso_pair *)
+(* Joy of Cats says that would be a quasicategory (see p 40 onwards) *)
+val cat_iso_pair_def = Define`
+ cat_iso_pair f g =
+ is_functor f ∧ is_functor g ∧ (f ≈> g) ∧
+ (f ◎ g = id_functor g.dom) ∧
+ (g ◎ f = id_functor f.dom)`;
+
+val id_on_def = Define`
+ id_on id_map x = <|dom := x; cod := x; map:= id_map x|>`;
+
+val gen_iso_pair_def = Define`
+ gen_iso_pair mor1 mor2 comp1 comp2 id_map1 id_map2 f g =
+ f ∈ mor1 ∧ g ∈ mor2 ∧ (f ≈> g) ∧
+ (compose comp1 f g = id_on id_map1 f.dom) ∧
+ (compose comp2 g f = id_on id_map2 g.dom)`;
+
+val gcat_iso_pair_def = Define`
+ gcat_iso_pair = gen_iso_pair
+ {f | is_functor f} {g | is_functor g}
+ (λf g. (g ◎ f).map) (λf g. (g ◎ f).map)
+ (λx. (id_functor x).map) (λy. (id_functor y).map)`;
+
+val gcat_iso_pair_eq_cat_iso_pair = Q.store_thm(
+"gcat_iso_pair_eq_cat_iso_pair",
+`gcat_iso_pair = cat_iso_pair`,
+srw_tac [][FUN_EQ_THM,gcat_iso_pair_def,cat_iso_pair_def,gen_iso_pair_def] >>
+EQ_TAC >> strip_tac >> fsrw_tac [][] >>
+ntac 2 (pop_assum mp_tac) >>
+fsrw_tac [][id_on_def,id_functor_def,functor_comp_def,mk_functor_def]);
+
+(* the types are still general in the above theorem!
+ maybe use gen_iso_pair (and other generic definitions) earlier/throughout? *)
+
+val cat_iso_pair_sym = Q.store_thm(
+"cat_iso_pair_sym",
+`∀f g. cat_iso_pair f g = cat_iso_pair g f`,
+metis_tac [cat_iso_pair_def,id_functor_dom,id_functor_cod,
+ functor_comp_dom_cod,composable_def]);
+
+val cat_iso_def = Define`
+ cat_iso f = ∃g. cat_iso_pair f g`;
+
+val iso_pair_between_cats_def = Define`
+ iso_pair_between_cats c f g d = (f :- c → d) ∧ cat_iso_pair f g`;
+
+val iso_cats_def = Define`
+ iso_cats c d = ∃f g. iso_pair_between_cats c f g d`;
+
+val cat_iso_pair_bij = Q.store_thm(
+"cat_iso_pair_bij",
+`∀f g. cat_iso_pair f g =
+ is_functor f ∧ is_functor g ∧ (f ≈> g) ∧ (g ≈> f) ∧
+ BIJ (objf f) f.dom.obj f.cod.obj ∧
+ (∀x. x ∈ g.dom.obj ⇒ (LINV (objf f) f.dom.obj x = g@@x)) ∧
+ ∀a b. a ∈ f.dom.obj ∧ b ∈ f.dom.obj ⇒
+ BIJ (morf f) (hom f.dom a b) (hom f.cod (f@@a) (f@@b)) ∧
+ (∀h. h ∈ (hom g.dom (f@@a) (f@@b)) ⇒ (LINV (morf f) (hom f.dom a b) h = g##h))`,
+map_every qx_gen_tac [`f`,`g`] >>
+EQ_TAC >> strip_tac >- (
+ fsrw_tac [][cat_iso_pair_def] >>
+ `g.cod = f.dom` by (
+ rpt (qpat_assum `X = id_functor Y` mp_tac) >>
+ fsrw_tac [][morphism_component_equality] ) >>
+ fsrw_tac [][] >>
+ conj_asm1_tac >- (
+ srw_tac [][BIJ_IFF_INV] >- metis_tac [objf_in_obj] >>
+ qexists_tac `objf g` >>
+ conj_tac >- metis_tac [objf_in_obj] >>
+ srw_tac [][] >- (
+ `(g ◎ f)@@x = (id_functor f.dom)@@x` by metis_tac [] >>
+ pop_assum mp_tac >> srw_tac [][is_functor_is_category] ) >>
+ `(f ◎ g)@@x = (id_functor g.dom)@@x` by metis_tac [] >>
+ pop_assum mp_tac >> srw_tac [][is_functor_is_category] ) >>
+ conj_tac >- (
+ srw_tac [][] >>
+ `f@@(LINV (objf f) f.dom.obj x) = x` by metis_tac [BIJ_LINV_INV] >>
+ `f@@(g@@x) = x` by metis_tac [functor_comp_objf,composable_def,id_functor_objf,is_functor_is_category] >>
+ `INJ (objf f) f.dom.obj g.dom.obj` by fsrw_tac [][BIJ_DEF] >>
+ fsrw_tac [][INJ_DEF] >>
+ first_x_assum (match_mp_tac o MP_CANON) >>
+ fsrw_tac [][] >>
+ conj_tac >- metis_tac [BIJ_LINV_BIJ,BIJ_DEF,INJ_DEF] >>
+ metis_tac [objf_in_obj] ) >>
+ rpt gen_tac >> strip_tac >> conj_asm1_tac >- (
+ srw_tac [][BIJ_IFF_INV,hom_def] >- metis_tac [maps_to_def,morf_maps_to] >>
+ qexists_tac `morf g` >>
+ conj_tac >- (
+ srw_tac [][] >>
+ match_mp_tac morf_maps_to >>
+ map_every qexists_tac [`g.dom`,`f@@a`,`f@@b`] >>
+ fsrw_tac [][] >>
+ `(g ◎ f)@@a = (id_functor f.dom)@@a` by metis_tac [] >>
+ pop_assum mp_tac >> srw_tac [][is_functor_is_category] >>
+ `(g ◎ f)@@b = (id_functor f.dom)@@b` by metis_tac [] >>
+ pop_assum mp_tac >> srw_tac [][is_functor_is_category] ) >>
+ conj_tac >- (
+ srw_tac [][] >>
+ `(g ◎ f)##x = (id_functor f.dom)##x` by metis_tac [] >>
+ pop_assum mp_tac >> fsrw_tac [][maps_to_in_def] ) >>
+ srw_tac [][] >>
+ `(f ◎ g)##x = (id_functor g.dom)##x` by metis_tac [] >>
+ pop_assum mp_tac >> fsrw_tac [][maps_to_in_def] ) >>
+ srw_tac [][] >>
+ `f##(LINV (morf f) (f.dom|a→b|)) h = h` by metis_tac [BIJ_LINV_INV] >>
+ `h ∈ g.dom.mor` by fsrw_tac [][hom_def,maps_to_in_def] >>
+ `f##(g##h) = h` by metis_tac [functor_comp_morf,id_functor_morf,composable_def] >>
+ `INJ (morf f) (f.dom|a→b|) (g.dom|f@@a→f@@b|)` by fsrw_tac [][BIJ_DEF] >>
+ fsrw_tac [][INJ_DEF] >>
+ first_x_assum (match_mp_tac o MP_CANON) >>
+ fsrw_tac [][] >>
+ conj_tac >- metis_tac [BIJ_LINV_BIJ,BIJ_DEF,INJ_DEF] >>
+ srw_tac [][hom_def] >>
+ match_mp_tac morf_maps_to >>
+ map_every qexists_tac [`g.dom`,`f@@a`,`f@@b`] >>
+ fsrw_tac [][hom_def] >>
+ metis_tac [functor_comp_objf,composable_def,id_functor_objf,is_functor_is_category] ) >>
+fsrw_tac [][cat_iso_pair_def] >>
+imp_res_tac is_functor_is_category >>
+conj_asm1_tac >>
+match_mp_tac functor_eq_thm >>
+fsrw_tac [][] >> srw_tac [][] >- (
+ `h.dom ∈ g.dom.obj ∧ h.cod ∈ g.dom.obj` by metis_tac[mor_obj] >>
+ `g@@h.dom ∈ f.dom.obj ∧ g@@h.cod ∈ f.dom.obj` by metis_tac [objf_in_obj] >>
+ first_x_assum (qspecl_then [`g@@(h.dom)`,`g@@(h.cod)`] mp_tac) >>
+ fsrw_tac [][] >> strip_tac >>
+ `f@@(g@@h.dom) = h.dom` by metis_tac [BIJ_LINV_INV] >>
+ `f@@(g@@h.cod) = h.cod` by metis_tac [BIJ_LINV_INV] >>
+ first_x_assum (qspec_then `h` mp_tac) >>
+ qmatch_assum_abbrev_tac `BIJ (morf f) hm1 hm2` >>
+ `h ∈ hm2` by fsrw_tac [][hom_def,Abbr`hm2`] >>
+ metis_tac [BIJ_LINV_INV] ) >>
+`(f ◎ g)##(f##h) = (id_functor g.dom)##(f##h)` by srw_tac [][] >>
+qpat_assum `f ◎ g = X` (K ALL_TAC) >>
+`f##h :- f@@h.dom → f@@h.cod -:g.dom` by (
+ metis_tac [morf_maps_to,maps_to_def,maps_to_in_def] ) >>
+imp_res_tac maps_to_in_def >>
+qpat_assum `(f ◎ g)##X = Y` mp_tac >>
+fsrw_tac [][functor_comp_morf] >>
+imp_res_tac maps_to_obj >>
+qsuff_tac `(h ∈ f.dom|h.dom→h.cod|) ∧ (g##(f##h)) ∈ f.dom|h.dom→h.cod|` >- (
+ first_x_assum (qspecl_then [`h.dom`,`h.cod`] mp_tac) >>
+ first_x_assum (qspecl_then [`h.dom`,`h.cod`] mp_tac) >>
+ first_x_assum (qspecl_then [`h.dom`,`h.cod`] mp_tac) >>
+ fsrw_tac [][BIJ_DEF,INJ_DEF] ) >>
+fsrw_tac [][hom_def] >>
+match_mp_tac morf_maps_to >>
+map_every qexists_tac [`g.dom`,`f@@h.dom`,`f@@h.cod`] >>
+fsrw_tac [][] >>
+metis_tac [LINV_DEF,BIJ_DEF]);
+
+val cat_iso_bij = Q.store_thm(
+"cat_iso_bij",
+`∀f. cat_iso f =
+ is_functor f ∧
+ BIJ (objf f) f.dom.obj f.cod.obj ∧
+ ∀a b. a ∈ f.dom.obj ∧ b ∈ f.dom.obj ⇒
+ BIJ (morf f) (f.dom|a→b|) (f.cod|f@@a→f@@b|)`,
+strip_tac >> EQ_TAC >> strip_tac >- (
+ fsrw_tac [][cat_iso_def,cat_iso_pair_bij] ) >>
+fsrw_tac [][cat_iso_def] >>
+fsrw_tac [][BIJ_IFF_INV] >>
+fsrw_tac [][GSYM RIGHT_EXISTS_IMP_THM, GSYM RIGHT_EXISTS_AND_THM] >>
+fsrw_tac [][SKOLEM_THM] >>
+qmatch_assum_rename_tac `∀x. x ∈ f.cod.obj ⇒ gob x ∈ f.dom.obj` [] >>
+pop_assum mp_tac >>
+qho_match_abbrev_tac `(∀a b. P1 a b ⇒ P2 a b ∧ P3 a b ∧ (∀x. x ∈ (f.dom|a→b|) ⇒ (gmo a b (f##x) = x)) ∧ P4 a b) ⇒ P5` >>
+qpat_assum `Abbrev (gmo = X)` (K ALL_TAC) >>
+unabbrev_all_tac >> srw_tac [][] >>
+fsrw_tac [boolSimps.DNF_ss][] >>
+ntac 4 (pop_assum (mp_tac o MP_CANON)) >>
+srw_tac [][hom_def] >>
+qabbrev_tac `g = <|dom:=f.cod; cod:=f.dom; map:=λh. gmo (gob h.dom) (gob h.cod) h|>` >>
+`∀h a b. (h :- a → b) ⇒ (g##h = gmo (gob a) (gob b) h)` by (
+ srw_tac [][morf_def,Abbr`g`] ) >>
+`(g.dom = f.cod) ∧ (g.cod = f.dom)` by srw_tac [][Abbr`g`] >>
+imp_res_tac is_functor_is_category >>
+`∀h a b. (h :- a → b -:f.cod) ⇒ (g##h :- gob a → gob b -:g.cod)` by (
+ rpt gen_tac >>
+ strip_tac >>
+ imp_res_tac maps_to_in_def >>
+ first_x_assum (qspecl_then [`h`,`a`,`b`] mp_tac) >>
+ fsrw_tac [][] >> rpt strip_tac >>
+ first_x_assum match_mp_tac >>
+ metis_tac [maps_to_obj,maps_to_in_def,maps_to_def] ) >>
+`∀x. x ∈ f.cod.obj ⇒ (g##id x -:f.cod = id (gob x) -:f.dom)` by (
+ srw_tac [][] >>
+ `g##id x-:f.cod = gmo (gob x) (gob x) (id x-:f.cod)` by (
+ first_x_assum match_mp_tac >>
+ Q.ISPECL_THEN [`f.cod`,`x`] mp_tac id_maps_to >>
+ srw_tac [][maps_to_in_def] ) >>
+ srw_tac [][] >>
+ `id x -:f.cod = f##(id gob x -:f.dom)` by (
+ metis_tac [morf_id,maps_to_def] ) >>
+ srw_tac [][] ) >>
+`∀x. x ∈ f.cod.obj ⇒ (g@@x = gob x)` by (
+ srw_tac [][objf_def] >>
+ SELECT_ELIM_TAC >>
+ srw_tac [][] >- (
+ qexists_tac `gob x` >> srw_tac [][] ) >>
+ match_mp_tac id_inj >>
+ qexists_tac `f.dom` >>
+ srw_tac [][] ) >>
+`∀h a b. h :- a → b -:f.cod ⇒ (f##(g##h) = h)` by (
+ srw_tac [][] >>
+ imp_res_tac maps_to_in_def >>
+ fsrw_tac [][] >>
+ first_x_assum match_mp_tac >>
+ imp_res_tac maps_to_obj >>
+ fsrw_tac [][] ) >>
+`∀h a b. h :- a → b -:f.dom ⇒ (g##(f##h) = h)` by (
+ srw_tac [][] >>
+ imp_res_tac maps_to_obj >>
+ fsrw_tac [][] >>
+ first_x_assum match_mp_tac >>
+ `f##h :- f@@a → f@@b -:f.cod` by (
+ match_mp_tac morf_maps_to >>
+ metis_tac [maps_to_def] ) >>
+ imp_res_tac maps_to_in_def >>
+ fsrw_tac [][] ) >>
+`is_functor (mk_functor g)` by (
+ srw_tac [][functor_axioms_def] >- (
+ imp_res_tac maps_to_obj >>
+ imp_res_tac maps_to_in_def >>
+ fsrw_tac [][] )
+ >- ( qexists_tac `gob x` >> fsrw_tac [][] ) >>
+ qmatch_assum_rename_tac `k ≈> j -:f.cod` [] >>
+ `(g##k) ≈> (g##j) -:f.dom` by (
+ match_mp_tac maps_to_composable >>
+ metis_tac [composable_in_def,composable_def,maps_to_in_def,maps_to_def] ) >>
+ `f##((g##j) o (g##k) -:f.dom) = (f##(g##j)) o (f##(g##k)) -:f.cod` by (
+ match_mp_tac morf_comp >> srw_tac [][] ) >>
+ `(f##(g##j)) o (f##(g##k)) -:f.cod = j o k -:f.cod` by
+ metis_tac [composable_in_def,maps_to_in_def,composable_def,maps_to_def] >>
+ qsuff_tac `∃a b. (g##j) o (g##k) -:f.dom :- a → b -:f.dom` >- metis_tac [] >>
+ map_every qexists_tac [`(g##k).dom`,`(g##j).cod`] >>
+ match_mp_tac composable_maps_to >> srw_tac [][] ) >>
+srw_tac [][cat_iso_pair_def] >>
+qexists_tac `mk_functor g` >>
+fsrw_tac [][] >>
+conj_tac >> match_mp_tac functor_eq_thm >>
+srw_tac [][] >>
+qsuff_tac `mk_functor g##(f##h) = g##f##h` >- (
+ simp_tac std_ss [] >>
+ strip_tac >> first_x_assum match_mp_tac >>
+ metis_tac [maps_to_def,maps_to_in_def] ) >>
+match_mp_tac mk_functor_morf >>
+metis_tac [morf_mor_dom_cod]);
+
+val cat_iso_embedding = Q.store_thm(
+"cat_iso_embedding",
+`∀f. cat_iso f ⇒ embedding f`,
+srw_tac [][cat_iso_bij,embedding_def,full_def,faithful_def] >>
+first_x_assum (qspecl_then [`a`,`b`] mp_tac) >>
+imp_res_tac is_functor_is_category >>
+imp_res_tac maps_to_obj >>
+srw_tac [][BIJ_DEF,INJ_DEF,SURJ_DEF,hom_def]);
+val _ = export_rewrites["cat_iso_embedding"];
+
+val cat_iso_inj_obj = Q.store_thm(
+"cat_iso_inj_obj",
+`∀f. cat_iso f ⇒ inj_obj f`,
+srw_tac [][cat_iso_bij,inj_obj_def,BIJ_DEF,INJ_DEF]);
+val _ = export_rewrites["cat_iso_inj_obj"];
+
val pre_discrete_functor_def = Define`
pre_discrete_functor s c f = <|
dom := discrete_cat s;
@@ -599,7 +915,7 @@ srw_tac [][]);
val _ = export_rewrites["morf_discrete_mor"];
val is_comma_cat_obj_def = Define`
- is_comma_cat_obj (t:('a,'b,'c,'d) functor) (s:('e,'f,'c,'d) functor) x =
+ is_comma_cat_obj (t:(α,β,γ,δ) functor) (s:(ε,ζ,γ,δ) functor) x =
x.dom ∈ t.dom.obj ∧ x.cod ∈ s.dom.obj ∧
x.map :- t@@x.dom → s@@x.cod -:t.cod`;
@@ -875,10 +1191,7 @@ val is_category_cat_cat = Q.store_thm(
srw_tac [][cat_cat_def] >>
fsrw_tac [][category_axioms_def,is_functor_is_category] >>
conj_asm1_tac >- ( srw_tac [][maps_to_in_def] ) >>
-conj_tac >- srw_tac [][functor_comp_id_functor] >>
-conj_tac >- srw_tac [][functor_comp_id_functor] >>
-conj_tac >- srw_tac [][functor_comp_assoc] >>
-srw_tac [][maps_to_in_def]);
+fsrw_tac [][maps_to_in_def]);
val cat_cat_obj_mor = Q.store_thm(
"cat_cat_obj_mor",
@@ -887,4 +1200,15 @@ val cat_cat_obj_mor = Q.store_thm(
srw_tac [][cat_cat_def]);
val _ = export_rewrites["cat_cat_obj_mor"];
+(*
+val bifunctor_functors = Q.store_thm(
+"bifunctor_functors", (* Mac Lane p 37 *)
+`∀B C D M L.
+ is_category B ∧ is_category C ∧ is_category D ∧
+ (∀c. c ∈ C.obj ⇒ is_functor (L c) ∧ (L c) :- B → D) ∧
+ (∀b. b ∈ B.obj ⇒ is_functor (M b) ∧ (M b) :- C → D) ∧
+ (∀b c. b ∈ B.obj ∧ c ∈ C.obj ⇒ (M b)@@c = (L c)@@b) ⇒
+ (∃S. is_functor S ∧ S :- B × C → D ∧
+*)
+
val _ = export_theory ();
412 examples/category/hom_functorScript.sml
View
@@ -0,0 +1,412 @@
+open HolKernel Parse boolLib boolSimps bossLib pred_setTheory categoryTheory functorTheory ens_catTheory lcsymtacs;
+
+val _ = new_theory "hom_functor";
+
+val dom_homs_def = Define`
+ dom_homs c x = IMAGE (λy. c|x→y|) c.obj`;
+
+val cod_homs_def = Define`
+ cod_homs c x = IMAGE (λy. c|y→x|) c.obj`;
+
+val homs_def = Define`
+ homs c = let ob = c.obj in {(c|x→y|)| x ∈ ob ∧ y ∈ ob}`;
+
+val dom_homs_subset_homs = Q.store_thm(
+"dom_homs_subset_homs",
+`∀c x. x ∈ c.obj ⇒ dom_homs c x ⊆ homs c`,
+srw_tac [][dom_homs_def,homs_def,SUBSET_DEF] >>
+srw_tac [][] >> metis_tac []);
+val _ = export_rewrites["dom_homs_subset_homs"];
+
+val hom_in_dom_homs = Q.store_thm(
+"hom_in_dom_homs",
+`∀c x y. y ∈ c.obj ⇒ (c|x→y|) ∈ dom_homs c x`,
+srw_tac [][dom_homs_def] >> metis_tac []);
+val _ = export_rewrites["hom_in_dom_homs"];
+
+val hom_in_homs = Q.store_thm(
+"hom_in_homs",
+`∀c x y. x ∈ c.obj ∧ y ∈ c.obj ⇒ (c|x→y|) ∈ homs c`,
+srw_tac [][homs_def] >>
+srw_tac [][] >> metis_tac []);
+val _ = export_rewrites["hom_in_homs"];
+
+val pre_hom_functor_def = Define`
+ (pre_hom_functor c x : (α,β,(α,β) mor set, (α,β) mor -> (α,β) mor) functor) = <|
+ dom := c ; cod := ens_cat (dom_homs c x) ;
+ map := λf. TypedGraphFun ((c|x→f.dom|),(c|x→f.cod|)) (λg. f o g -:c)
+ |>`;
+
+val pre_hom_functor_dom = Q.store_thm(
+"pre_hom_functor_dom",
+`∀c x. (pre_hom_functor c x).dom = c`,
+srw_tac [][pre_hom_functor_def]);
+
+val pre_hom_functor_cod = Q.store_thm(
+"pre_hom_functor_cod",
+`∀c x. (pre_hom_functor c x).cod = ens_cat (dom_homs c x)`,
+srw_tac [][pre_hom_functor_def]);
+
+val _ = export_rewrites["pre_hom_functor_cod","pre_hom_functor_dom"];
+
+val pre_hom_functor_morf_dom_cod = Q.store_thm(
+"pre_hom_functor_morf_dom_cod",
+`∀c x f. (((pre_hom_functor c x)##f).dom = c|x→f.dom|) ∧
+ (((pre_hom_functor c x)##f).cod = c|x→f.cod|)`,
+srw_tac [][pre_hom_functor_def,morf_def,TypedGraphFun_def]);
+val _ = export_rewrites ["pre_hom_functor_morf_dom_cod"];
+
+val pre_hom_functor_morf = Q.store_thm(
+"pre_hom_functor_morf",
+`∀c x f. (pre_hom_functor c x)##f =
+ TypedGraphFun ((c|x→f.dom|), c|x→f.cod|) (λg. f o g -:c)`,
+srw_tac [][pre_hom_functor_def,morf_def]);
+val _ = export_rewrites["pre_hom_functor_morf"];
+
+val pre_hom_functor_objf = Q.store_thm(
+"pre_hom_functor_objf",
+`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj
+ ⇒ ((pre_hom_functor c x)@@y = c|x→y|)`,
+srw_tac [][objf_def,pre_hom_functor_def] >>
+imp_res_tac id_dom_cod >>
+SELECT_ELIM_TAC >>
+srw_tac [][] >- (
+ qexists_tac `c|x→y|` >>
+ fsrw_tac [][morphism_component_equality,TypedGraphFun_def] >>
+ srw_tac [][restrict_def,FUN_EQ_THM] >> srw_tac [][] >>
+ fsrw_tac [][hom_def,maps_to_in_def] ) >>
+pop_assum mp_tac >>
+fsrw_tac [][TypedGraphFun_def]);
+val _ = export_rewrites ["pre_hom_functor_objf"];
+
+val _ = add_rule{
+ term_name = "hom_functor",
+ fixity=Suffix 620,
+ pp_elements=[TOK"|",TM,TOK"\226\134\146_|"],
+ paren_style=OnlyIfNecessary,
+ block_style=(AroundEachPhrase,(PP.INCONSISTENT,0))};
+
+val hom_functor_def = Define`
+ c|x→_| = inclusion_functor (dom_homs c x) (homs c) ◎
+ mk_functor (pre_hom_functor c x)`;
+
+val functor_axioms_pre_hom_functor = Q.store_thm(
+"functor_axioms_pre_hom_functor",
+`∀c x. is_category c ∧ x ∈ c.obj ⇒ functor_axioms (pre_hom_functor c x)`,
+srw_tac [][functor_axioms_def]
+>- (
+ match_mp_tac hom_in_dom_homs >>
+ fsrw_tac [][maps_to_in_def] )
+>- (
+ match_mp_tac hom_in_dom_homs >>
+ fsrw_tac [][maps_to_in_def] )
+>- (
+ srw_tac [][hom_def] >>
+ match_mp_tac maps_to_comp >>
+ qexists_tac `f.dom` >>
+ fsrw_tac [][hom_def,maps_to_in_def] )
+>- (
+ imp_res_tac maps_to_obj >>
+ fsrw_tac [][maps_to_in_def] )
+>- (
+ imp_res_tac maps_to_obj >>
+ fsrw_tac [][maps_to_in_def] )
+>- (
+ qmatch_assum_rename_tac `y ∈ c.obj` [] >>
+ qexists_tac `c|x→y|` >>
+ srw_tac [][TypedGraphFun_def] >>
+ srw_tac [][FUN_EQ_THM,restrict_def] >>
+ srw_tac [][] >>
+ fsrw_tac [][hom_def,maps_to_in_def] ) >>
+qmatch_abbrev_tac `hh = gg o ff -:(ens_cat U)` >>
+`ff ≈> gg -:(ens_cat U)` by (
+ fsrw_tac [][Abbr`ff`,Abbr`gg`,Abbr`U`,TypedGraphFun_def] >>
+ imp_res_tac composable_in_def >> fsrw_tac [][] >>
+ fsrw_tac [][hom_def] >>
+ metis_tac [maps_to_comp,maps_to_in_dom_cod] ) >>
+srw_tac [][] >>
+`(ff ≈> gg) ∧ f ≈> g` by (
+ imp_res_tac composable_in_def >>
+ srw_tac [][] ) >>
+srw_tac [][Abbr`ff`,Abbr`gg`,Abbr`hh`] >>
+srw_tac [][morphism_component_equality] >>
+TRY ( srw_tac [][hom_def,compose_in_def,restrict_def] >> NO_TAC) >>
+srw_tac [][ComposeFun_def] >>
+srw_tac [][restrict_def,FUN_EQ_THM] >>
+srw_tac [][] >- (
+ match_mp_tac comp_assoc >>
+ fsrw_tac [][hom_def,composable_in_def,maps_to_in_def] ) >>
+qsuff_tac `F` >- srw_tac [][] >>
+qpat_assum `X ∉ Y` mp_tac >> srw_tac [][] >>
+fsrw_tac [][hom_def,comp_mor_dom_cod] >>
+pop_assum mp_tac >> srw_tac [][comp_mor_dom_cod]);
+val _ = export_rewrites["functor_axioms_pre_hom_functor"];
+
+val is_functor_hom_functor = Q.store_thm(
+"is_functor_hom_functor",
+`∀c x. is_category c ∧ x ∈ c.obj ⇒ is_functor (c|x→_|)`,
+srw_tac [][hom_functor_def]);
+val _ = export_rewrites["is_functor_hom_functor"];
+
+val hom_functor_objf = Q.store_thm(
+"hom_functor_objf",
+`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj
+ ⇒ (objf (hom_functor c x) y = c|x→y|)`,
+srw_tac [][hom_functor_def] >>
+`(c|x→y|) ∈ dom_homs c x` by (
+ srw_tac [][dom_homs_def] ) >>
+imp_res_tac dom_homs_subset_homs >>
+fsrw_tac [][SUBSET_DEF]);
+
+val hom_functor_morf = Q.store_thm(
+"hom_functor_morf",
+`∀c x f. is_category c ∧ f ∈ c.mor ⇒
+((c|x→_|)##f =
+ TypedGraphFun ((c|x→f.dom|), c|x→f.cod|) (λg. f o g -:c))`,
+srw_tac [][hom_functor_def] >>
+qmatch_abbrev_tac `inclusion_functor u1 u2##z = X` >>
+`z ∈ (ens_cat u1).mor` by (
+ unabbrev_all_tac >>
+ srw_tac [][hom_in_dom_homs,mor_obj] >>
+ fsrw_tac [][hom_def] >>
+ match_mp_tac maps_to_comp >>
+ metis_tac [maps_to_in_def,maps_to_def] ) >>
+srw_tac [][]);
+
+val _ = export_rewrites["hom_functor_objf","hom_functor_morf"];
+
+val hom_functor_dom = Q.store_thm(
+"hom_functor_dom",
+`∀c x. (hom_functor c x).dom = c`,
+srw_tac [][hom_functor_def]);
+
+val hom_functor_cod = Q.store_thm(
+"hom_functor_cod",
+`∀c x. (hom_functor c x).cod = (ens_cat (homs c))`,
+srw_tac [][hom_functor_def]);
+
+val _ = export_rewrites["hom_functor_cod","hom_functor_dom"];
+
+val hom_op_cat = Q.store_thm(
+"hom_op_cat",
+`∀c x y. (c° |x→y|) = IMAGE op_mor (c|y→x|)`,
+srw_tac [][hom_def,EXTENSION] >>
+metis_tac [op_cat_maps_to_in,op_mor_map,op_mor_idem]);
+val _ = export_rewrites["hom_op_cat"];
+
+(*
+val contra_functor_def = Define`
+ contra_functor G = <| dom := G.dom°; cod := G.cod; map := G.map o op_mor |>`;
+
+val contra_functor_components = Q.store_thm(
+"contra_functor_components",
+`∀G. ((contra_functor G).dom = G.dom°) ∧
+ ((contra_functor G).cod = G.cod) ∧
+ ((contra_functor G).map = G.map o op_mor)`,
+srw_tac [][contra_functor_def]);
+val _ = export_rewrites["contra_functor_components"];
+
+val contra_functor_morf = Q.store_thm(
+"contra_functor_morf",
+`∀G f. (contra_functor G)##f = G##(f°)`,
+srw_tac [][contra_functor_def,morf_def]);
+
+val contra_functor_objf = Q.store_thm(
+"contra_functor_objf",
+`∀G x. is_category G.dom ∧ x ∈ G.dom.obj ⇒ ((contra_functor G)@@x = G@@x)`,
+srw_tac [][objf_def,contra_functor_def]);
+
+val _ = export_rewrites["contra_functor_morf","contra_functor_objf"];
+
+val extensional_functor_contra_functor = Q.store_thm(
+"extensional_functor_contra_functor",
+`∀G. extensional_functor (contra_functor G) ⇔ extensional_functor G`,
+srw_tac [DNF_ss][extensional_functor_def,extensional_def,EQ_IMP_THM] >- (
+ first_x_assum (qspec_then `e°` mp_tac) >>
+ srw_tac [][] ) >>
+first_x_assum match_mp_tac >>
+first_x_assum (qspec_then `e°` mp_tac) >>
+srw_tac [][] );
+
+val functor_axioms_contra_functor = Q.store_thm(
+"functor_axioms_contra_functor",
+`∀G. functor_axioms (contra_functor G) ⇔ functor_axioms G`,
+srw_tac [][functor_axioms_def] >> EQ_TAC >> strip_tac >> fsrw_tac [][] >- (
+ conj_tac >- (
+ srw_tac [][] >>
+ first_x_assum (qspecl_then [`f°`,`x`,`y`] mp_tac) >>
+ imp_res_tac maps_to_obj >>
+ srw_tac [][]
+
+val is_functor_contra_functor = Q.store_thm(
+"is_functor_contra_functor",
+`∀G. is_functor (contra_functor G) ⇔ is_functor G`,
+srw_tac [][is_functor_def,extensional_functor_contra_functor,functor_axioms_contra_functor]);
+val _ = export_rewrites["is_functor_contra_functor"];
+*)
+
+val pre_op_mor_functor_def = Define`
+ pre_op_mor_functor u1 u2 = <| dom := ens_cat u1; cod := ens_cat u2;
+ map := λf. TypedGraphFun
+ (IMAGE op_mor f.dom, IMAGE op_mor f.cod)
+ (op_mor o f.map o op_mor) |>`;
+
+val pre_op_mor_functor_components = Q.store_thm(
+"pre_op_mor_functor_components",
+`∀u1 u2.
+ ((pre_op_mor_functor u1 u2).dom = ens_cat u1) ∧
+ ((pre_op_mor_functor u1 u2).cod = ens_cat u2) ∧
+ ((pre_op_mor_functor u1 u2).map = λf. TypedGraphFun
+ (IMAGE op_mor f.dom, IMAGE op_mor f.cod)
+ (op_mor o f.map o op_mor))`,
+srw_tac [][pre_op_mor_functor_def]);
+val _ = export_rewrites["pre_op_mor_functor_components"];
+
+val pre_op_mor_functor_morf = Q.store_thm(
+"pre_op_mor_functor_morf",
+`∀u1 u2 f. (pre_op_mor_functor u1 u2)##f =
+ TypedGraphFun (IMAGE op_mor f.dom, IMAGE op_mor f.cod) (op_mor o f.map o op_mor)`,
+srw_tac [][morf_def]);
+val _ = export_rewrites["pre_op_mor_functor_morf"];
+
+val pre_op_mor_functor_objf = Q.store_thm(
+"pre_op_mor_functor_objf",
+`∀u1 u2 x. x ∈ u1 ∧ IMAGE op_mor x ∈ u2 ⇒ ((pre_op_mor_functor u1 u2)@@x = IMAGE op_mor x)`,
+srw_tac [][objf_def] >>
+SELECT_ELIM_TAC >>
+conj_tac >- (
+ qexists_tac `IMAGE op_mor x` >>
+ srw_tac [][] >>
+ srw_tac [][morphism_component_equality] >>
+ srw_tac [][restrict_def,FUN_EQ_THM] >>
+ srw_tac [][] >> fsrw_tac [][] ) >>
+srw_tac [][] >>
+fsrw_tac [][morphism_component_equality]);
+val _ = export_rewrites["pre_op_mor_functor_objf"];
+
+val op_mor_functor_def = Define`
+ op_mor_functor u1 u2 = mk_functor (pre_op_mor_functor u1 u2)`;
+
+val is_functor_op_mor_functor = Q.store_thm(
+"is_functor_op_mor_functor",
+`∀u1 u2. (∀x. x ∈ u1 ⇒ IMAGE op_mor x ∈ u2) ⇒ is_functor (op_mor_functor u1 u2)`,
+srw_tac [][op_mor_functor_def] >>
+srw_tac [][functor_axioms_def] >>
+srw_tac [][] >- fsrw_tac [][IsTypedFun_def,HasFunType_def]
+>- (
+ qexists_tac `IMAGE op_mor x` >>
+ srw_tac [][morphism_component_equality] >>
+ srw_tac [][restrict_def,FUN_EQ_THM] >>
+ srw_tac [][] >> fsrw_tac [][] ) >>
+qmatch_abbrev_tac `hh = gg o ff -: ens_cat u2` >>
+`ff ≈> gg -:ens_cat u2` by (
+ srw_tac [][Abbr`ff`,Abbr`gg`] >>
+ fsrw_tac [][IsTypedFun_def,HasFunType_def] ) >>
+srw_tac [][] >>
+srw_tac [][Abbr`gg`,Abbr`ff`,Abbr`hh`,morphism_component_equality] >>
+srw_tac [][ComposeFun_def] >>
+srw_tac [][restrict_def,FUN_EQ_THM] >>
+srw_tac [][] >>
+fsrw_tac [][IsTypedFun_def,HasFunType_def] >>
+metis_tac []);
+val _ = export_rewrites["is_functor_op_mor_functor"];
+
+val op_mor_functor_dom_cod = Q.store_thm(
+"op_mor_functor_dom_cod",
+`∀u1 u2. ((op_mor_functor u1 u2).dom = ens_cat u1) ∧
+ ((op_mor_functor u1 u2).cod = ens_cat u2)`,
+srw_tac [][op_mor_functor_def]);
+val _ = export_rewrites["op_mor_functor_dom_cod"];
+
+val op_mor_functor_morf = Q.store_thm(
+"op_mor_functor_morf",
+`∀u1 u2 f. IsTypedFunIn u1 f ⇒ ((op_mor_functor u1 u2)##f =
+ TypedGraphFun (IMAGE op_mor f.dom, IMAGE op_mor f.cod) (op_mor o f.map o op_mor))`,
+srw_tac [][op_mor_functor_def,mk_functor_def,morphism_component_equality,morf_def,
+ restrict_def]);
+val _ = export_rewrites["op_mor_functor_morf"];
+
+val op_mor_functor_objf = Q.store_thm(
+"op_mor_functor_objf",
+`∀u1 u2 x. x ∈ u1 ∧ IMAGE op_mor x ∈ u2 ⇒ ((op_mor_functor u1 u2)@@x = IMAGE op_mor x)`,
+srw_tac [][op_mor_functor_def]);
+val _ = export_rewrites["op_mor_functor_objf"];
+
+val _ = add_rule{
+ term_name = "contra_hom_functor",
+ fixity=Suffix 620,
+ pp_elements=[TOK"|_\226\134\146",TM,TOK"|"],
+ paren_style=OnlyIfNecessary,
+ block_style=(AroundEachPhrase,(PP.INCONSISTENT,0))};
+
+val _ = overload_on("contra_hom_functor",``λc x. (op_mor_functor (homs c°) (homs c)) ◎ (hom_functor c° x)``);
+
+val IMAGE_op_mor_idem = Q.store_thm(
+"IMAGE_op_mor_idem",
+`∀s. IMAGE op_mor (IMAGE op_mor s) = s`,
+srw_tac [DNF_ss][EXTENSION]);
+val _ = export_rewrites["IMAGE_op_mor_idem"];
+
+val is_functor_contra_hom_functor_lemma = Q.store_thm(
+"is_functor_contra_hom_functor_lemma",
+`∀c. is_functor (op_mor_functor (homs c°) (homs c))`,
+srw_tac [][] >>
+match_mp_tac is_functor_op_mor_functor >>
+srw_tac [DNF_ss][homs_def,LET_THM] >>
+metis_tac []);
+val _ = export_rewrites["is_functor_contra_hom_functor_lemma"];
+
+val contra_hom_functor_objf = Q.store_thm(
+"contra_hom_functor_objf",
+`∀c x y. is_category c ∧ x ∈ c.obj ∧ y ∈ c.obj ⇒ ((c|_→y|)@@x = (c|x→y|))`,
+srw_tac [][] >>
+`IMAGE op_mor (c|x→y|) ∈ homs c°` by (
+ srw_tac [][homs_def] >>
+ srw_tac [][] >> metis_tac [] ) >>
+`IMAGE op_mor (IMAGE op_mor (c|x→y|)) ∈ (homs c)` by (
+ srw_tac [DNF_ss][homs_def,EXTENSION] >>
+ srw_tac [][] >> metis_tac [] ) >>
+srw_tac [][] >> srw_tac [DNF_ss][EXTENSION]);
+
+val contra_hom_functor_morf = Q.store_thm(
+"contra_hom_functor_morf",
+`∀c x f. is_category c ∧ f° ∈ c.mor ∧ x ∈ c.obj ⇒
+ ((c|_→x|)##f = TypedGraphFun ((c|f.dom→x|), (c|f.cod→x|)) (λg. g o f° -:c))`,
+srw_tac [][] >>
+qabbrev_tac `ff = f° °` >>
+`f = ff` by srw_tac [][Abbr`ff`] >>
+`ff ∈ c°.mor` by (
+ srw_tac [][Abbr`ff`] >>
+ qexists_tac `f°` >> srw_tac [][] ) >>
+fsrw_tac [][] >> srw_tac [][] >>
+qmatch_abbrev_tac `(op_mor_functor u1 u2)##f = g` >>
+`IsTypedFun f` by (
+ srw_tac [][Abbr`f`,Abbr`g`] >>
+ qmatch_assum_rename_tac `f ∈ (c|g.cod→x|)` [] >>
+ qexists_tac `f° ° o g° ° -:c` >>
+ `g° ° ≈> f° ° -:c` by (
+ match_mp_tac maps_to_composable >>
+ srw_tac [][] >> fsrw_tac [][hom_def,maps_to_in_def] ) >>
+ conj_tac >- (
+ match_mp_tac op_cat_compose_in >>
+ srw_tac [][] ) >>
+ imp_res_tac composable_maps_to >>
+ fsrw_tac [][hom_def] >>
+ fsrw_tac [][maps_to_in_def] ) >>
+`IsTypedFunIn u1 f` by (
+ fsrw_tac [][Abbr`f`,Abbr`u1`,Abbr`u2`,homs_def] >>
+ fsrw_tac [][LET_THM] >>
+ metis_tac [mor_obj] ) >>
+srw_tac [][Abbr`g`,Abbr`f`,morphism_component_equality] >>
+TRY (srw_tac [DNF_ss][EXTENSION] >> NO_TAC) >>
+srw_tac [][restrict_def,FUN_EQ_THM] >>
+srw_tac [][] >> fsrw_tac [DNF_ss][] >- (
+ qmatch_rename_tac `(g° o f° -:c°)° = f o g -:c` [] >>
+ qspecl_then [`f`,`g`,`c°`] mp_tac op_cat_compose_in >>
+ srw_tac [][] >> pop_assum (match_mp_tac o GSYM) >>
+ match_mp_tac maps_to_composable >>
+ fsrw_tac [][hom_def,maps_to_in_def] ) >>
+metis_tac [op_mor_idem]);
+val _ = export_rewrites["contra_hom_functor_objf","contra_hom_functor_morf"];
+
+val _ = export_theory();
70 examples/category/limitScript.sml
View
@@ -31,6 +31,28 @@ val initial_unique = Q.store_thm(
`∀c x y. is_category c ∧ is_initial c x ∧ is_initial c y ⇒ uiso_objs c x y`,
metis_tac [terminal_unique,is_initial_def,is_category_op_cat,op_cat_uiso_objs]);
+val is_terminal_cat_iso = Q.store_thm(
+"is_terminal_cat_iso", (* actually should work for just an equivalence *)
+`∀f c d x. cat_iso f ∧ (f :- c → d) ∧ is_terminal c x ⇒ is_terminal d (f@@x)`,
+srw_tac [][cat_iso_def] >>
+imp_res_tac cat_iso_pair_sym >>
+`is_functor f ∧ is_functor g` by fsrw_tac [][cat_iso_pair_def] >>
+`(f ≈> g) ∧ (g ≈> f)` by fsrw_tac [][cat_iso_pair_def] >>
+`faithful g` by metis_tac [cat_iso_embedding,embedding_def,cat_iso_def] >>
+fsrw_tac [][is_terminal_def,objf_in_obj] >>
+qx_gen_tac `y` >> strip_tac >>
+`g@@y ∈ f.dom.obj` by metis_tac [objf_in_obj,composable_def] >>
+first_x_assum (qspec_then `g@@y` mp_tac) >>
+srw_tac [][] >>
+imp_res_tac is_functor_is_category >>
+fsrw_tac [][EXISTS_UNIQUE_THM] >>
+qmatch_assum_rename_tac `h :- g@@y → x -:f.dom` [] >>
+`f##h :- f@@(g@@y) → f@@x -:f.cod` by metis_tac [morf_maps_to,maps_to_def] >>
+conj_tac >- metis_tac [functor_comp_objf,cat_iso_pair_def,id_functor_objf,composable_def] >>
+qx_gen_tac `h1` >> qx_gen_tac `h2` >> strip_tac >>
+fsrw_tac [][faithful_def,cat_iso_pair_def] >>
+metis_tac [morf_maps_to,functor_comp_objf,id_functor_objf,composable_def,maps_to_def]);
+
val cone_cat_def = Define`
cone_cat f = comma_cat (diagonal_functor f.dom f.cod) (itself_functor f)`;
@@ -47,10 +69,10 @@ match_mp_tac is_functor_itself_functor >>
srw_tac [][]);
val _ = export_rewrites["is_category_cone_cat"];
-val _ = type_abbrev("cone",``:('a,unit,('b,'a,'c,'d) nat_trans) morphism``);
-val _ = type_abbrev("cone_mor",``:(('a,'b,'c,'d) cone, ('a,'d) mor # (unit, unit) mor) mor``);
-val _ = overload_on("vertex",``λ(c:('a,'b,'c,'d)cone). c.dom``);
-val _ = overload_on("proj",``λ(c:('a,'b,'c,'d)cone) x. c.map@+x``);
+val _ = type_abbrev("cone",``:(γ,unit,(α,β,γ,δ) nat_trans) morphism``);
+val _ = type_abbrev("cone_mor",``:((α,β,γ,δ) cone, (γ,δ) mor # (unit, unit) mor) mor``);
+val _ = overload_on("vertex",``λ(c:(α,β,γ,δ)cone). c.dom``);
+val _ = overload_on("proj",``λ(c:(α,β,γ,δ)cone) x. c.map@+x``);
val _ = overload_on("is_cone",``λd c. c ∈ (cone_cat d).obj``);
val _ = overload_on("is_cone_mor",``λd f. f ∈ (cone_cat d).mor``);
@@ -110,7 +132,7 @@ fsrw_tac [][] >>
metis_tac []);
val mk_cone_def = Define`
- (mk_cone d v ps : ('a,'b,'c,'d) cone) =
+ (mk_cone d v ps : (α,β,γ,δ) cone) =
<| dom := v; cod := ();
map := mk_nt <| dom := K_functor d.dom d.cod v;
cod := d;
@@ -189,7 +211,7 @@ match_mp_tac nt_eq_thm >>
fsrw_tac [][]);
val mk_cone_mor_def = Define`
- (mk_cone_mor c1 c2 m : ('a,'b,'c,'d) cone_mor) =
+ (mk_cone_mor c1 c2 m : (α,β,γ,δ) cone_mor) =
<| dom := c1; cod := c2; map := (m,ARB) |>`;
val mk_cone_mor_dom_cod = Q.store_thm(
@@ -283,15 +305,15 @@ val has_limits_def = Define`
(*
val functor_cat_pointwise_limits = Q.store_thm(
"functor_cat_pointwise_limits", (* Mac Lane p 111*)
-`∀D J P X tau. is_functor D ∧ (D :- J → [P→X]) ∧
- (∀p. p ∈ P.obj ⇒ is_limit ((eval_functor P X p) ◎ D) (tau p)) ⇒
+`∀D J P X τ. is_functor D ∧ (D :- J → [P→X]) ∧
+ (∀p. p ∈ P.obj ⇒ is_limit ((eval_functor P X p) ◎ D) (τ p)) ⇒
(∃L. is_functor L ∧ (L :- P → X) ∧
- (∀p. p ∈ P.obj ⇒ (L@@p = vertex (tau p))) ∧
+ (∀p. p ∈ P.obj ⇒ (L@@p = vertex (τ p))) ∧
let t = λL. (mk_nt <|dom := (diagonal_functor J [P→X])@@L; cod := D;
map := λj. mk_nt <|dom := ((diagonal_functor J [P→X])@@L)@@j; cod := D@@j;
- map := λp. proj (tau p) j|> |>) in
+ map := λp. proj (τ p) j|> |>) in
(is_nat_trans (t L)) ∧
- (∀L'. is_functor L' ∧ (L' :- P → X) ∧ (∀p. p ∈ P.obj ⇒ (L'@@p = vertex (tau p))) ∧ is_nat_trans (t L') ⇒ (L' = L)) ∧
+ (∀L'. is_functor L' ∧ (L' :- P → X) ∧ (∀p. p ∈ P.obj ⇒ (L'@@p = vertex (τ p))) ∧ is_nat_trans (t L') ⇒ (L' = L)) ∧
(is_limit D (mk_cone D L ((t L).map))))`,
srw_tac [][] >>
limit_universal
@@ -305,14 +327,32 @@ val functor_cat_has_limits = Q.store_thm(
srw_tac [][has_limits_def] >>
fsrw_tac [][GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM] >>
qabbrev_tac `j = d.dom` >>
-qabbrev_tac `tau = λp. f (eval_functor c v p ◎ d)` >>
-`∀p. p ∈ c.obj ⇒ is_limit (eval_functor c v p ◎ d) (tau p)` by
- srw_tac [][Abbr`tau`] >>
-Q.ISPECL_THEN [`d`,`j`,`c`,`v`,`tau`] mp_tac functor_cat_pointwise_limits >>
+qabbrev_tac `τ = λp. f (eval_functor c v p ◎ d)` >>
+`∀p. p ∈ c.obj ⇒ is_limit (eval_functor c v p ◎ d) (τ p)` by
+ srw_tac [][Abbr`τ`] >>
+Q.ISPECL_THEN [`d`,`j`,`c`,`v`,`τ`] mp_tac functor_cat_pointwise_limits >>
srw_tac [][LET_THM] >>
metis_tac []);
*)
+(*
+val _ = overload_on("empty_diagram",``λc. discrete_functor {} c ARB``);
+
+val is_functor_empty_diagram = Q.store_thm(
+"is_functor_empty_diagram",
+`∀c. is_category c ⇒ is_functor (empty_diagram c)`,
+srw_tac [][is_functor_discrete_functor]);
+val _ = export_rewrites["is_functor_empty_diagram"];
+
+val limit_empty_diagram_terminal = Q.store_thm(
+"limit_empty_diagram_terminal",
+`∀c. is_category c ⇒ (is_limit (empty_diagram c) = is_terminal c o vertex)`,
+srw_tac [][FUN_EQ_THM,is_limit_def] >>
+srw_tac [][is_terminal_def,is_cone_thm,EQ_IMP_THM] >- (
+ fsrw_tac [][is_cone_thm]
+why bother proving this?
+*)
+
val _ = overload_on("product_diagram",``λc a b. discrete_functor {1;2} c (λn. if n = 1 then a else b)``);
val is_functor_product_diagram = Q.store_thm(
357 examples/category/nat_transScript.sml
View
@@ -3,13 +3,13 @@ open HolKernel Parse boolLib bossLib lcsymtacs categoryTheory functorTheory;
val _ = new_theory "nat_trans";
val _ = type_abbrev("nat_trans",
-``:(('a1,'b1,'a2,'b2) functor,('a1,'b1,'a2,'b2) functor,
- 'a1 -> ('a2,'b2) mor) morphism``);
+``:((α,β,γ,δ) functor,(α,β,γ,δ) functor,
+ α -> (γ,δ) mor) morphism``);
val _ = overload_on("ntdom", ``λn. n.dom.dom``);
val _ = overload_on("ntcod", ``λn. n.cod.cod``);
val _ = set_fixity "@+" (Infixl 2000);
-val _ = overload_on("@+", ``λ(n:('a,'b,'c,'d) nat_trans) x. n.map x``);
+val _ = overload_on("@+", ``λ(n:(α,β,γ,δ) nat_trans) x. n.map x``);
val extensional_nat_trans_def = Define`
extensional_nat_trans n = extensional n.map (ntdom n).obj`;
@@ -495,6 +495,357 @@ EQ_TAC >> strip_tac >- (
metis_tac []
*)
+val pre_functor_nt_def = Define`
+ pre_functor_nt f n = <|
+ dom := f ◎ n.dom;
+ cod := f ◎ n.cod;
+ map := λx. f##(n@+x) |>`;
+
+val pre_functor_nt_components = Q.store_thm(
+"pre_functor_nt_components",
+`∀f n. ((pre_functor_nt f n).dom = f ◎ n.dom) ∧
+ ((pre_functor_nt f n).cod = f ◎ n.cod) ∧
+ (∀x. (pre_functor_nt f n)@+x = f##(n@+x))`,
+srw_tac [][pre_functor_nt_def]);
+val _ = export_rewrites["pre_functor_nt_components"];
+