(* Title: SetCat Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter SetCat theory SetCat imports SetCategory ConcreteCategory begin text‹ This theory proves the consistency of the ‹set_category› locale by giving a particular concrete construction of an interpretation for it. Applying the general construction given by @{locale concrete_category}, we define arrows to be terms ‹MkArr A B F›, where ‹A› and ‹B› are sets and ‹F› is an extensional function that maps ‹A› to ‹B›. › text‹ This locale uses an extra dummy parameter just to fix the element type for sets. Without this, a type is used for each interpretation, which makes it impossible to construct set categories whose element types are related to the context. An additional parameter, @{term Setp}, allows some control over which subsets of the element type are assumed to correspond to objects of the category. › locale setcat = fixes elem_type :: "'e itself" and Setp :: "'e set ⇒ bool" assumes Setp_singleton: "Setp {x}" and Setp_respects_subset: "A' ⊆ A ⟹ Setp A ⟹ Setp A'" and union_preserves_Setp: "⟦ Setp A; Setp B ⟧ ⟹ Setp (A ∪ B)" begin lemma finite_imp_Setp: "finite A ⟹ Setp A" using Setp_singleton by (metis finite_induct insert_is_Un Setp_respects_subset singleton_insert_inj_eq union_preserves_Setp) type_synonym 'b arr = "('b set, 'b ⇒ 'b) concrete_category.arr" interpretation S: concrete_category ‹Collect Setp› ‹λA B. extensional A ∩ (A → B)› ‹λA. λx ∈ A. x› ‹λC B A g f. compose A g f› using compose_Id Id_compose apply unfold_locales apply auto[3] apply blast by (metis IntD2 compose_assoc) abbreviation comp :: "'e setcat.arr comp" (infixr "⋅" 55) where "comp ≡ S.COMP" notation S.in_hom ("«_ : _ → _»") lemma is_category: shows "category comp" using S.category_axioms by simp lemma MkArr_expansion: assumes "S.arr f" shows "f = S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x)" proof (intro S.arr_eqI) show "S.arr f" by fact show "S.arr (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))" using assms S.arr_char by (metis (mono_tags, lifting) Int_iff S.MkArr_Map extensional_restrict) show "S.Dom f = S.Dom (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))" by simp show "S.Cod f = S.Cod (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))" by simp show "S.Map f = S.Map (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))" using assms S.arr_char by (metis (mono_tags, lifting) Int_iff S.MkArr_Map extensional_restrict) qed lemma arr_char: shows "S.arr f ⟷ f ≠ S.Null ∧ Setp (S.Dom f) ∧ Setp (S.Cod f) ∧ S.Map f ∈ extensional (S.Dom f) ∩ (S.Dom f → S.Cod f)" using S.arr_char by auto lemma terminal_char: shows "S.terminal a ⟷ (∃x. a = S.MkIde {x})" proof show "∃x. a = S.MkIde {x} ⟹ S.terminal a" proof - assume a: "∃x. a = S.MkIde {x}" from this obtain x where x: "a = S.MkIde {x}" by blast have "S.terminal (S.MkIde {x})" proof show 1: "S.ide (S.MkIde {x})" using finite_imp_Setp S.ide_MkIde by auto show "⋀a. S.ide a ⟹ ∃!f. «f : a → S.MkIde {x}»" proof fix a :: "'e setcat.arr" assume a: "S.ide a" show "«S.MkArr (S.Dom a) {x} (λ_∈S.Dom a. x) : a → S.MkIde {x}»" proof show 2: "S.arr (S.MkArr (S.Dom a) {x} (λ_ ∈ S.Dom a. x))" using a 1 S.arr_MkArr [of "S.Dom a" "{x}"] S.ide_char⇩_{C}⇩_{C}by force show "S.dom (S.MkArr (S.Dom a) {x} (λ_ ∈ S.Dom a. x)) = a" using a 2 S.dom_MkArr by force show "S.cod (S.MkArr (S.Dom a) {x} (λ_∈S.Dom a. x)) = S.MkIde {x}" using 2 S.cod_MkArr by blast qed fix f :: "'e setcat.arr" assume f: "«f : a → S.MkIde {x}»" show "f = S.MkArr (S.Dom a) {x} (λ_ ∈ S.Dom a. x)" proof - have 1: "S.Dom f = S.Dom a ∧ S.Cod f = {x}" using a f by (metis (mono_tags, lifting) S.Dom.simps(1) S.in_hom_char) moreover have "S.Map f = (λ_ ∈ S.Dom a. x)" proof fix z have "z ∉ S.Dom a ⟹ S.Map f z = (λ_ ∈ S.Dom a. x) z" using f 1 MkArr_expansion by (metis (mono_tags, lifting) S.Map.simps(1) S.in_homE restrict_apply) moreover have "z ∈ S.Dom a ⟹ S.Map f z = (λ_ ∈ S.Dom a. x) z" using f 1 arr_char [of f] by fastforce ultimately show "S.Map f z = (λ_ ∈ S.Dom a. x) z" by auto qed ultimately show ?thesis using f MkArr_expansion [of f] by fastforce qed qed qed thus "S.terminal a" using x by simp qed show "S.terminal a ⟹ ∃x. a = S.MkIde {x}" proof - assume a: "S.terminal a" hence ide_a: "S.ide a" using S.terminal_def by auto have 1: "∃!x. x ∈ S.Dom a" proof - have "S.Dom a = {} ⟹ ¬S.terminal a" proof - assume "S.Dom a = {}" hence 1: "a = S.MkIde {}" using S.MkIde_Dom' ‹S.ide a› by fastforce have "⋀f. f ∈ S.hom (S.MkIde {undefined}) (S.MkIde ({} :: 'e set)) ⟹ S.Map f ∈ {undefined} → {}" proof - fix f assume f: "f ∈ S.hom (S.MkIde {undefined}) (S.MkIde ({} :: 'e set))" show "S.Map f ∈ {undefined} → {}" using f MkArr_expansion arr_char [of f] S.in_hom_char by auto qed hence "S.hom (S.MkIde {undefined}) a = {}" using 1 by auto moreover have "S.ide (S.MkIde {undefined})" using finite_imp_Setp by (metis (mono_tags, lifting) finite.intros(1-2) S.ide_MkIde mem_Collect_eq) ultimately show "¬S.terminal a" by blast qed moreover have "⋀x x'. x ∈ S.Dom a ∧ x' ∈ S.Dom a ∧ x ≠ x' ⟹ ¬S.terminal a" proof - fix x x' assume 1: "x ∈ S.Dom a ∧ x' ∈ S.Dom a ∧ x ≠ x'" let ?f = "S.MkArr {undefined} (S.Dom a) (λ_ ∈ {undefined}. x)" let ?f' = "S.MkArr {undefined} (S.Dom a) (λ_ ∈ {undefined}. x')" have "S.par ?f ?f'" proof - have "«?f : S.MkIde {undefined} → a»" proof show 2: "S.arr ?f" proof (intro S.arr_MkArr) show "{undefined} ∈ {A. Setp A}" by (simp add: finite_imp_Setp) show "S.Dom a ∈ {A. Setp A}" using ide_a S.ide_char⇩_{C}⇩_{C}by blast show "(λ_ ∈ {undefined}. x) ∈ extensional {undefined} ∩ ({undefined} → S.Dom a)" using 1 by blast qed show "S.dom ?f = S.MkIde {undefined}" using 2 S.dom_MkArr by auto show "S.cod ?f = a" using 2 S.cod_MkArr ide_a by force qed moreover have "«?f' : S.MkIde {undefined} → a»" proof show 2: "S.arr ?f'" proof (intro S.arr_MkArr) show "{undefined} ∈ {A. Setp A}" by (simp add: finite_imp_Setp) show "S.Dom a ∈ {A. Setp A}" using ide_a S.ide_char⇩_{C}⇩_{C}by blast show "(λ_ ∈ {undefined}. x') ∈ extensional {undefined} ∩ ({undefined} → S.Dom a)" using 1 by blast qed show "S.dom ?f' = S.MkIde {undefined}" using 2 S.dom_MkArr by auto show "S.cod ?f' = a" using 2 S.cod_MkArr ide_a by force qed ultimately show ?thesis by (metis (no_types, lifting) S.in_homE) qed moreover have "?f ≠ ?f'" using 1 by (metis S.arr.inject restrict_apply' singletonI) ultimately show "¬S.terminal a" using S.cod_MkArr ide_a S.terminal_arr_unique [of ?f ?f'] by auto qed ultimately show ?thesis using a by auto qed hence "S.Dom a = {THE x. x ∈ S.Dom a}" using theI [of "λx. x ∈ S.Dom a"] by auto hence "a = S.MkIde {THE x. x ∈ S.Dom a}" using a S.terminal_def by (metis (mono_tags, lifting) S.MkIde_Dom') thus "∃x. a = S.MkIde {x}" by auto qed qed definition IMG :: "'e setcat.arr ⇒ 'e setcat.arr" where "IMG f = S.MkIde (S.Map f ` S.Dom f)" interpretation S: set_category_data comp IMG .. lemma terminal_unity: shows "S.terminal S.unity" using terminal_char S.unity_def someI_ex [of S.terminal] by (metis (mono_tags, lifting)) text‹ The inverse maps @{term arr_of} and @{term elem_of} are used to pass back and forth between the inhabitants of type @{typ 'a} and the corresponding terminal objects. These are exported so that a client of the theory can relate the concrete element type @{typ 'a} to the otherwise abstract arrow type. › definition arr_of :: "'e ⇒ 'e setcat.arr" where "arr_of x ≡ S.MkIde {x}" definition elem_of :: "'e setcat.arr ⇒ 'e" where "elem_of t ≡ the_elem (S.Dom t)" abbreviation U where "U ≡ elem_of S.unity" lemma arr_of_mapsto: shows "arr_of ∈ UNIV → S.Univ" using terminal_char arr_of_def by fast lemma elem_of_mapsto: shows "elem_of ∈ Univ → UNIV" by auto lemma elem_of_arr_of [simp]: shows "elem_of (arr_of x) = x" by (simp add: elem_of_def arr_of_def) lemma arr_of_elem_of [simp]: assumes "t ∈ S.Univ" shows "arr_of (elem_of t) = t" using assms terminal_char arr_of_def elem_of_def by (metis (mono_tags, lifting) mem_Collect_eq elem_of_arr_of) lemma inj_arr_of: shows "inj arr_of" by (metis elem_of_arr_of injI) lemma bij_arr_of: shows "bij_betw arr_of UNIV S.Univ" proof (intro bij_betwI) show "⋀x :: 'e. elem_of (arr_of x) = x" by simp show "⋀t. t ∈ S.Univ ⟹ arr_of (elem_of t) = t" by simp show "arr_of ∈ UNIV → S.Univ" using arr_of_mapsto by auto show "elem_of ∈ Collect S.terminal → UNIV" by auto qed lemma bij_elem_of: shows "bij_betw elem_of S.Univ UNIV" proof (intro bij_betwI) show "⋀t. t ∈ S.Univ ⟹ arr_of (elem_of t) = t" by simp show "⋀x. x ∈ UNIV ⟹ elem_of (arr_of x) = x" by simp show "elem_of ∈ S.Univ → UNIV" using elem_of_mapsto by auto show "arr_of ∈ UNIV → S.Univ" using arr_of_mapsto by auto qed lemma elem_of_img_arr_of_img [simp]: shows "elem_of ` arr_of ` A = A" by force lemma arr_of_img_elem_of_img [simp]: assumes "A ⊆ S.Univ" shows "arr_of ` elem_of ` A = A" using assms by force lemma Dom_terminal: assumes "S.terminal t" shows "S.Dom t = {elem_of t}" using assms arr_of_def by (metis (mono_tags, lifting) S.Dom.simps(1) elem_of_def terminal_char the_elem_eq) text‹ The image of a point @{term "p ∈ hom unity a"} is a terminal object, which is given by the formula @{term "(arr_of o Fun p o elem_of) unity"}. › lemma IMG_point: assumes "«p : S.unity → a»" shows "IMG ∈ S.hom S.unity a → S.Univ" and "IMG p = (arr_of o S.Map p o elem_of) S.unity" proof - show "IMG ∈ S.hom S.unity a → S.Univ" proof fix f assume f: "f ∈ S.hom S.unity a" have "S.terminal (S.MkIde (S.Map f ` S.Dom S.unity))" proof - obtain u :: 'e where u: "S.unity = S.MkIde {u}" using terminal_unity terminal_char by (metis (mono_tags, lifting)) have "S.Map f ` S.Dom S.unity = {S.Map f u}" using u by simp thus ?thesis using terminal_char by auto qed hence "S.MkIde (S.Map f ` S.Dom S.unity) ∈ S.Univ" by simp moreover have "S.MkIde (S.Map f ` S.Dom S.unity) = IMG f" using f IMG_def S.in_hom_char by (metis (mono_tags, lifting) mem_Collect_eq) ultimately show "IMG f ∈ S.Univ" by auto qed have "IMG p = S.MkIde (S.Map p ` S.Dom p)" using IMG_def by blast also have "... = S.MkIde (S.Map p ` {U})" using assms S.in_hom_char terminal_unity Dom_terminal by (metis (mono_tags, lifting)) also have "... = (arr_of o S.Map p o elem_of) S.unity" by (simp add: arr_of_def) finally show "IMG p = (arr_of o S.Map p o elem_of) S.unity" using assms by auto qed text‹ The function @{term IMG} is injective on @{term "hom unity a"} and its inverse takes a terminal object @{term t} to the arrow in @{term "hom unity a"} corresponding to the constant-@{term t} function. › abbreviation MkElem :: "'e setcat.arr => 'e setcat.arr => 'e setcat.arr" where "MkElem t a ≡ S.MkArr {U} (S.Dom a) (λ_ ∈ {U}. elem_of t)" lemma MkElem_in_hom: assumes "S.arr f" and "x ∈ S.Dom f" shows "«MkElem (arr_of x) (S.dom f) : S.unity → S.dom f»" proof - have "(λ_ ∈ {U}. elem_of (arr_of x)) ∈ {U} → S.Dom (S.dom f)" using assms S.dom_char [of f] by simp moreover have "S.MkIde {U} = S.unity" using terminal_char terminal_unity by (metis (mono_tags, lifting) elem_of_arr_of arr_of_def) moreover have "S.MkIde (S.Dom (S.dom f)) = S.dom f" using assms S.dom_char S.MkIde_Dom' S.ide_dom by blast ultimately show ?thesis using assms S.MkArr_in_hom [of "{U}" "S.Dom (S.dom f)" "λ_ ∈ {U}. elem_of (arr_of x)"] by (metis (no_types, lifting) S.Dom.simps(1) S.Dom_in_Obj IntI S.arr_dom S.ideD(1) restrict_extensional S.terminal_def terminal_unity) qed lemma MkElem_IMG: assumes "p ∈ S.hom S.unity a" shows "MkElem (IMG p) a = p" proof - have 0: "IMG p = arr_of (S.Map p U)" using assms IMG_point(2) by auto have 1: "S.Dom p = {U}" using assms terminal_unity Dom_terminal by (metis (mono_tags, lifting) S.in_hom_char mem_Collect_eq) moreover have "S.Cod p = S.Dom a" using assms by (metis (mono_tags, lifting) S.in_hom_char mem_Collect_eq) moreover have "S.Map p = (λ_ ∈ {U}. elem_of (IMG p))" proof fix e show "S.Map p e = (λ_ ∈ {U}. elem_of (IMG p)) e" proof - have "S.Map p e = (λx ∈ S.Dom p. S.Map p x) e" using assms MkArr_expansion [of p] by (metis (mono_tags, lifting) CollectD S.Map.simps(1) S.in_homE) also have "... = (λ_ ∈ {U}. elem_of (IMG p)) e" using assms 0 1 by simp finally show ?thesis by blast qed qed ultimately show "MkElem (IMG p) a = p" using assms S.MkArr_Map CollectD by (metis (mono_tags, lifting) S.in_homE mem_Collect_eq) qed lemma inj_IMG: assumes "S.ide a" shows "inj_on IMG (S.hom S.unity a)" proof (intro inj_onI) fix x y assume x: "x ∈ S.hom S.unity a" assume y: "y ∈ S.hom S.unity a" assume eq: "IMG x = IMG y" show "x = y" proof (intro S.arr_eqI) show "S.arr x" using x by blast show "S.arr y" using y by blast show "S.Dom x = S.Dom y" using x y S.in_hom_char by (metis (mono_tags, lifting) CollectD) show "S.Cod x = S.Cod y" using x y S.in_hom_char by (metis (mono_tags, lifting) CollectD) show "S.Map x = S.Map y" proof - have "⋀a. y ∈ S.hom S.unity a ⟹ S.MkArr {U} (S.Dom a) (λe∈{U}. elem_of (IMG x)) = y" using MkElem_IMG eq by presburger hence "y = x" using MkElem_IMG x y by blast thus ?thesis by meson qed qed qed lemma set_char: assumes "S.ide a" shows "S.set a = arr_of ` S.Dom a" proof show "S.set a ⊆ arr_of ` S.Dom a" proof fix t assume "t ∈ S.set a" from this obtain p where p: "«p : S.unity → a» ∧ t = IMG p" using S.set_def by blast have "t = (arr_of o S.Map p o elem_of) S.unity" using p IMG_point(2) by blast moreover have "(S.Map p o elem_of) S.unity ∈ S.Dom a" using p arr_char S.in_hom_char Dom_terminal terminal_unity by (metis (mono_tags, lifting) IntD2 Pi_split_insert_domain o_apply) ultimately show "t ∈ arr_of ` S.Dom a" by simp qed show "arr_of ` S.Dom a ⊆ S.set a" proof fix t assume "t ∈ arr_of ` S.Dom a" from this obtain x where x: "x ∈ S.Dom a ∧ t = arr_of x" by blast let ?p = "MkElem (arr_of x) a" have p: "?p ∈ S.hom S.unity a" using assms x MkElem_in_hom [of "S.dom a"] S.ideD(1-2) by force moreover have "IMG ?p = t" using p x elem_of_arr_of IMG_def arr_of_def by (metis (no_types, lifting) S.Dom.simps(1) S.Map.simps(1) image_empty image_insert image_restrict_eq) ultimately show "t ∈ S.set a" using S.set_def by blast qed qed lemma Map_via_comp: assumes "S.arr f" shows "S.Map f = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U)" proof fix x have "x ∉ S.Dom f ⟹ S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x" using assms arr_char [of f] IntD1 extensional_arb restrict_apply by fastforce moreover have "x ∈ S.Dom f ⟹ S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x" proof - assume x: "x ∈ S.Dom f" let ?X = "MkElem (arr_of x) (S.dom f)" have "«?X : S.unity → S.dom f»" using assms x MkElem_in_hom by auto moreover have "S.Dom ?X = {U} ∧ S.Map ?X = (λ_ ∈ {U}. x)" using x by simp ultimately have "S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) = compose {U} (S.Map f) (λ_ ∈ {U}. x)" using assms x S.Map_comp [of "MkElem (arr_of x) (S.dom f)" f] by (metis (mono_tags, lifting) S.Cod.simps(1) S.Dom_dom S.arr_iff_in_hom S.seqE S.seqI') thus ?thesis using x by (simp add: compose_eq restrict_apply' singletonI) qed ultimately show "S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x" by auto qed lemma arr_eqI': assumes "S.par f f'" and "⋀t. «t : S.unity → S.dom f» ⟹ f ⋅ t = f' ⋅ t" shows "f = f'" proof (intro S.arr_eqI) show "S.arr f" using assms by simp show "S.arr f'" using assms by simp show "S.Dom f = S.Dom f'" using assms by (metis (mono_tags, lifting) S.Dom_dom) show "S.Cod f = S.Cod f'" using assms by (metis (mono_tags, lifting) S.Cod_cod) show "S.Map f = S.Map f'" proof have 1: "⋀x. x ∈ S.Dom f ⟹ «MkElem (arr_of x) (S.dom f) : S.unity → S.dom f»" using MkElem_in_hom by (metis (mono_tags, lifting) assms(1)) fix x show "S.Map f x = S.Map f' x" using assms 1 ‹S.Dom f = S.Dom f'› by (simp add: Map_via_comp) qed qed lemma Setp_elem_of_img: assumes "A ∈ S.set ` Collect S.ide" shows "Setp (elem_of ` A)" proof - obtain a where a: "S.ide a ∧ S.set a = A" using assms by blast have "elem_of ` S.set a = S.Dom a" proof - have "S.set a = arr_of ` S.Dom a" using a set_char by blast moreover have "elem_of ` arr_of ` S.Dom a = S.Dom a" using elem_of_arr_of by force ultimately show ?thesis by presburger qed thus ?thesis using a S.ide_char⇩_{C}⇩_{C}by auto qed lemma set_MkIde_elem_of_img: assumes "A ⊆ S.Univ" and "S.ide (S.MkIde (elem_of ` A))" shows "S.set (S.MkIde (elem_of ` A)) = A" proof - have "S.Dom (S.MkIde (elem_of ` A)) = elem_of ` A" by simp moreover have "arr_of ` elem_of ` A = A" using assms arr_of_elem_of by force ultimately show ?thesis using assms Setp_elem_of_img set_char S.ide_MkIde by auto qed (* * We need this result, which characterizes what sets of terminals correspond * to sets. *) lemma set_img_Collect_ide_iff: shows "A ∈ S.set ` Collect S.ide ⟷ A ⊆ S.Univ ∧ Setp (elem_of ` A)" proof show "A ∈ S.set ` Collect S.ide ⟹ A ⊆ S.Univ ∧ Setp (elem_of ` A)" using set_char arr_of_mapsto Setp_elem_of_img by auto assume A: "A ⊆ S.Univ ∧ Setp (elem_of ` A)" have "S.ide (S.MkIde (elem_of ` A))" using A S.ide_MkIde by blast moreover have "S.set (S.MkIde (elem_of ` A)) = A" using A calculation set_MkIde_elem_of_img by presburger ultimately show "A ∈ S.set ` Collect S.ide" by blast qed text‹ The main result, which establishes the consistency of the ‹set_category› locale and provides us with a way of obtaining ``set categories'' at arbitrary types. › theorem is_set_category: shows "set_category comp (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))" proof show "∃img :: 'e setcat.arr ⇒ 'e setcat.arr. set_category_given_img comp img (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))" proof show "set_category_given_img comp IMG (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))" proof show "S.Univ ≠ {}" using terminal_char by blast fix a :: "'e setcat.arr" assume a: "S.ide a" show "S.set a ⊆ S.Univ ∧ Setp (elem_of ` S.set a)" using a set_img_Collect_ide_iff by auto show "inj_on IMG (S.hom S.unity a)" using a inj_IMG terminal_unity by blast next fix t :: "'e setcat.arr" assume t: "S.terminal t" show "t ∈ IMG ` S.hom S.unity t" proof - have "t ∈ S.set t" using t set_char [of t] by (metis (mono_tags, lifting) S.Dom.simps(1) image_insert insertI1 arr_of_def terminal_char S.terminal_def) thus ?thesis using t S.set_def [of t] by simp qed next show "⋀A. A ⊆ S.Univ ∧ Setp (elem_of ` A) ⟹ ∃a. S.ide a ∧ S.set a = A" using set_img_Collect_ide_iff by fast next fix a b :: "'e setcat.arr" assume a: "S.ide a" and b: "S.ide b" and ab: "S.set a = S.set b" show "a = b" using a b ab set_char inj_arr_of inj_image_eq_iff S.dom_char S.in_homE S.ide_in_hom by (metis (mono_tags, lifting)) next fix f f' :: "'e setcat.arr" assume par: "S.par f f'" and ff': "⋀x. «x : S.unity → S.dom f» ⟹ f ⋅ x = f' ⋅ x" show "f = f'" using par ff' arr_eqI' by blast next fix a b :: "'e setcat.arr" and F :: "'e setcat.arr ⇒ 'e setcat.arr" assume a: "S.ide a" and b: "S.ide b" and F: "F ∈ S.hom S.unity a → S.hom S.unity b" show "∃f. «f : a → b» ∧ (∀x. «x : S.unity → S.dom f» ⟶ f ⋅ x = F x)" proof let ?f = "S.MkArr (S.Dom a) (S.Dom b) (λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U)" have 1: "«?f : a → b»" proof - have "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U) ∈ extensional (S.Dom a) ∩ (S.Dom a → S.Dom b)" proof show "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U) ∈ extensional (S.Dom a)" using a F by simp show "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U) ∈ S.Dom a → S.Dom b" proof fix x assume x: "x ∈ S.Dom a" have "MkElem (arr_of x) a ∈ S.hom S.unity a" using x a MkElem_in_hom [of a x] S.ide_char S.ideD(1-2) by force hence 1: "F (MkElem (arr_of x) a) ∈ S.hom S.unity b" using F by auto moreover have "S.Dom (F (MkElem (arr_of x) a)) = {U}" using 1 MkElem_IMG by (metis (mono_tags, lifting) S.Dom.simps(1)) moreover have "S.Cod (F (MkElem (arr_of x) a)) = S.Dom b" using 1 by (metis (mono_tags, lifting) CollectD S.in_hom_char) ultimately have "S.Map (F (MkElem (arr_of x) a)) ∈ {U} → S.Dom b" using arr_char [of "F (MkElem (arr_of x) a)"] by blast thus "S.Map (F (MkElem (arr_of x) a)) U ∈ S.Dom b" by blast qed qed hence "«?f : S.MkIde (S.Dom a) → S.MkIde (S.Dom b)»" using a b S.MkArr_in_hom S.ide_char⇩_{C}⇩_{C}by blast thus ?thesis using a b by simp qed moreover have "⋀x. «x : S.unity → S.dom ?f» ⟹ ?f ⋅ x = F x" proof - fix x assume x: "«x : S.unity → S.dom ?f»" have 2: "x = MkElem (IMG x) a" using a x 1 MkElem_IMG [of x a] by (metis (mono_tags, lifting) S.in_homE mem_Collect_eq) moreover have 5: "S.Dom x = {U} ∧ S.Cod x = S.Dom a ∧ S.Map x = (λ_ ∈ {U}. elem_of (IMG x))" using x 2 by (metis (no_types, lifting) S.Cod.simps(1) S.Dom.simps(1) S.Map.simps(1)) moreover have "S.Cod ?f = S.Dom b" using 1 by simp ultimately have 3: "?f ⋅ x = S.MkArr {U} (S.Dom b) (compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)))" by (metis (no_types, lifting) "1" S.Map.simps(1) S.comp_MkArr S.in_homE x) have 4: "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) = S.Map (F x)" proof fix y have "y ∉ {U} ⟹ compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y" proof - assume y: "y ∉ {U}" have "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = undefined" using y compose_def extensional_arb by simp also have "... = S.Map (F x) y" proof - have 5: "F x ∈ S.hom S.unity b" using x F 1 by fastforce hence "S.Dom (F x) = {U}" by (metis (mono_tags, lifting) "2" CollectD S.Dom.simps(1) S.in_hom_char x) thus ?thesis using x y F 5 arr_char [of "F x"] extensional_arb [of "S.Map (F x)" "{U}" y] by (metis (mono_tags, lifting) CollectD Int_iff S.in_hom_char) qed ultimately show ?thesis by auto qed moreover have "y ∈ {U} ⟹ compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y" proof - assume y: "y ∈ {U}" have "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map ?f (elem_of (IMG x))" using y by (simp add: compose_eq restrict_apply') also have "... = (λx. S.Map (F (MkElem (arr_of x) a)) U) (elem_of (IMG x))" proof - have "elem_of (IMG x) ∈ S.Dom a" using x y a 5 arr_char S.in_homE restrict_apply by force thus ?thesis using restrict_apply by simp qed also have "... = S.Map (F x) y" using x y 1 2 MkElem_IMG [of x a] by simp finally show "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y" by auto qed ultimately show "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y" by auto qed show "?f ⋅ x = F x" proof (intro S.arr_eqI) have 5: "?f ⋅ x ∈ S.hom S.unity b" using 1 x by blast have 6: "F x ∈ S.hom S.unity b" using x F 1 by (metis (mono_tags, lifting) PiE S.in_homE mem_Collect_eq) show "S.arr (comp ?f x)" using 5 by blast show "S.arr (F x)" using 6 by blast show "S.Dom (comp ?f x) = S.Dom (F x)" using 5 6 by (metis (mono_tags, lifting) CollectD S.in_hom_char) show "S.Cod (comp ?f x) = S.Cod (F x)" using 5 6 by (metis (mono_tags, lifting) CollectD S.in_hom_char) show "S.Map (comp ?f x) = S.Map (F x)" using 3 4 by simp qed qed thus "«?f : a → b» ∧ (∀x. «x : S.unity → S.dom ?f» ⟶ comp ?f x = F x)" using 1 by blast qed next show "⋀A. A ⊆ S.Univ ∧ Setp (elem_of ` A) ⟹ A ⊆ S.Univ" by simp show "⋀A' A. ⟦A' ⊆ A; A ⊆ S.Univ ∧ Setp (elem_of ` A)⟧ ⟹ A' ⊆ S.Univ ∧ Setp (elem_of ` A')" by (meson image_mono setcat.Setp_respects_subset setcat_axioms subset_trans) show "⋀A B. ⟦A ⊆ S.Univ ∧ Setp (elem_of ` A); B ⊆ S.Univ ∧ Setp (elem_of ` B)⟧ ⟹ A ∪ B ⊆ S.Univ ∧ Setp (elem_of ` (A ∪ B))" by (simp add: image_Un union_preserves_Setp) qed qed qed text‹ ‹SetCat› can be viewed as a concrete set category over its own element type @{typ 'a}, using @{term arr_of} as the required injection from @{typ 'a} to the universe of ‹SetCat›. › corollary is_concrete_set_category: shows "concrete_set_category comp (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A)) UNIV arr_of" proof - interpret S': set_category comp ‹λA. A ⊆ S.Univ ∧ Setp (elem_of ` A)› using is_set_category by auto show ?thesis proof show 1: "arr_of ∈ UNIV → S'.Univ" using arr_of_def terminal_char by force show "inj_on arr_of UNIV" using inj_arr_of by blast qed qed text‹ As a consequence of the categoricity of the ‹set_category› axioms, if @{term S} interprets ‹set_category›, and if @{term φ} is a bijection between the universe of @{term S} and the elements of type @{typ 'a}, then @{term S} is isomorphic to the category ‹setcat› of @{typ 'a} sets and functions between them constructed here. › corollary set_category_iso_SetCat: fixes S :: "'s comp" and φ :: "'s ⇒ 'e" assumes "set_category S 𝒮" and "bij_betw φ (set_category_data.Univ S) UNIV" and "⋀A. 𝒮 A ⟷ A ⊆ set_category_data.Univ S ∧ (arr_of ∘ φ) ` A ∈ S.set ` Collect S.ide" shows "∃Φ. invertible_functor S comp Φ ∧ (∀m. set_category.incl S 𝒮 m ⟶ set_category.incl comp (λA. A ∈ S.set ` Collect S.ide) (Φ m))" proof - interpret S': set_category S 𝒮 using assms by auto let ?ψ = "inv_into S'.Univ φ" have "bij_betw (arr_of o φ) S'.Univ S.Univ" proof (intro bij_betwI) show "arr_of o φ ∈ S'.Univ → Collect S.terminal" using assms(2) arr_of_mapsto by auto show "?ψ o elem_of ∈ S.Univ → S'.Univ" proof fix x :: "'e setcat.arr" assume x: "x ∈ S.Univ" show "(inv_into S'.Univ φ ∘ elem_of) x ∈ S'.Univ" using x assms(2) bij_betw_def comp_apply inv_into_into by (metis UNIV_I) qed fix t assume "t ∈ S'.Univ" thus "(?ψ o elem_of) ((arr_of o φ) t) = t" using assms(2) bij_betw_inv_into_left by (metis comp_apply elem_of_arr_of) next fix t' :: "'e setcat.arr" assume "t' ∈ S.Univ" thus "(arr_of o φ) ((?ψ o elem_of) t') = t'" using assms(2) by (simp add: bij_betw_def f_inv_into_f) qed thus ?thesis using assms is_set_category set_img_Collect_ide_iff set_category_is_categorical [of S 𝒮 comp "λA. A ∈ S.set ` Collect S.ide" "arr_of o φ"] by simp qed sublocale category comp using is_category by blast sublocale set_category comp ‹λA. A ⊆ Collect S.terminal ∧ Setp (elem_of ` A)› using is_set_category set_img_Collect_ide_iff by simp interpretation concrete_set_category comp ‹λA. A ⊆ Collect S.terminal ∧ Setp (elem_of ` A)› UNIV arr_of using is_concrete_set_category by simp end (* interpretation SetCat: setcat undefined ‹λS. True› by unfold_locales auto *) text‹ Here we discard the temporary interpretations ‹S›, leaving only the exported definitions and facts. › context setcat begin text‹ We establish mappings to pass back and forth between objects and arrows of the category and sets and functions on the underlying elements. › interpretation set_category comp ‹λA. A ⊆ Collect terminal ∧ Setp (elem_of ` A)› using is_set_category by blast interpretation concrete_set_category comp ‹λA. A ⊆ Univ ∧ Setp (elem_of ` A)› UNIV arr_of using is_concrete_set_category by blast definition set_of_ide :: "'e setcat.arr ⇒ 'e set" where "set_of_ide a ≡ elem_of ` set a" definition ide_of_set :: "'e set ⇒ 'e setcat.arr" where "ide_of_set A ≡ mkIde (arr_of ` A)" lemma bij_betw_ide_set: shows "set_of_ide ∈ Collect ide → Collect Setp" and "ide_of_set ∈ Collect Setp → Collect ide" and [simp]: "ide a ⟹ ide_of_set (set_of_ide a) = a" and [simp]: "Setp A ⟹ set_of_ide (ide_of_set A) = A" and "bij_betw set_of_ide (Collect ide) (Collect Setp)" and "bij_betw ide_of_set (Collect Setp) (Collect ide)" proof - show 1: "set_of_ide ∈ Collect ide → Collect Setp" using setp_set_ide set_of_ide_def by auto show 2: "ide_of_set ∈ Collect Setp → Collect ide" proof fix A :: "'e set" assume A: "A ∈ Collect Setp" have "arr_of ` A ⊆ Univ" using A arr_of_mapsto by auto moreover have "Setp (elem_of ` arr_of ` A)" using A elem_of_arr_of Setp_respects_subset by simp ultimately have "ide (mkIde (arr_of ` A))" using ide_mkIde by blast thus "ide_of_set A ∈ Collect ide" using ide_of_set_def by simp qed show 3: "⋀a. ide a ⟹ ide_of_set (set_of_ide a) = a" using arr_of_img_elem_of_img ide_of_set_def mkIde_set set_of_ide_def setp_set_ide by presburger show 4: "⋀A. Setp A ⟹ set_of_ide (ide_of_set A) = A" proof - fix A :: "'e set" assume A: "Setp A" have "elem_of ` set (mkIde (arr_of ` A)) = elem_of ` arr_of ` A" proof - have "arr_of ` A ⊆ Univ" using A arr_of_mapsto by blast moreover have "Setp (elem_of ` arr_of ` A)" using A by simp ultimately have "set (mkIde (arr_of ` A)) = arr_of ` A" using A set_mkIde by blast thus ?thesis by auto qed also have "... = A" using A elem_of_arr_of by force finally show "set_of_ide (ide_of_set A) = A" using ide_of_set_def set_of_ide_def by simp qed show "bij_betw set_of_ide (Collect ide) (Collect Setp)" using 1 2 3 4 by (intro bij_betwI) blast+ show "bij_betw ide_of_set (Collect Setp) (Collect ide)" using 1 2 3 4 by (intro bij_betwI) blast+ qed definition fun_of_arr :: "'e setcat.arr ⇒ 'e ⇒ 'e" where "fun_of_arr f ≡ restrict (elem_of o Fun f o arr_of) (elem_of `Dom f)" definition arr_of_fun :: "'e set ⇒ 'e set ⇒ ('e ⇒ 'e) ⇒ 'e setcat.arr" where "arr_of_fun A B F ≡ mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of)" lemma bij_betw_hom_fun: shows "fun_of_arr ∈ hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)" and "⟦Setp A; Setp B⟧ ⟹ arr_of_fun A B ∈ (A → B) → hom (ide_of_set A) (ide_of_set B)" and "f ∈ hom a b ⟹ arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f" and "⟦Setp A; Setp B; F ∈ A → B; F ∈ extensional A⟧ ⟹ fun_of_arr (arr_of_fun A B F) = F" and "⟦ide a; ide b⟧ ⟹ bij_betw fun_of_arr (hom a b) (extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b))" and "⟦Setp A; Setp B⟧ ⟹ bij_betw (arr_of_fun A B) (extensional A ∩ (A → B)) (hom (ide_of_set A) (ide_of_set B))" proof - show 1: "⋀a b. fun_of_arr ∈ hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)" proof fix a b f assume f: "f ∈ hom a b" have Dom: "Dom f = arr_of ` set_of_ide a" using f set_of_ide_def by (metis (mono_tags, lifting) arr_dom arr_mkIde bij_betw_ide_set(3) ide_dom ide_of_set_def in_homE mem_Collect_eq set_mkIde) have Cod: "Cod f = arr_of ` set_of_ide b" using f set_of_ide_def by (metis (mono_tags, lifting) arr_cod arr_mkIde bij_betw_ide_set(3) ide_cod ide_of_set_def in_homE mem_Collect_eq set_mkIde) have "fun_of_arr f ∈ set_of_ide a → set_of_ide b" proof fix x assume x: "x ∈ set_of_ide a" have 1: "arr_of x ∈ Dom f" using x Dom by blast hence "Fun f (arr_of x) ∈ Cod f" using f Fun_mapsto Cod by blast hence "elem_of (Fun f (arr_of x)) ∈ set_of_ide b" using Cod by auto hence "restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f) x ∈ set_of_ide b" using 1 by force thus "fun_of_arr f x ∈ set_of_ide b" unfolding fun_of_arr_def by auto qed moreover have "fun_of_arr f ∈ extensional (set_of_ide a)" unfolding fun_of_arr_def using set_of_ide_def f by blast ultimately show "fun_of_arr f ∈ extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)" by blast qed show 2: "⋀A B. ⟦Setp A; Setp B⟧ ⟹ arr_of_fun A B ∈ (A → B) → hom (ide_of_set A) (ide_of_set B)" proof fix x and A B :: "'e set" assume A: "Setp A" and B: "Setp B" assume x: "x ∈ A → B" show "arr_of_fun A B x ∈ hom (ide_of_set A) (ide_of_set B)" proof show "«arr_of_fun A B x : ide_of_set A → ide_of_set B»" proof show 1: "arr (arr_of_fun A B x)" proof - have "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)" using A arr_of_mapsto elem_of_arr_of by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) moreover have "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)" using B arr_of_mapsto elem_of_arr_of by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) moreover have "arr_of ∘ x ∘ elem_of ∈ arr_of ` A → arr_of ` B" using x by auto ultimately show ?thesis unfolding arr_of_fun_def by blast qed show "dom (arr_of_fun A B x) = ide_of_set A" using 1 dom_mkArr ide_of_set_def arr_of_fun_def by simp show "cod (arr_of_fun A B x) = ide_of_set B" using 1 cod_mkArr ide_of_set_def arr_of_fun_def by simp qed qed qed show 3: "⋀a b f. f ∈ hom a b ⟹ arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f" proof - fix a b f assume f: "f ∈ hom a b" have 1: "Dom f = set a ∧ Cod f = set b" using f by blast have Dom: "Dom f ⊆ Univ ∧ Setp (elem_of ` Dom f)" using setp_set_ide f ide_dom by blast have Cod: "Cod f ⊆ Univ ∧ Setp (elem_of ` Cod f)" using setp_set_ide f ide_cod by blast have "mkArr (set a) (set b) (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) = mkArr (Dom f) (Cod f) (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of)" using 1 by simp also have "... = mkArr (Dom f) (Cod f) (Fun f)" proof (intro mkArr_eqI') show 2: "⋀x. x ∈ Dom f ⟹ (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x = Fun f x" proof - fix x assume x: "x ∈ Dom f" hence 1: "elem_of x ∈ elem_of ` Dom f" by blast have "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x = arr_of (restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f) (elem_of x))" by auto also have "... = arr_of ((elem_of o Fun f o arr_of) (elem_of x))" using 1 by auto also have "... = arr_of (elem_of (Fun f (arr_of (elem_of x))))" by auto also have "... = arr_of (elem_of (Fun f x))" using x arr_of_elem_of ‹Dom f ⊆ Univ ∧ Setp (elem_of ` Dom f)› by auto also have "... = Fun f x" using x f Dom Cod Fun_mapsto arr_of_elem_of [of "Fun f x"] by blast finally show "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x = Fun f x" by blast qed have "arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of ∈ Dom f → Cod f" proof fix x assume x: "x ∈ Dom f" have "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x = Fun f x" using 2 x by blast moreover have "... ∈ Cod f" using f x Fun_mapsto by blast ultimately show "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x ∈ Cod f" by argo qed thus "arr (mkArr (Dom f) (Cod f) (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of))" using Dom Cod by blast qed finally have "mkArr (set a) (set b) (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) = f" using f mkArr_Fun by (metis (no_types, lifting) in_homE mem_Collect_eq) thus "arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f" using 1 f by (metis (no_types, lifting) Cod Dom arr_of_img_elem_of_img arr_of_fun_def fun_of_arr_def set_of_ide_def) qed show 4: "⋀A B F. ⟦Setp A; Setp B; F ∈ A → B; F ∈ extensional A⟧ ⟹ fun_of_arr (arr_of_fun A B F) = F" proof fix F and A B :: "'e set" assume A: "Setp A" and B: "Setp B" assume F: "F ∈ A → B" and ext: "F ∈ extensional A" have 4: "arr (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of))" proof - have "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)" using A by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) moreover have "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)" using B by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) moreover have "arr_of ∘ F ∘ elem_of ∈ arr_of ` A → arr_of ` B" using F by auto ultimately show ?thesis by blast qed show "⋀x. fun_of_arr (arr_of_fun A B F) x = F x" proof - fix x have "fun_of_arr (arr_of_fun A B F) x = restrict (elem_of ∘ Fun (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) ∘ arr_of) A x" proof - have "elem_of ` Dom (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) = A" using A 4 elem_of_arr_of dom_mkArr set_of_ide_def bij_betw_ide_set(4) ide_of_set_def by auto thus ?thesis using arr_of_fun_def fun_of_arr_def by auto qed also have "... = F x" proof (cases "x ∈ A") show "x ∉ A ⟹ ?thesis" using ext extensional_arb by fastforce assume x: "x ∈ A" show "restrict (elem_of ∘ Fun (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) ∘ arr_of) A x = F x" using x 4 Fun_mkArr by simp qed finally show "fun_of_arr (arr_of_fun A B F) x = F x" by blast qed qed show "⟦Setp A; Setp B⟧ ⟹ bij_betw (arr_of_fun A B) (extensional A ∩ (A → B)) (hom (ide_of_set A) (ide_of_set B))" proof - assume A: "Setp A" and B: "Setp B" have "ide (ide_of_set A) ∧ ide (ide_of_set B)" using A B bij_betw_ide_set(2) by auto have "set_of_ide (ide_of_set A) = A ∧ set_of_ide (ide_of_set B) = B" using A B by simp show ?thesis using A B 1 [of "ide_of_set A" "ide_of_set B"] 2 3 4 apply (intro bij_betwI) apply auto apply blast by fastforce qed show "⟦ide a; ide b⟧ ⟹ bij_betw fun_of_arr (hom a b) (extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b))" proof (intro bij_betwI) assume a: "ide a" and b: "ide b" show "fun_of_arr ∈ hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)" using 1 by blast show "arr_of_fun (set_of_ide a) (set_of_ide b) ∈ extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b) → hom a b" using a b 2 [of "set_of_ide a" "set_of_ide b"] setp_set_ide set_of_ide_def bij_betw_ide_set(3) by auto show "⋀f. f ∈ hom a b ⟹ arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f" using a b 3 by blast show "⋀F. F ∈ extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b) ⟹ fun_of_arr (arr_of_fun (set_of_ide a) (set_of_ide b) F) = F" using a b 4 [of "set_of_ide a" "set_of_ide b"] by (metis (no_types, lifting) IntE set_of_ide_def setp_set_ide) qed qed lemma fun_of_arr_ide: assumes "ide a" shows "fun_of_arr a = restrict id (elem_of ` Dom a)" proof fix x show "fun_of_arr a x = restrict id (elem_of ` Dom a) x" proof (cases "x ∈ elem_of ` Dom a") show "x ∉ elem_of ` Dom a ⟹ ?thesis" using fun_of_arr_def extensional_arb by auto assume x: "x ∈ elem_of ` Dom a" have "fun_of_arr a x = restrict (elem_of ∘ Fun a ∘ arr_of) (elem_of ` Dom a) x" using x fun_of_arr_def by simp also have "... = elem_of (Fun a (arr_of x))" using x by auto also have "... = elem_of ((λx∈set a. x) (arr_of x))" using assms x Fun_ide by auto also have "... = elem_of (arr_of x)" proof - have "x ∈ elem_of ` set a" using assms x ideD(2) by force hence "arr_of x ∈ set a" by (metis (mono_tags, lifting) arr_of_img_elem_of_img assms image_eqI setp_set_ide) thus ?thesis by simp qed also have "... = x" by simp also have "... = restrict id (elem_of ` Dom a) x" using x by auto finally show ?thesis by blast qed qed lemma arr_of_fun_id: assumes "Setp A" shows "arr_of_fun A A (restrict id A) = ide_of_set A" proof - have A: "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)" using assms elem_of_arr_of by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) have "arr_of_fun A A (restrict id A) = mkArr (arr_of ` A) (arr_of ` A) (arr_of ∘ restrict id A ∘ elem_of)" unfolding arr_of_fun_def by simp also have "... = mkArr (arr_of ` A) (arr_of ` A) (λx. x)" using A arr_mkArr by (intro mkArr_eqI') auto also have "... = ide_of_set A" using A ide_of_set_def mkIde_as_mkArr by simp finally show ?thesis by blast qed lemma fun_of_arr_comp: assumes "f ∈ hom a b" and "g ∈ hom b c" shows "fun_of_arr (comp g f) = restrict (fun_of_arr g ∘ fun_of_arr f) (set_of_ide a)" proof - have 1: "seq g f" using assms by blast have "fun_of_arr (comp g f) = restrict (elem_of ∘ Fun (comp g f) ∘ arr_of) (elem_of ` Dom (comp g f))" unfolding fun_of_arr_def by blast also have "... = restrict (elem_of ∘ Fun (comp g f) ∘ arr_of) (elem_of ` Dom f)" using assms dom_comp seqI' by auto also have "... = restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of) (elem_of ` Dom f)" using 1 Fun_comp by auto also have "... = restrict (restrict (elem_of o Fun g o arr_of) (elem_of ` Dom g) ∘ restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f)) (elem_of ` Dom f)" proof fix x show "restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of) (elem_of ` Dom f) x = restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) (elem_of ` Dom f) x" proof (cases "x ∈ elem_of ` Dom f") show "x ∉ elem_of ` Dom f ⟹ ?thesis" by auto assume x: "x ∈ elem_of ` Dom f" have 2: "arr_of x ∈ Dom f" proof - have "arr_of x ∈ arr_of ` elem_of ` Dom f" using x by simp thus ?thesis by (metis (no_types, lifting) 1 arr_of_img_elem_of_img ide_dom seqE setp_set_ide) qed have 3: "Dom g = Cod f" using assms by fastforce have "restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of) (elem_of ` Dom f) x = elem_of (Fun g (Fun f (arr_of x)))" using x 2 by simp also have "... = restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) (elem_of ` Dom f) x" proof - have "restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) (elem_of ` Dom f) x = elem_of (Fun g (Fun f (arr_of x)))" proof - have "restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) (elem_of ` Dom f) x = (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) o restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) x" using 2 by force also have "... = restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) (restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) x)" by simp also have "... = restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) (elem_of (Fun f (arr_of x)))" using 2 by force also have "... = (elem_of o Fun g o arr_of) (elem_of (Fun f (arr_of x)))" proof - have "elem_of (Fun f (arr_of x)) ∈ elem_of ` Dom g" using assms 2 3 Fun_mapsto [of f] by blast thus ?thesis by simp qed also have "... = elem_of (Fun g (arr_of (elem_of (Fun f (arr_of x)))))" by simp also have "... = elem_of (Fun g (Fun f (arr_of x)))" proof - have "Fun f (arr_of x) ∈ Univ" using assms 2 setp_set_ide ide_cod Fun_mapsto by blast thus ?thesis using 2 by simp qed finally show ?thesis by blast qed thus ?thesis by simp qed finally show ?thesis by blast qed qed also have "... = restrict (fun_of_arr g o fun_of_arr f) (elem_of ` Dom f)" unfolding fun_of_arr_def by blast finally show ?thesis unfolding set_of_ide_def using assms by blast qed lemma arr_of_fun_comp: assumes "Setp A" and "Setp B" and "Setp C" and "F ∈ extensional A ∩ (A → B)" and "G ∈ extensional B ∩ (B → C)" shows "arr_of_fun A C (G o F) = comp (arr_of_fun B C G) (arr_of_fun A B F)" proof - have A: "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)" using assms elem_of_arr_of by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) have B: "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)" using assms elem_of_arr_of by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) have C: "arr_of ` C ⊆ Univ ∧ Setp (elem_of ` arr_of ` C)" using assms elem_of_arr_of by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2) ide_implies_incl ide_of_set_def incl_def mem_Collect_eq) have "arr_of_fun A C (G o F) = mkArr (arr_of ` A) (arr_of ` C) (arr_of ∘ (G ∘ F) ∘ elem_of)" unfolding arr_of_fun_def by simp also have "... = mkArr (arr_of ` A) (arr_of ` C) ((arr_of ∘ G ∘ elem_of) o (arr_of o F ∘ elem_of))" proof (intro mkArr_eqI') show "arr (mkArr (arr_of ` A) (arr_of ` C) (arr_of ∘ (G ∘ F) ∘ elem_of))" proof - have "arr_of ∘ (G ∘ F) ∘ elem_of ∈ arr_of ` A → arr_of ` C" using assms by force thus ?thesis using A B C by blast qed show "⋀x. x ∈ arr_of ` A ⟹ (arr_of ∘ (G ∘ F) ∘ elem_of) x = ((arr_of ∘ G ∘ elem_of) o (arr_of o F ∘ elem_of)) x" by simp qed also have "... = comp (mkArr (arr_of ` B) (arr_of ` C) (arr_of ∘ G ∘ elem_of)) (mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of))" proof - have "arr (mkArr (arr_of ` B) (arr_of ` C) (arr_of ∘ G ∘ elem_of))" using assms B C elem_of_arr_of by fastforce moreover have "arr (mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of))" using assms A B elem_of_arr_of by fastforce ultimately show ?thesis using comp_mkArr by auto qed also have "... = comp (arr_of_fun B C G) (arr_of_fun A B F)" using arr_of_fun_def by presburger finally show ?thesis by blast qed end text‹ When there is no restriction on the sets that determine objects, the resulting set category is replete. This is the normal use case, which we want to streamline as much as possible, so it is useful to introduce a special locale for this purpose. › locale replete_setcat = fixes elem_type :: "'e itself" begin interpretation SC: setcat elem_type ‹λ_. True› by unfold_locales blast definition comp where "comp ≡ SC.comp" definition arr_of where "arr_of ≡ SC.arr_of" definition elem_of where "elem_of ≡ SC.elem_of" sublocale replete_set_category comp unfolding comp_def using SC.is_set_category replete_set_category_def set_category_def by auto lemma is_replete_set_category: shows "replete_set_category comp" .. lemma is_set_category⇩_{R}⇩_{S}⇩_{C}: shows "set_category comp (λA. A ⊆ Univ)" using is_set_category by blast sublocale concrete_set_category comp setp UNIV arr_of using SC.is_concrete_set_category comp_def SC.set_img_Collect_ide_iff arr_of_def by auto lemma is_concrete_set_category: shows "concrete_set_category comp setp UNIV arr_of" .. lemma bij_arr_of: shows "bij_betw arr_of UNIV Univ" using SC.bij_arr_of comp_def arr_of_def by presburger lemma bij_elem_of: shows "bij_betw elem_of Univ UNIV" using SC.bij_elem_of comp_def elem_of_def by auto end (* interpretation RepleteSetCat: replete_setcat undefined . *) end