(* Title: SetCategory Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter SetCategory theory SetCategory imports Category Functor Subcategory begin text‹ This theory defines a locale ‹set_category› that axiomatizes the notion ``category of @{typ 'a}-sets and functions between them'' in the context of HOL. A primary reason for doing this is to make it possible to prove results (such as the Yoneda Lemma) that use such categories without having to commit to a particular element type @{typ 'a} and without having the results depend on the concrete details of a particular construction. The axiomatization given here is categorical, in the sense that if categories @{term S} and @{term S'} each interpret the ‹set_category› locale, then a bijection between the sets of terminal objects of @{term S} and @{term S'} extends to an isomorphism of @{term S} and @{term S'} as categories. The axiomatization is based on the following idea: if, for some type @{typ 'a}, category @{term S} is the category of all @{typ 'a}-sets and functions between them, then the elements of type @{typ 'a} are in bijective correspondence with the terminal objects of category @{term S}. In addition, if @{term unity} is an arbitrarily chosen terminal object of @{term S}, then for each object @{term a}, the hom-set @{term "hom unity a"} (\emph{i.e.} the set of ``points'' or ``global elements'' of @{term a}) is in bijective correspondence with a subset of the terminal objects of @{term S}. By making a specific, but arbitrary, choice of such a correspondence, we can then associate with each object @{term a} of @{term S} a set @{term "set a"} that consists of all terminal objects @{term t} that correspond to some point @{term x} of @{term a}. Each arrow @{term f} then induces a function ‹Fun f ∈ set (dom f) → set (cod f)›, defined on terminal objects of @{term S} by passing to points of @{term "dom f"}, composing with @{term f}, then passing back from points of @{term "cod f"} to terminal objects. Once we can associate a set with each object of @{term S} and a function with each arrow, we can force @{term S} to be isomorphic to the category of @{typ 'a}-sets by imposing suitable extensionality and completeness axioms. › section "Some Lemmas about Restriction" text‹ \sloppypar The development of the ‹set_category› locale makes heavy use of the theory @{theory "HOL-Library.FuncSet"}. However, in some cases, I found that that theory did not provide results about restriction in the form that was most useful to me. I used the following additional results in various places. › (* This variant of FuncSet.restrict_ext is sometimes useful. *) lemma restr_eqI: assumes "A = A'" and "⋀x. x ∈ A ⟹ F x = F' x" shows "restrict F A = restrict F' A'" using assms by force (* This rule avoided a long proof in at least one instance where FuncSet.restrict_apply did not work. *) lemma restr_eqE [elim]: assumes "restrict F A = restrict F' A" and "x ∈ A" shows "F x = F' x" using assms restrict_def by metis (* This seems more useful than compose_eq in FuncSet. *) lemma compose_eq' [simp]: shows "compose A G F = restrict (G o F) A" unfolding compose_def restrict_def by auto section "Set Categories" text‹ We first define the locale ‹set_category_data›, which sets out the basic data and definitions for the ‹set_category› locale, without imposing any conditions other than that @{term S} is a category and that @{term img} is a function defined on the arrow type of @{term S}. The function @{term img} should be thought of as a mapping that takes a point @{term "x ∈ hom unity a"} to a corresponding terminal object @{term "img x"}. Eventually, assumptions will be introduced so that this is in fact the case. The set of terminal objects of the category will serve as abstract ``elements'' of sets; we will refer to the set of \emph{all} terminal objects as the \emph{universe}. › locale set_category_data = category S for S :: "'s comp" (infixr "⋅" 55) and img :: "'s ⇒ 's" begin notation in_hom ("«_ : _ → _»") text‹ Call the set of all terminal objects of S the ``universe''. › abbreviation Univ :: "'s set" where "Univ ≡ Collect terminal" text‹ Choose an arbitrary element of the universe and call it @{term unity}. › definition unity :: 's where "unity = (SOME t. terminal t)" text‹ Each object @{term a} determines a subset @{term "set a"} of the universe, consisting of all those terminal objects @{term t} such that @{term "t = img x"} for some @{term "x ∈ hom unity a"}. › definition set :: "'s ⇒ 's set" where "set a = img ` hom unity a" end text‹ Next, we define a locale ‹set_category_given_img› that augments the ‹set_category_data› locale with assumptions that serve to define the notion of a set category with a chosen correspondence between points and terminal objects. The assumptions require that the universe be nonempty (so that the definition of @{term unity} makes sense), that the map @{term img} is a locally injective map taking points to terminal objects, that each terminal object @{term t} belongs to @{term "set t"}, that two objects of @{term S} are equal if they determine the same set, that two parallel arrows of @{term S} are equal if they determine the same function, and that for any objects @{term a} and @{term b} and function @{term "F ∈ hom unity a → hom unity b"} there is an arrow @{term "f ∈ hom a b"} whose action under the composition of @{term S} coincides with the function @{term F}. The parameter @{term setp} is a predicate that determines which subsets of the universe are to be regarded as defining objects of the category. This parameter has been introduced because most of the characteristic properties of a category of sets and functions do not depend on there being an object corresponding to \emph{every} subset of the universe, and we intend to consider in particular the cases in which only finite subsets or only ``small'' subsets of the universe determine objects. Accordingly, we assume that there is an object corresponding to each subset of the universe that satisfies @{term setp}. It is also necessary to assume some basic regularity properties of the predicate @{term setp}; namely, that it holds for all subsets of the universe corresponding to objects of @{term S}, and that it respects subset and union. › locale set_category_given_img = set_category_data S img for S :: "'s comp" (infixr "⋅" 55) and img :: "'s ⇒ 's" and setp :: "'s set ⇒ bool" + assumes setp_imp_subset_Univ: "setp A ⟹ A ⊆ Univ" and setp_set_ide: "ide a ⟹ setp (set a)" and setp_respects_subset: "A' ⊆ A ⟹ setp A ⟹ setp A'" and setp_respects_union: "⟦ setp A; setp B ⟧ ⟹ setp (A ∪ B)" and nonempty_Univ: "Univ ≠ {}" and inj_img: "ide a ⟹ inj_on img (hom unity a)" and stable_img: "terminal t ⟹ t ∈ img ` hom unity t" and extensional_set: "⟦ ide a; ide b; set a = set b ⟧ ⟹ a = b" and extensional_arr: "⟦ par f f'; ⋀x. «x : unity → dom f» ⟹ f ⋅ x = f' ⋅ x ⟧ ⟹ f = f'" and set_complete: "setp A ⟹ ∃a. ide a ∧ set a = A" and fun_complete_ax: "⟦ ide a; ide b; F ∈ hom unity a → hom unity b ⟧ ⟹ ∃f. «f : a → b» ∧ (∀x. «x : unity → dom f» ⟶ f ⋅ x = F x)" begin lemma setp_singleton: assumes "terminal a" shows "setp {a}" using assms by (metis setp_set_ide Set.set_insert Un_upper1 insert_is_Un set_def setp_respects_subset stable_img terminal_def) lemma setp_empty: shows "setp {}" using setp_singleton setp_respects_subset nonempty_Univ by blast lemma finite_imp_setp: assumes "A ⊆ Univ" and "finite A" shows "setp A" using setp_empty setp_singleton setp_respects_union by (metis assms(1-2) finite_subset_induct insert_is_Un mem_Collect_eq) text‹ Each arrow @{term "f ∈ hom a b"} determines a function @{term "Fun f ∈ Univ → Univ"}, by passing from @{term Univ} to @{term "hom a unity"}, composing with @{term f}, then passing back to @{term Univ}. › definition Fun :: "'s ⇒ 's ⇒ 's" where "Fun f = restrict (img o S f o inv_into (hom unity (dom f)) img) (set (dom f))" lemma comp_arr_point⇩_{S}⇩_{C}: assumes "arr f" and "«x : unity → dom f»" shows "f ⋅ x = inv_into (hom unity (cod f)) img (Fun f (img x))" proof - have "«f ⋅ x : unity → cod f»" using assms by blast thus ?thesis using assms Fun_def inj_img set_def by simp qed text‹ Parallel arrows that determine the same function are equal. › lemma arr_eqI⇩_{S}⇩_{C}: assumes "par f f'" and "Fun f = Fun f'" shows "f = f'" using assms comp_arr_point⇩_{S}⇩_{C}extensional_arr by metis lemma terminal_unity⇩_{S}⇩_{C}: shows "terminal unity" using unity_def nonempty_Univ by (simp add: someI_ex) lemma ide_unity [simp]: shows "ide unity" using terminal_unity⇩_{S}⇩_{C}terminal_def by blast lemma setp_set' [simp]: assumes "ide a" shows "setp (set a)" using assms setp_set_ide by auto lemma inj_on_set: shows "inj_on set (Collect ide)" using extensional_set by (intro inj_onI, auto) text‹ The inverse of the map @{term set} is a map @{term mkIde} that takes each subset of the universe to an identity of @{term[source=true] S}. › definition mkIde :: "'s set ⇒ 's" where "mkIde A = (if setp A then inv_into (Collect ide) set A else null)" lemma mkIde_set [simp]: assumes "ide a" shows "mkIde (set a) = a" by (simp add: assms inj_on_set mkIde_def) lemma set_mkIde [simp]: assumes "setp A" shows "set (mkIde A) = A" using assms mkIde_def set_complete someI_ex [of "λa. a ∈ Collect ide ∧ set a = A"] mkIde_set by metis lemma ide_mkIde [simp]: assumes "setp A" shows "ide (mkIde A)" using assms mkIde_def mkIde_set set_complete by metis lemma arr_mkIde [iff]: shows "arr (mkIde A) ⟷ setp A" using not_arr_null mkIde_def ide_mkIde by auto lemma dom_mkIde [simp]: assumes "setp A" shows "dom (mkIde A) = mkIde A" using assms ide_mkIde by simp lemma cod_mkIde [simp]: assumes "setp A" shows "cod (mkIde A) = mkIde A" using assms ide_mkIde by simp text‹ Each arrow @{term f} determines an extensional function from @{term "set (dom f)"} to @{term "set (cod f)"}. › lemma Fun_mapsto: assumes "arr f" shows "Fun f ∈ extensional (set (dom f)) ∩ (set (dom f) → set (cod f))" proof show "Fun f ∈ extensional (set (dom f))" using Fun_def by fastforce show "Fun f ∈ set (dom f) → set (cod f)" proof fix t assume t: "t ∈ set (dom f)" have "Fun f t = img (f ⋅ inv_into (hom unity (dom f)) img t)" using assms t Fun_def comp_def by simp moreover have "... ∈ set (cod f)" using assms t set_def inv_into_into [of t img "hom unity (dom f)"] by blast ultimately show "Fun f t ∈ set (cod f)" by auto qed qed text‹ Identities of @{term[source=true] S} correspond to restrictions of the identity function. › lemma Fun_ide: assumes "ide a" shows "Fun a = restrict (λx. x) (set a)" using assms Fun_def inj_img set_def comp_cod_arr by fastforce lemma Fun_mkIde [simp]: assumes "setp A" shows "Fun (mkIde A) = restrict (λx. x) A" using assms ide_mkIde set_mkIde Fun_ide by simp text‹ Composition in @{term S} corresponds to extensional function composition. › lemma Fun_comp [simp]: assumes "seq g f" shows "Fun (g ⋅ f) = restrict (Fun g o Fun f) (set (dom f))" proof - have "restrict (img o S (g ⋅ f) o (inv_into (hom unity (dom (g ⋅ f))) img)) (set (dom (g ⋅ f))) = restrict (Fun g o Fun f) (set (dom f))" proof - let ?img' = "λa. λt. inv_into (hom unity a) img t" have 1: "set (dom (g ⋅ f)) = set (dom f)" using assms by auto moreover have "⋀t. t ∈ set (dom (g ⋅ f)) ⟹ (img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = (Fun g o Fun f) t" proof - fix t assume "t ∈ set (dom (g ⋅ f))" hence t: "t ∈ set (dom f)" by (simp add: 1) have "(img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = img (g ⋅ f ⋅ ?img' (dom f) t)" using assms dom_comp comp_assoc by simp also have "... = img (g ⋅ ?img' (dom g) (Fun f t))" proof - have "⋀a x. x ∈ hom unity a ⟹ ?img' a (img x) = x" using assms inj_img ide_cod inv_into_f_eq by (metis arrI in_homE mem_Collect_eq) thus ?thesis using assms t Fun_def set_def comp_arr_point⇩_{S}⇩_{C}by auto qed also have "... = Fun g (Fun f t)" proof - have "Fun f t ∈ img ` hom unity (cod f)" using assms t Fun_mapsto set_def by fast thus ?thesis using assms by (auto simp add: set_def Fun_def) qed finally show "(img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = (Fun g o Fun f) t" by auto qed ultimately show ?thesis by auto qed thus ?thesis using Fun_def by auto qed text‹ The constructor @{term mkArr} is used to obtain an arrow given subsets @{term A} and @{term B} of the universe and a function @{term "F ∈ A → B"}. › definition mkArr :: "'s set ⇒ 's set ⇒ ('s ⇒ 's) ⇒ 's" where "mkArr A B F = (if setp A ∧ setp B ∧ F ∈ A → B then (THE f. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F A) else null)" text‹ Each function @{term "F ∈ set a → set b"} determines a unique arrow @{term "f ∈ hom a b"}, such that @{term "Fun f"} is the restriction of @{term F} to @{term "set a"}. › lemma fun_complete: assumes "ide a" and "ide b" and "F ∈ set a → set b" shows "∃!f. «f : a → b» ∧ Fun f = restrict F (set a)" proof - let ?P = "λf. «f : a → b» ∧ Fun f = restrict F (set a)" show "∃!f. ?P f" proof have "∃f. ?P f" proof - let ?F' = "λx. inv_into (hom unity b) img (F (img x))" have "?F' ∈ hom unity a → hom unity b" proof fix x assume x: "x ∈ hom unity a" have "F (img x) ∈ set b" using assms(3) x set_def by auto thus "inv_into (hom unity b) img (F (img x)) ∈ hom unity b" using assms setp_set_ide inj_img set_def by auto qed hence "∃f. «f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = ?F' x)" using assms fun_complete_ax [of a b] by force from this obtain f where f: "«f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = ?F' x)" by blast let ?img' = "λa. λt. inv_into (hom unity a) img t" have "Fun f = restrict F (set a)" proof (unfold Fun_def, intro restr_eqI) show "set (dom f) = set a" using f by auto show "⋀t. t ∈ set (dom f) ⟹ (img ∘ S f ∘ ?img' (dom f)) t = F t" proof - fix t assume t: "t ∈ set (dom f)" have "(img ∘ S f ∘ ?img' (dom f)) t = img (f ⋅ ?img' (dom f) t)" by simp also have "... = img (?F' (?img' (dom f) t))" by (metis f in_homE inv_into_into set_def mem_Collect_eq t) also have "... = img (?img' (cod f) (F t))" using f t set_def inj_img by auto also have "... = F t" proof - have "F t ∈ set (cod f)" using assms f t by auto thus ?thesis using f t set_def inj_img by auto qed finally show "(img ∘ S f ∘ ?img' (dom f)) t = F t" by auto qed qed thus ?thesis using f by blast qed thus F: "?P (SOME f. ?P f)" using someI_ex [of ?P] by fast show "⋀f'. ?P f' ⟹ f' = (SOME f. ?P f)" using F arr_eqI⇩_{S}⇩_{C}by (metis (no_types, lifting) in_homE) qed qed lemma mkArr_in_hom: assumes "setp A" and "setp B" and "F ∈ A → B" shows "«mkArr A B F : mkIde A → mkIde B»" using assms mkArr_def fun_complete [of "mkIde A" "mkIde B" F] ide_mkIde set_mkIde theI' [of "λf. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F A"] setp_imp_subset_Univ by simp text‹ The ``only if'' direction of the next lemma can be achieved only if there exists a non-arrow element of type @{typ 's}, which can be used as the value of @{term "mkArr A B F"} in cases where @{term "F ∉ A → B"}. Nevertheless, it is essential to have this, because without the ``only if'' direction, we can't derive any useful consequences from an assumption of the form @{term "arr (mkArr A B F)"}; instead we have to obtain @{term "F ∈ A → B"} some other way. This is is usually highly inconvenient and it makes the theory very weak and almost unusable in practice. The observation that having a non-arrow value of type @{typ 's} solves this problem is ultimately what led me to incorporate @{term null} first into the definition of the ‹set_category› locale and then, ultimately, into the definition of the ‹category› locale. I believe this idea is critical to the usability of the entire development. › lemma arr_mkArr [iff]: shows "arr (mkArr A B F) ⟷ setp A ∧ setp B ∧ F ∈ A → B" proof show "arr (mkArr A B F) ⟹ setp A ∧ setp B ∧ F ∈ A → B" using mkArr_def not_arr_null ex_un_null someI_ex [of "λf. ¬arr f"] setp_imp_subset_Univ by metis show "setp A ∧ setp B ∧ F ∈ A → B ⟹ arr (mkArr A B F)" using mkArr_in_hom by auto qed lemma arr_mkArrI [intro]: assumes "setp A" and "setp B" and "F ∈ A → B" shows "arr (mkArr A B F)" using assms arr_mkArr by blast lemma Fun_mkArr': assumes "arr (mkArr A B F)" shows "«mkArr A B F : mkIde A → mkIde B»" and "Fun (mkArr A B F) = restrict F A" proof - have 1: "setp A ∧ setp B ∧ F ∈ A → B" using assms by fast have 2: "mkArr A B F ∈ hom (mkIde A) (mkIde B) ∧ Fun (mkArr A B F) = restrict F (set (mkIde A))" proof - have "∃!f. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F (set (mkIde A))" using 1 fun_complete [of "mkIde A" "mkIde B" F] ide_mkIde set_mkIde by simp thus ?thesis using 1 mkArr_def theI' set_mkIde by simp qed show "«mkArr A B F : mkIde A → mkIde B»" using 1 2 by auto show "Fun (mkArr A B F) = restrict F A" using 1 2 set_mkIde by auto qed lemma mkArr_Fun: assumes "arr f" shows "mkArr (set (dom f)) (set (cod f)) (Fun f) = f" proof - have 1: "setp (set (dom f)) ∧ setp (set (cod f)) ∧ ide (dom f) ∧ ide (cod f) ∧ Fun f ∈ extensional (set (dom f)) ∩ (set (dom f) → set (cod f))" using Fun_mapsto assms ide_cod ide_dom setp_set' by presburger hence "∃!f'. f' ∈ hom (dom f) (cod f) ∧ Fun f' = restrict (Fun f) (set (dom f))" using fun_complete by force moreover have "f ∈ hom (dom f) (cod f) ∧ Fun f = restrict (Fun f) (set (dom f))" using assms 1 extensional_restrict by force ultimately have "f = (THE f'. f' ∈ hom (dom f) (cod f) ∧ Fun f' = restrict (Fun f) (set (dom f)))" using theI' [of "λf'. f' ∈ hom (dom f) (cod f) ∧ Fun f' = restrict (Fun f) (set (dom f))"] by blast also have "... = mkArr (set (dom f)) (set (cod f)) (Fun f)" using assms 1 mkArr_def mkIde_set by simp finally show ?thesis by auto qed lemma dom_mkArr [simp]: assumes "arr (mkArr A B F)" shows "dom (mkArr A B F) = mkIde A" using assms Fun_mkArr' by auto lemma cod_mkArr [simp]: assumes "arr (mkArr A B F)" shows "cod (mkArr A B F) = mkIde B" using assms Fun_mkArr' by auto lemma Fun_mkArr [simp]: assumes "arr (mkArr A B F)" shows "Fun (mkArr A B F) = restrict F A" using assms Fun_mkArr' by auto text‹ The following provides the basic technique for showing that arrows constructed using @{term mkArr} are equal. › lemma mkArr_eqI [intro]: assumes "arr (mkArr A B F)" and "A = A'" and "B = B'" and "⋀x. x ∈ A ⟹ F x = F' x" shows "mkArr A B F = mkArr A' B' F'" using assms Fun_mkArr by (intro arr_eqI⇩_{S}⇩_{C}, auto simp add: Pi_iff) text‹ This version avoids trivial proof obligations when the domain and codomain sets are identical from the context. › lemma mkArr_eqI' [intro]: assumes "arr (mkArr A B F)" and "⋀x. x ∈ A ⟹ F x = F' x" shows "mkArr A B F = mkArr A B F'" using assms mkArr_eqI by simp lemma mkArr_restrict_eq: assumes "arr (mkArr A B F)" shows "mkArr A B (restrict F A) = mkArr A B F" using assms by (intro mkArr_eqI', auto) lemma mkArr_restrict_eq': assumes "arr (mkArr A B (restrict F A))" shows "mkArr A B (restrict F A) = mkArr A B F" using assms by (intro mkArr_eqI', auto) lemma mkIde_as_mkArr [simp]: assumes "setp A" shows "mkArr A A (λx. x) = mkIde A" using assms arr_mkIde dom_mkIde cod_mkIde Fun_mkIde by (intro arr_eqI⇩_{S}⇩_{C}, auto) lemma comp_mkArr: assumes "arr (mkArr A B F)" and "arr (mkArr B C G)" shows "mkArr B C G ⋅ mkArr A B F = mkArr A C (G ∘ F)" proof (intro arr_eqI⇩_{S}⇩_{C}) have 1: "seq (mkArr B C G) (mkArr A B F)" using assms by force have 2: "G o F ∈ A → C" using assms by auto show "par (mkArr B C G ⋅ mkArr A B F) (mkArr A C (G ∘ F))" using assms 1 2 by (intro conjI) simp_all show "Fun (mkArr B C G ⋅ mkArr A B F) = Fun (mkArr A C (G ∘ F))" using 1 2 by fastforce qed text‹ The locale assumption @{prop stable_img} forces @{term "t ∈ set t"} in case @{term t} is a terminal object. This is very convenient, as it results in the characterization of terminal objects as identities @{term t} for which @{term "set t = {t}"}. However, it is not absolutely necessary to have this. The following weaker characterization of terminal objects can be proved without the @{prop stable_img} assumption. › lemma terminal_char1: shows "terminal t ⟷ ide t ∧ (∃!x. x ∈ set t)" proof - have "terminal t ⟹ ide t ∧ (∃!x. x ∈ set t)" proof - assume t: "terminal t" have "ide t" using t terminal_def by auto moreover have "∃!x. x ∈ set t" proof - have "∃!x. x ∈ hom unity t" using t terminal_unity⇩_{S}⇩_{C}terminal_def by auto thus ?thesis using set_def by auto qed ultimately show "ide t ∧ (∃!x. x ∈ set t)" by auto qed moreover have "ide t ∧ (∃!x. x ∈ set t) ⟹ terminal t" proof - assume t: "ide t ∧ (∃!x. x ∈ set t)" from this obtain t' where "set t = {t'}" by blast hence t': "set t = {t'} ∧ setp {t'} ∧ t = mkIde {t'}" using t setp_set_ide mkIde_set by metis show "terminal t" proof show "ide t" using t by simp show "⋀a. ide a ⟹ ∃!f. «f : a → t»" proof - fix a assume a: "ide a" show "∃!f. «f : a → t»" proof show 1: "«mkArr (set a) {t'} (λx. t') : a → t»" using a t t' mkArr_in_hom by (metis Pi_I' mkIde_set setp_set_ide singletonD) show "⋀f. «f : a → t» ⟹ f = mkArr (set a) {t'} (λx. t')" proof - fix f assume f: "«f : a → t»" show "f = mkArr (set a) {t'} (λx. t')" proof (intro arr_eqI⇩_{S}⇩_{C}) show 1: "par f (mkArr (set a) {t'} (λx. t'))" using 1 f in_homE by metis show "Fun f = Fun (mkArr (set a) {t'} (λx. t'))" proof - have "Fun (mkArr (set a) {t'} (λx. t')) = (λx∈set a. t')" using 1 Fun_mkArr by simp also have "... = Fun f" proof - have "⋀x. x ∈ set a ⟹ Fun f x = t'" using f t' Fun_def mkArr_Fun arr_mkArr by (metis PiE in_homE singletonD) moreover have "⋀x. x ∉ set a ⟹ Fun f x = undefined" using f Fun_def by auto ultimately show ?thesis by auto qed finally show ?thesis by force qed qed qed qed qed qed qed ultimately show ?thesis by blast qed text‹ As stated above, in the presence of the @{prop stable_img} assumption we have the following stronger characterization of terminal objects. › lemma terminal_char2: shows "terminal t ⟷ ide t ∧ set t = {t}" proof assume t: "terminal t" show "ide t ∧ set t = {t}" proof show "ide t" using t terminal_char1 by auto show "set t = {t}" proof - have "∃!x. x ∈ hom unity t" using t terminal_def terminal_unity⇩_{S}⇩_{C}by force moreover have "t ∈ img ` hom unity t" using t stable_img set_def by simp ultimately show ?thesis using set_def by auto qed qed next assume "ide t ∧ set t = {t}" thus "terminal t" using terminal_char1 by force qed end text‹ At last, we define the ‹set_category› locale by existentially quantifying out the choice of a particular @{term img} map. We need to know that such a map exists, but it does not matter which one we choose. › locale set_category = category S for S :: "'s comp" (infixr "⋅" 55) and setp :: "'s set ⇒ bool" + assumes ex_img: "∃img. set_category_given_img S img setp" begin notation in_hom ("«_ : _ → _»") definition some_img where "some_img = (SOME img. set_category_given_img S img setp)" sublocale set_category_given_img S some_img setp proof - have "∃img. set_category_given_img S img setp" using ex_img by auto thus "set_category_given_img S some_img setp" using someI_ex [of "λimg. set_category_given_img S img setp"] some_img_def by metis qed end text‹We call a set category \emph{replete} if there is an object corresponding to every subset of the universe. › locale replete_set_category = category S + set_category S ‹λA. A ⊆ Collect terminal› for S :: "'s comp" (infixr "⋅" 55) begin abbreviation setp where "setp ≡ λA. A ⊆ Univ" lemma is_set_category: shows "set_category S (λA. A ⊆ Collect terminal)" .. end context set_category begin text‹ The arbitrary choice of @{term img} induces a system of arrows corresponding to inclusions of subsets. › definition incl :: "'s ⇒ bool" where "incl f = (arr f ∧ set (dom f) ⊆ set (cod f) ∧ f = mkArr (set (dom f)) (set (cod f)) (λx. x))" lemma Fun_incl: assumes "incl f" shows "Fun f = (λx ∈ set (dom f). x)" using assms incl_def by (metis Fun_mkArr) lemma ex_incl_iff_subset: assumes "ide a" and "ide b" shows "(∃f. «f : a → b» ∧ incl f) ⟷ set a ⊆ set b" proof show "∃f. «f : a → b» ∧ incl f ⟹ set a ⊆ set b" using incl_def by auto show "set a ⊆ set b ⟹ ∃f. «f : a → b» ∧ incl f" proof assume 1: "set a ⊆ set b" show "«mkArr (set a) (set b) (λx. x) : a → b» ∧ incl (mkArr (set a) (set b) (λx. x))" proof show "«mkArr (set a) (set b) (λx. x) : a → b»" by (metis 1 assms image_ident image_subset_iff_funcset mkIde_set mkArr_in_hom setp_set_ide) thus "incl (mkArr (set a) (set b) (λx. x))" using 1 incl_def by force qed qed qed end section "Categoricity" text‹ In this section we show that the ‹set_category› locale completely characterizes the structure of its interpretations as categories, in the sense that for any two interpretations @{term S} and @{term S'}, a @{term setp}-respecting bijection between the universe of @{term S} and the universe of @{term S'} extends to an isomorphism of @{term S} and @{term S'}. › locale two_set_categories_bij_betw_Univ = S: set_category S setp + S': set_category S' setp' for S :: "'s comp" (infixr "⋅" 55) and setp :: "'s set ⇒ bool" and S' :: "'t comp" (infixr "⋅´" 55) and setp' :: "'t set ⇒ bool" and φ :: "'s ⇒ 't" + assumes bij_φ: "bij_betw φ S.Univ S'.Univ" and φ_respects_setp: "A ⊆ S.Univ ⟹ setp' (φ ` A) ⟷ setp A" begin notation S.in_hom ("«_ : _ → _»") notation S'.in_hom ("«_ : _ →'' _»") abbreviation ψ where "ψ ≡ inv_into S.Univ φ" lemma ψ_φ: assumes "t ∈ S.Univ" shows "ψ (φ t) = t" using assms bij_φ bij_betw_inv_into_left by metis lemma φ_ψ: assumes "t' ∈ S'.Univ" shows "φ (ψ t') = t'" using assms bij_φ bij_betw_inv_into_right by metis lemma ψ_img_φ_img: assumes "A ⊆ S.Univ" shows "ψ ` φ ` A = A" using assms bij_φ by (simp add: bij_betw_def) lemma φ_img_ψ_img: assumes "A' ⊆ S'.Univ" shows "φ ` ψ ` A' = A'" using assms bij_φ by (simp add: bij_betw_def image_inv_into_cancel) text‹ We define the object map @{term Φo} of a functor from @{term[source=true] S} to @{term[source=true] S'}. › definition Φo where "Φo = (λa ∈ Collect S.ide. S'.mkIde (φ ` S.set a))" lemma set_Φo: assumes "S.ide a" shows "S'.set (Φo a) = φ ` S.set a" by (simp add: S.setp_imp_subset_Univ Φo_def φ_respects_setp assms) lemma Φo_preserves_ide: assumes "S.ide a" shows "S'.ide (Φo a)" using assms S'.ide_mkIde bij_φ bij_betw_def image_mono restrict_apply' S.setp_set' φ_respects_setp S.setp_imp_subset_Univ unfolding Φo_def by simp text‹ The map @{term Φa} assigns to each arrow @{term f} of @{term[source=true] S} the function on the universe of @{term[source=true] S'} that is the same as the function induced by @{term f} on the universe of @{term[source=true] S}, up to the bijection @{term φ} between the two universes. › definition Φa where "Φa = (λf. λx' ∈ φ ` S.set (S.dom f). φ (S.Fun f (ψ x')))" lemma Φa_mapsto: assumes "S.arr f" shows "Φa f ∈ S'.set (Φo (S.dom f)) → S'.set (Φo (S.cod f))" proof - have "Φa f ∈ φ ` S.set (S.dom f) → φ ` S.set (S.cod f)" proof fix x assume x: "x ∈ φ ` S.set (S.dom f)" have "ψ x ∈ S.set (S.dom f)" using assms x ψ_img_φ_img [of "S.set (S.dom f)"] S.setp_imp_subset_Univ by auto hence "S.Fun f (ψ x) ∈ S.set (S.cod f)" using assms S.Fun_mapsto by auto hence "φ (S.Fun f (ψ x)) ∈ φ ` S.set (S.cod f)" by simp thus "Φa f x ∈ φ ` S.set (S.cod f)" using x Φa_def by auto qed thus ?thesis using assms set_Φo Φo_preserves_ide by auto qed text‹ The map @{term Φa} takes composition of arrows to extensional composition of functions. › lemma Φa_comp: assumes gf: "S.seq g f" shows "Φa (g ⋅ f) = restrict (Φa g o Φa f) (S'.set (Φo (S.dom f)))" proof - have "Φa (g ⋅ f) = (λx' ∈ φ ` S.set (S.dom f). φ (S.Fun (S g f) (ψ x')))" using gf Φa_def by auto also have "... = (λx' ∈ φ ` S.set (S.dom f). φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')))" using gf set_Φo S.Fun_comp by simp also have "... = restrict (Φa g o Φa f) (S'.set (Φo (S.dom f)))" proof - have "⋀x'. x' ∈ φ ` S.set (S.dom f) ⟹ φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')) = Φa g (Φa f x')" proof - fix x' assume X': "x' ∈ φ ` S.set (S.dom f)" hence 1: "ψ x' ∈ S.set (S.dom f)" using gf ψ_img_φ_img S.setp_imp_subset_Univ S.ide_dom S.setp_set_ide by blast hence "φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')) = φ (S.Fun g (S.Fun f (ψ x')))" using restrict_apply by auto also have "... = φ (S.Fun g (ψ (φ (S.Fun f (ψ x')))))" proof - have "S.Fun f (ψ x') ∈ S.set (S.cod f)" using gf 1 S.Fun_mapsto by fast hence "ψ (φ (S.Fun f (ψ x'))) = S.Fun f (ψ x')" using assms bij_φ S.setp_imp_subset_Univ bij_betw_def inv_into_f_f subsetCE S.ide_cod S.setp_set_ide by (metis S.seqE) thus ?thesis by auto qed also have "... = Φa g (Φa f x')" proof - have "Φa f x' ∈ φ ` S.set (S.cod f)" using gf S.ide_dom S.ide_cod X' Φa_mapsto [of f] set_Φo [of "S.dom f"] set_Φo [of "S.cod f"] by blast thus ?thesis using gf X' Φa_def by auto qed finally show "φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')) = Φa g (Φa f x')" by auto qed thus ?thesis using assms set_Φo by fastforce qed finally show ?thesis by auto qed text‹ Finally, we use @{term Φo} and @{term Φa} to define a functor @{term Φ}. › definition Φ where "Φ f = (if S.arr f then S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f) else S'.null)" lemma Φ_in_hom: assumes "S.arr f" shows "Φ f ∈ S'.hom (Φo (S.dom f)) (Φo (S.cod f))" proof - have "«Φ f : S'.dom (Φ f) →' S'.cod (Φ f)»" using assms Φ_def Φa_mapsto Φo_preserves_ide by (intro S'.in_homI) auto thus ?thesis using assms Φ_def Φa_mapsto Φo_preserves_ide by auto qed lemma Φ_ide [simp]: assumes "S.ide a" shows "Φ a = Φo a" proof - have "Φ a = S'.mkArr (S'.set (Φo a)) (S'.set (Φo a)) (λx'. x')" proof - have "«Φ a : Φo a →' Φo a»" using assms Φ_in_hom S.ide_in_hom by fastforce moreover have "Φa a = restrict (λx'. x') (S'.set (Φo a))" proof - have "Φa a = (λx' ∈ φ ` S.set a. φ (S.Fun a (ψ x')))" using assms Φa_def restrict_apply by auto also have "... = (λx' ∈ S'.set (Φo a). φ (ψ x'))" proof - have "S.Fun a = (λx ∈ S.set a. x)" using assms S.Fun_ide by auto moreover have "⋀x'. x' ∈ φ ` S.set a ⟹ ψ x' ∈ S.set a" using assms bij_φ S.setp_imp_subset_Univ image_iff S.setp_set_ide by (metis ψ_img_φ_img) ultimately show ?thesis using assms set_Φo by auto qed also have "... = restrict (λx'. x') (S'.set (Φo a))" using assms S'.setp_imp_subset_Univ S'.setp_set_ide Φo_preserves_ide φ_ψ by (meson restr_eqI subsetCE) ultimately show ?thesis by auto qed ultimately show ?thesis using assms Φ_def Φo_preserves_ide S'.mkArr_restrict_eq' by (metis S'.arrI S.ide_char) qed thus ?thesis using assms S'.mkIde_as_mkArr Φo_preserves_ide Φ_in_hom S'.mkIde_set by simp qed lemma set_dom_Φ: assumes "S.arr f" shows "S'.set (S'.dom (Φ f)) = φ ` (S.set (S.dom f))" using assms S.ide_dom Φ_in_hom Φ_ide set_Φo by fastforce lemma Φ_comp: assumes "S.seq g f" shows "Φ (g ⋅ f) = Φ g ⋅´ Φ f" proof - have "Φ (g ⋅ f) = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g))) (Φa (S g f))" using Φ_def assms by auto also have "... = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g))) (restrict (Φa g o Φa f) (S'.set (Φo (S.dom f))))" using assms Φa_comp set_Φo by force also have "... = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g))) (Φa g o Φa f)" by (metis S'.mkArr_restrict_eq' Φ_in_hom assms calculation S'.in_homE mem_Collect_eq) also have "... = S' (S'.mkArr (S'.set (Φo (S.dom g))) (S'.set (Φo (S.cod g))) (Φa g)) (S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f))" proof - have "S'.arr (S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f))" using assms Φa_mapsto set_Φo S.ide_dom S.ide_cod Φo_preserves_ide S'.arr_mkArr S'.setp_imp_subset_Univ S'.setp_set_ide S.seqE by metis moreover have "S'.arr (S'.mkArr (S'.set (Φo (S.dom g))) (S'.set (Φo (S.cod g))) (Φa g))" using assms Φa_mapsto set_Φo S.ide_dom S.ide_cod Φo_preserves_ide S'.arr_mkArr S'.setp_imp_subset_Univ S'.setp_set_ide S.seqE by metis ultimately show ?thesis using assms S'.comp_mkArr by auto qed also have "... = Φ g ⋅´ Φ f" using assms Φ_def by force finally show ?thesis by fast qed interpretation Φ: "functor" S S' Φ apply unfold_locales using Φ_def apply simp using Φ_in_hom Φ_comp by auto lemma Φ_is_functor: shows "functor S S' Φ" .. lemma Fun_Φ: assumes "S.arr f" and "x ∈ S.set (S.dom f)" shows "S'.Fun (Φ f) (φ x) = Φa f (φ x)" using assms Φ_def Φ.preserves_arr set_Φo by auto lemma Φ_acts_elementwise: assumes "S.ide a" shows "S'.set (Φ a) = Φ ` S.set a" proof have 0: "S'.set (Φ a) = φ ` S.set a" using assms Φ_ide set_Φo by simp have 1: "⋀x. x ∈ S.set a ⟹ Φ x = φ x" proof - fix x assume x: "x ∈ S.set a" have 1: "S.terminal x" using assms x S.setp_imp_subset_Univ S.setp_set_ide by blast hence 2: "S'.terminal (φ x)" by (metis CollectD CollectI bij_φ bij_betw_def image_iff) have "Φ x = Φo x" using assms x 1 Φ_ide S.terminal_def by auto also have "... = φ x" proof - have "Φo x = S'.mkIde (φ ` S.set x)" using assms 1 x Φo_def S.terminal_def by auto moreover have "S'.mkIde (φ ` S.set x) = φ x" using assms x 1 2 S.terminal_char2 S'.terminal_char2 S'.mkIde_set bij_φ by (metis (no_types, lifting) empty_is_image image_insert) ultimately show ?thesis by auto qed finally show "Φ x = φ x" by auto qed show "S'.set (Φ a) ⊆ Φ ` S.set a" using 0 1 by force show "Φ ` S.set a ⊆ S'.set (Φ a)" using 0 1 by force qed lemma Φ_preserves_incl: assumes "S.incl m" shows "S'.incl (Φ m)" proof - have 1: "S.arr m ∧ S.set (S.dom m) ⊆ S.set (S.cod m) ∧ m = S.mkArr (S.set (S.dom m)) (S.set (S.cod m)) (λx. x)" using assms S.incl_def by blast have "S'.arr (Φ m)" using 1 by auto moreover have 2: "S'.set (S'.dom (Φ m)) ⊆ S'.set (S'.cod (Φ m))" using 1 Φ.preserves_dom Φ.preserves_cod Φ_acts_elementwise by auto moreover have "Φ m = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (λx'. x')" proof - have "Φ m = S'.mkArr (S'.set (Φo (S.dom m))) (S'.set (Φo (S.cod m))) (Φa m)" using 1 Φ_def by simp also have "... = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (Φa m)" using 1 Φ_ide by auto finally have 3: "Φ m = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (Φa m)" by auto also have "... = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (λx'. x')" proof - have 4: "S.Fun m = restrict (λx. x) (S.set (S.dom m))" using assms S.incl_def by (metis (full_types) S.Fun_mkArr) hence "Φa m = restrict (λx'. x') (φ ` (S.set (S.dom m)))" proof - have 5: "⋀x'. x' ∈ φ ` S.set (S.dom m) ⟹ φ (ψ x') = x'" by (meson 1 S.ide_dom S.setp_imp_subset_Univ S.setp_set' f_inv_into_f image_mono subset_eq) have "Φa m = restrict (λx'. φ (S.Fun m (ψ x'))) (φ ` S.set (S.dom m))" using Φa_def by simp also have "... = restrict (λx'. x') (φ ` S.set (S.dom m))" proof - have "⋀x. x ∈ φ ` (S.set (S.dom m)) ⟹ φ (S.Fun m (ψ x)) = x" proof - fix x assume x: "x ∈ φ ` (S.set (S.dom m))" hence "ψ x ∈ S.set (S.dom m)" using 1 S.ide_dom S.setp_imp_subset_Univ S.setp_set_ide ψ_img_φ_img image_eqI by metis thus "φ (S.Fun m (ψ x)) = x" using 1 4 5 x by simp qed thus ?thesis by auto qed finally show ?thesis by auto qed hence "Φa m = restrict (λx'. x') (S'.set (S'.dom (Φ m)))" using 1 set_dom_Φ by auto thus ?thesis using 2 3 ‹S'.arr (Φ m)› S'.mkArr_restrict_eq S'.ide_cod S'.ide_dom S'.incl_def by (metis S'.arr_mkArr image_restrict_eq image_subset_iff_funcset) qed finally show ?thesis by auto qed ultimately show ?thesis using S'.incl_def by blast qed lemma ψ_respects_sets: assumes "A' ⊆ S'.Univ" shows "setp (ψ ` A') ⟷ setp' A'" using assms φ_respects_setp φ_img_ψ_img bij_φ by (metis ψ_img_φ_img bij_betw_def image_mono order_refl) text‹ Interchange the role of @{term φ} and @{term ψ} to obtain a functor ‹Ψ› from @{term[source=true] S'} to @{term[source=true] S}. › interpretation INV: two_set_categories_bij_betw_Univ S' setp' S setp ψ using ψ_respects_sets bij_φ bij_betw_inv_into by unfold_locales auto abbreviation Ψo where "Ψo ≡ INV.Φo" abbreviation Ψa where "Ψa ≡ INV.Φa" abbreviation Ψ where "Ψ ≡ INV.Φ" interpretation Ψ: "functor" S' S Ψ using INV.Φ_is_functor by auto text‹ The functors @{term Φ} and @{term Ψ} are inverses. › lemma Fun_Ψ: assumes "S'.arr f'" and "x' ∈ S'.set (S'.dom f')" shows "S.Fun (Ψ f') (ψ x') = Ψa f' (ψ x')" using assms INV.Fun_Φ by blast lemma Ψo_Φo: assumes "S.ide a" shows "Ψo (Φo a) = a" using assms Φo_def INV.Φo_def ψ_img_φ_img Φo_preserves_ide set_Φo S.mkIde_set by (simp add: S.setp_imp_subset_Univ) lemma ΦΨ: assumes "S.arr f" shows "Ψ (Φ f) = f" proof (intro S.arr_eqI⇩_{S}⇩_{C}) show par: "S.par (Ψ (Φ f)) f" using assms Φo_preserves_ide Ψo_Φo by auto show "S.Fun (Ψ (Φ f)) = S.Fun f" proof - have "S.arr (Ψ (Φ f))" using assms by auto moreover have "Ψ (Φ f) = S.mkArr (S.set (S.dom f)) (S.set (S.cod f)) (Ψa (Φ f))" using assms INV.Φ_def Φ_in_hom Ψo_Φo by auto moreover have "Ψa (Φ f) = (λx ∈ S.set (S.dom f). ψ (S'.Fun (Φ f) (φ x)))" proof - have "Ψa (Φ f) = (λx ∈ ψ ` S'.set (S'.dom (Φ f)). ψ (S'.Fun (Φ f) (φ x)))" proof - have "⋀x. x ∈ ψ ` S'.set (S'.dom (Φ f)) ⟹ INV.ψ x = φ x" using assms S.ide_dom S.setp_imp_subset_Univ Ψ.preserves_reflects_arr par bij_φ inv_into_inv_into_eq subsetCE INV.set_dom_Φ by (metis (no_types) S.setp_set') thus ?thesis using INV.Φa_def by auto qed moreover have "ψ ` S'.set (S'.dom (Φ f)) = S.set (S.dom f)" using assms by (metis par Ψ.preserves_reflects_arr INV.set_dom_Φ) ultimately show ?thesis by auto qed ultimately have 1: "S.Fun (Ψ (Φ f)) = (λx ∈ S.set (S.dom f). ψ (S'.Fun (Φ f) (φ x)))" using S'.Fun_mkArr by simp show ?thesis proof fix x have "x ∉ S.set (S.dom f) ⟹ S.Fun (Ψ (Φ f)) x = S.Fun f x" using 1 assms extensional_def S.Fun_mapsto S.Fun_def by auto moreover have "x ∈ S.set (S.dom f) ⟹ S.Fun (Ψ (Φ f)) x = S.Fun f x" proof - assume x: "x ∈ S.set (S.dom f)" have "S.Fun (Ψ (Φ f)) x = ψ (φ (S.Fun f (ψ (φ x))))" using assms x 1 Fun_Φ bij_φ Φa_def by auto also have "... = S.Fun f x" proof - have 2: "⋀x. x ∈ S.Univ ⟹ ψ (φ x) = x" using bij_φ bij_betw_inv_into_left by fast have "S.Fun f (ψ (φ x)) = S.Fun f x" using assms x 2 S.ide_dom S.setp_imp_subset_Univ by (metis S.setp_set' subsetD) moreover have "S.Fun f x ∈ S.Univ" using x assms S.Fun_mapsto S.setp_imp_subset_Univ S.setp_set' S.ide_cod by blast ultimately show ?thesis using 2 by auto qed finally show ?thesis by auto qed ultimately show "S.Fun (Ψ (Φ f)) x = S.Fun f x" by auto qed qed qed lemma Φo_Ψo: assumes "S'.ide a'" shows "Φo (Ψo a') = a'" using assms Φo_def INV.Φo_def φ_img_ψ_img INV.Φo_preserves_ide ψ_φ INV.set_Φo S'.mkIde_set S'.setp_imp_subset_Univ by force lemma ΨΦ: assumes "S'.arr f'" shows "Φ (Ψ f') = f'" proof (intro S'.arr_eqI⇩_{S}⇩_{C}) show par: "S'.par (Φ (Ψ f')) f'" using assms Φ.preserves_ide Ψ.preserves_ide Φ_ide INV.Φ_ide Φo_Ψo by auto show "S'.Fun (Φ (Ψ f')) = S'.Fun f'" proof - have "S'.arr (Φ (Ψ f'))" using assms by blast moreover have "Φ (Ψ f') = S'.mkArr (S'.set (S'.dom f')) (S'.set (S'.cod f')) (Φa (Ψ f'))" using assms Φ_def INV.Φ_in_hom Φo_Ψo by simp moreover have "Φa (Ψ f') = (λx' ∈ S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))" unfolding Φa_def using assms par Ψ.preserves_arr set_dom_Φ by metis ultimately have 1: "S'.Fun (Φ (Ψ f')) = (λx' ∈ S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))" using S'.Fun_mkArr by simp show ?thesis proof fix x' have "x' ∉ S'.set (S'.dom f') ⟹ S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'" using 1 assms S'.Fun_mapsto extensional_def by (simp add: S'.Fun_def) moreover have "x' ∈ S'.set (S'.dom f') ⟹ S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'" proof - assume x': "x' ∈ S'.set (S'.dom f')" have "S'.Fun (Φ (Ψ f')) x' = φ (S.Fun (Ψ f') (ψ x'))" using x' 1 by auto also have "... = φ (Ψa f' (ψ x'))" using Fun_Ψ x' assms S'.setp_imp_subset_Univ bij_φ by metis also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))" proof - have "φ (Ψa f' (ψ x')) = φ (ψ (S'.Fun f' x'))" proof - have "x' ∈ S'.Univ" by (meson S'.ide_dom S'.setp_imp_subset_Univ S'.setp_set_ide assms subsetCE x') thus ?thesis by (simp add: INV.Φa_def INV.ψ_φ x') qed also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))" using assms x' φ_ψ S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom by (metis subsetCE) finally show ?thesis by auto qed also have "... = S'.Fun f' x'" proof - have 2: "⋀x'. x' ∈ S'.Univ ⟹ φ (ψ x') = x'" using bij_φ bij_betw_inv_into_right by fast have "S'.Fun f' (φ (ψ x')) = S'.Fun f' x'" using assms x' 2 S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom by (metis subsetCE) moreover have "S'.Fun f' x' ∈ S'.Univ" using x' assms S'.Fun_mapsto S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_cod by blast ultimately show ?thesis using 2 by auto qed finally show ?thesis by auto qed ultimately show "S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'" by auto qed qed qed lemma inverse_functors_Φ_Ψ: shows "inverse_functors S S' Ψ Φ" proof - interpret ΦΨ: composite_functor S S' S Φ Ψ .. have inv: "Ψ o Φ = S.map" using ΦΨ S.map_def ΦΨ.is_extensional by auto interpret ΨΦ: composite_functor S' S S' Ψ Φ .. have inv': "Φ o Ψ = S'.map" using ΨΦ S'.map_def ΨΦ.is_extensional by auto show ?thesis using inv inv' by (unfold_locales, auto) qed lemma are_isomorphic: shows "∃Φ. invertible_functor S S' Φ ∧ (∀m. S.incl m ⟶ S'.incl (Φ m))" proof - interpret inverse_functors S S' Ψ Φ using inverse_functors_Φ_Ψ by auto have 1: "inverse_functors S S' Ψ Φ" .. interpret invertible_functor S S' Φ apply unfold_locales using 1 by auto have "invertible_functor S S' Φ" .. thus ?thesis using Φ_preserves_incl by auto qed end text‹ The main result: @{locale set_category} is categorical, in the following (logical) sense: If ‹S› and ‹S'› are two "set categories", and if the sets of terminal objects of ‹S› and ‹S'› are in correspondence via a @{term setp}-preserving bijection, then ‹S› and ‹S'› are isomorphic as categories, via a functor that preserves inclusion maps, hence also the inclusion relation between sets. › theorem set_category_is_categorical: assumes "set_category S setp" and "set_category S' setp'" and "bij_betw φ (set_category_data.Univ S) (set_category_data.Univ S')" and "⋀A. A ⊆ set_category_data.Univ S ⟹ setp' (φ ` A) ⟷ setp A" shows "∃Φ. invertible_functor S S' Φ ∧ (∀m. set_category.incl S setp m ⟶ set_category.incl S' setp' (Φ m))" proof - interpret S: set_category S setp using assms(1) by auto interpret S': set_category S' setp' using assms(2) by auto interpret two_set_categories_bij_betw_Univ S setp S' setp' φ apply (unfold_locales) using assms(3-4) by auto show ?thesis using are_isomorphic by auto qed section "Further Properties of Set Categories" text‹ In this section we further develop the consequences of the ‹set_category› axioms, and establish characterizations of a number of standard category-theoretic notions for a ‹set_category›. › context set_category begin abbreviation Dom where "Dom f ≡ set (dom f)" abbreviation Cod where "Cod f ≡ set (cod f)" subsection "Initial Object" text‹ The object corresponding to the empty set is an initial object. › definition empty where "empty = mkIde {}" lemma initial_empty: shows "initial empty" proof show 0: "ide empty" using empty_def by (simp add: setp_empty) show "⋀b. ide b ⟹ ∃!f. «f : empty → b»" proof - fix b assume b: "ide b" show "∃!f. «f : empty → b»" proof show 1: "«mkArr {} (set b) (λx. x) : empty → b»" using 0 b empty_def mkArr_in_hom mkIde_set setp_imp_subset_Univ arr_mkIde by (metis Pi_I empty_iff ide_def mkIde_def) show "⋀f. «f : empty → b» ⟹ f = mkArr {} (set b) (λx. x)" by (metis "1" arr_mkArr empty_iff in_homE empty_def mkArr_Fun mkArr_eqI set_mkIde) qed qed qed subsection "Identity Arrows" text‹ Identity arrows correspond to restrictions of the identity function. › lemma ide_char⇩_{S}⇩_{C}: assumes "arr f" shows "ide f ⟷ Dom f = Cod f ∧ Fun f = (λx ∈ Dom f. x)" using assms mkIde_as_mkArr mkArr_Fun Fun_ide in_homE ide_cod mkArr_Fun mkIde_set by (metis ide_char) lemma ideI: assumes "arr f" and "Dom f = Cod f" and "⋀x. x ∈ Dom f ⟹ Fun f x = x" shows "ide f" proof - have "Fun f = (λx ∈ Dom f. x)" using assms Fun_def by auto thus ?thesis using assms ide_char⇩_{S}⇩_{C}by blast qed subsection "Inclusions" lemma ide_implies_incl: assumes "ide a" shows "incl a" by (simp add: assms incl_def) definition incl_in :: "'s ⇒ 's ⇒ bool" where "incl_in a b = (ide a ∧ ide b ∧ set a ⊆ set b)" abbreviation incl_of where "incl_of a b ≡ mkArr (set a) (set b) (λx. x)" lemma elem_set_implies_set_eq_singleton: assumes "a ∈ set b" shows "set a = {a}" proof - have "ide b" using assms set_def by auto thus ?thesis using assms setp_imp_subset_Univ terminal_char2 by (metis setp_set' insert_subset mem_Collect_eq mk_disjoint_insert) qed lemma elem_set_implies_incl_in: assumes "a ∈ set b" shows "incl_in a b" proof - have b: "ide b" using assms set_def by auto hence "setp (set b)" by simp hence "a ∈ Univ ∧ set a ⊆ set b" using setp_imp_subset_Univ assms elem_set_implies_set_eq_singleton by auto hence "ide a ∧ set a ⊆ set b" using b terminal_char1 by simp thus ?thesis using b incl_in_def by simp qed lemma incl_incl_of [simp]: assumes "incl_in a b" shows "incl (incl_of a b)" and "«incl_of a b : a → b»" proof - show "«incl_of a b : a → b»" using assms incl_in_def mkArr_in_hom by (metis image_ident image_subset_iff_funcset mkIde_set setp_set_ide) thus "incl (incl_of a b)" using assms incl_def incl_in_def by fastforce qed text‹ There is at most one inclusion between any pair of objects. › lemma incls_coherent: assumes "par f f'" and "incl f" and "incl f'" shows "f = f'" using assms incl_def fun_complete by auto text‹ The set of inclusions is closed under composition. › lemma incl_comp [simp]: assumes "incl f" and "incl g" and "cod f = dom g" shows "incl (g ⋅ f)" proof - have 1: "seq g f" using assms incl_def by auto moreover have 2: "Dom (g ⋅ f) ⊆ Cod (g ⋅ f)" using assms 1 incl_def by auto moreover have "g ⋅ f = mkArr (Dom f) (Cod g) (restrict (λx. x) (Dom f))" proof (intro arr_eqI⇩_{S}⇩_{C}) have 3: "arr (mkArr (Dom f) (Cod g) (λx∈Dom f. x))" by (metis 1 2 cod_comp dom_comp ide_cod ide_dom incl_def incl_in_def incl_incl_of(1) mkArr_restrict_eq) show 4: "par (g ⋅ f) (mkArr (Dom f) (Cod g) (λx∈Dom f. x))" using assms 1 3 mkIde_set by auto show "Fun (g ⋅ f) = Fun (mkArr (Dom f) (Cod g) (λx∈Dom f. x))" using assms 3 4 Fun_comp Fun_mkArr by (metis comp_cod_arr dom_cod ide_cod ide_implies_incl incl_def mkArr_restrict_eq') qed ultimately show ?thesis using incl_def by force qed subsection "Image Factorization" text‹ The image of an arrow is the object that corresponds to the set-theoretic image of the domain set under the function induced by the arrow. › abbreviation Img where "Img f ≡ Fun f ` Dom f" definition img where "img f = mkIde (Img f)" lemma ide_img [simp]: assumes "arr f" shows "ide (img f)" proof - have "Fun f ` Dom f ⊆ Cod f" using assms Fun_mapsto by blast moreover have "setp (Cod f)" using assms by simp ultimately show ?thesis using img_def setp_respects_subset by auto qed lemma set_img [simp]: assumes "arr f" shows "set (img f) = Img f" proof - have 1: "Img f ⊆ Cod f ∧ setp (set (cod f))" using assms Fun_mapsto by auto hence "Fun f ` set (dom f) ⊆ Univ" using setp_imp_subset_Univ by blast thus ?thesis using assms 1 img_def set_mkIde setp_respects_subset by auto qed lemma img_point_in_Univ: assumes "«x : unity → a»" shows "img x ∈ Univ" proof - have "set (img x) = {Fun x unity}" using assms terminal_char2 terminal_unity⇩_{S}⇩_{C}by auto thus "img x ∈ Univ" using assms terminal_char1 by auto qed lemma incl_in_img_cod: assumes "arr f" shows "incl_in (img f) (cod f)" proof (unfold img_def) have 1: "Img f ⊆ Cod f ∧ setp (Cod f)" using assms Fun_mapsto by auto hence 2: "ide (mkIde (Img f))" using setp_respects_subset by auto moreover have "ide (cod f)" using assms by auto moreover have "set (mkIde (Img f)) ⊆ Cod f" using 1 2 using setp_respects_subset by force ultimately show "incl_in (mkIde (Img f)) (cod f)" using assms incl_in_def ide_cod by blast qed lemma img_point_elem_set: assumes "«x : unity → a»" shows "img x ∈ set a" by (metis assms img_point_in_Univ in_homE incl_in_img_cod insert_subset mem_Collect_eq incl_in_def terminal_char2) text‹ The corestriction of an arrow @{term f} is the arrow @{term "corestr f ∈ hom (dom f) (img f)"} that induces the same function on the universe as @{term f}. › definition corestr where "corestr f = mkArr (Dom f) (Img f) (Fun f)" lemma corestr_in_hom: assumes "arr f" shows "«corestr f : dom f → img f»" by (metis assms corestr_def equalityD2 ide_dom ide_img image_subset_iff_funcset mkIde_set set_img mkArr_in_hom setp_set_ide) text‹ Every arrow factors as a corestriction followed by an inclusion. › lemma img_fact: assumes "arr f" shows "S (incl_of (img f) (cod f)) (corestr f) = f" proof (intro arr_eqI⇩_{S}⇩_{C}) have 1: "«corestr f : dom f → img f»" using assms corestr_in_hom by blast moreover have 2: "«incl_of (img f) (cod f) : img f → cod f»" using assms incl_in_img_cod incl_incl_of by fast ultimately show P: "par (incl_of (img f) (cod f) ⋅ corestr f) f" using assms in_homE by blast show "Fun (incl_of (img f) (cod f) ⋅ corestr f) = Fun f" by (metis (no_types, lifting) 1 2 Fun_comp Fun_ide Fun_mkArr P comp_cod_arr corestr_def ide_img in_homE mkArr_Fun) qed lemma Fun_corestr: assumes "arr f" shows "Fun (corestr f) = Fun f" by (metis Fun_mkArr arrI assms corestr_def corestr_in_hom mkArr_Fun) subsection "Points and Terminal Objects" text‹ To each element @{term t} of @{term "set a"} is associated a point @{term "mkPoint a t ∈ hom unity a"}. The function induced by such a point is the constant-@{term t} function on the set @{term "{unity}"}. › definition mkPoint where "mkPoint a t ≡ mkArr {unity} (set a) (λ_. t)" lemma mkPoint_in_hom: assumes "ide a" and "t ∈ set a" shows "«mkPoint a t : unity → a»" using assms mkArr_in_hom by (metis Pi_I mkIde_set setp_set_ide terminal_char2 terminal_unity⇩_{S}⇩_{C}mkPoint_def) lemma Fun_mkPoint: assumes "ide a" and "t ∈ set a" shows "Fun (mkPoint a t) = (λ_ ∈ {unity}. t)" using assms mkPoint_def terminal_unity⇩_{S}⇩_{C}mkPoint_in_hom by fastforce text‹ For each object @{term a} the function @{term "mkPoint a"} has as its inverse the restriction of the function @{term img} to @{term "hom unity a"} › lemma mkPoint_img: shows "img ∈ hom unity a → set a" and "⋀x. «x : unity → a» ⟹ mkPoint a (img x) = x" proof - show "img ∈ hom unity a → set a" using img_point_elem_set by simp show "⋀x. «x : unity → a» ⟹ mkPoint a (img x) = x" proof - fix x assume x: "«x : unity → a»" show "mkPoint a (img x) = x" proof (intro arr_eqI⇩_{S}⇩_{C}) have 0: "img x ∈ set a" using x img_point_elem_set by metis hence 1: "mkPoint a (img x) ∈ hom unity a" using x mkPoint_in_hom by force thus 2: "par (mkPoint a (img x)) x" using x by fastforce have "Fun (mkPoint a (img x)) = (λ_ ∈ {unity}. img x)" using 1 mkPoint_def by auto also have "... = Fun x" by (metis 0 Fun_corestr calculation elem_set_implies_set_eq_singleton ide_cod ide_unity in_homE mem_Collect_eq Fun_mkPoint corestr_in_hom img_point_in_Univ mkPoint_in_hom singletonI terminalE x) finally show "Fun (mkPoint a (img x)) = Fun x" by auto qed qed qed lemma img_mkPoint: assumes "ide a" shows "mkPoint a ∈ set a → hom unity a" and "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t" proof - show "mkPoint a ∈ set a → hom unity a" using assms(1) mkPoint_in_hom by simp show "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t" proof - fix t assume t: "t ∈ set a" show "img (mkPoint a t) = t" proof - have 1: "arr (mkPoint a t)" using assms t mkPoint_in_hom by auto have "Fun (mkPoint a t) ` {unity} = {t}" using 1 mkPoint_def by simp thus ?thesis by (metis in_homE img_def mkIde_set mkPoint_in_hom elem_set_implies_incl_in elem_set_implies_set_eq_singleton incl_in_def t terminal_char2 terminal_unity⇩_{S}⇩_{C}) qed qed qed text‹ For each object @{term a} the elements of @{term "hom unity a"} are therefore in bijective correspondence with @{term "set a"}. › lemma bij_betw_points_and_set: assumes "ide a" shows "bij_betw img (hom unity a) (set a)" proof (intro bij_betwI) show "img ∈ hom unity a → set a" using assms mkPoint_img by auto show "mkPoint a ∈ set a → hom unity a" using assms img_mkPoint by auto show "⋀x. x ∈ hom unity a ⟹ mkPoint a (img x) = x" using assms mkPoint_img by auto show "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t" using assms img_mkPoint by auto qed lemma setp_img_points: assumes "ide a" shows "setp (img ` hom unity a)" using assms by (metis image_subset_iff_funcset mkPoint_img(1) setp_respects_subset setp_set_ide) text‹ The function on the universe induced by an arrow @{term f} agrees, under the bijection between @{term "hom unity (dom f)"} and @{term "Dom f"}, with the action of @{term f} by composition on @{term "hom unity (dom f)"}. › lemma Fun_point: assumes "«x : unity → a»" shows "Fun x = (λ_ ∈ {unity}. img x)" using assms mkPoint_img img_mkPoint Fun_mkPoint [of a "img x"] img_point_elem_set by auto lemma comp_arr_mkPoint: assumes "arr f" and "t ∈ Dom f" shows "f ⋅ mkPoint (dom f) t = mkPoint (cod f) (Fun f t)" proof (intro arr_eqI⇩_{S}⇩_{C}) have 0: "seq f (mkPoint (dom f) t)" using assms mkPoint_in_hom [of "dom f" t] by auto have 1: "«f ⋅ mkPoint (dom f) t : unity → cod f»" using assms mkPoint_in_hom [of "dom f" t] by auto show "par (f ⋅ mkPoint (dom f) t) (mkPoint (cod f) (Fun f t))" proof - have "«mkPoint (cod f) (Fun f t) : unity → cod f»" using assms Fun_mapsto mkPoint_in_hom [of "cod f" "Fun f t"] by auto thus ?thesis using 1 by fastforce qed show "Fun (f ⋅ mkPoint (dom f) t) = Fun (mkPoint (cod f) (Fun f t))" proof - have "Fun (f ⋅ mkPoint (dom f) t) = restrict (Fun f o Fun (mkPoint (dom f) t)) {unity}" using assms 0 1 Fun_comp terminal_char2 terminal_unity⇩_{S}⇩_{C}by auto also have "... = (λ_ ∈ {unity}. Fun f t)" using assms Fun_mkPoint by auto also have "... = Fun (mkPoint (cod f) (Fun f t))" using assms Fun_mkPoint [of "cod f" "Fun f t"] Fun_mapsto by fastforce finally show ?thesis by auto qed qed lemma comp_arr_point⇩_{S}⇩_{S}⇩_{C}: assumes "arr f" and "«x : unity → dom f»" shows "f ⋅ x = mkPoint (cod f) (Fun f (img x))" by (metis assms comp_arr_mkPoint img_point_elem_set mkPoint_img(2)) text‹ This agreement allows us to express @{term "Fun f"} in terms of composition. › lemma Fun_in_terms_of_comp: assumes "arr f" shows "Fun f = restrict (img o S f o mkPoint (dom f)) (Dom f)" proof fix t have "t ∉ Dom f ⟹ Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t" using assms by (simp add: Fun_def) moreover have "t ∈ Dom f ⟹ Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t" proof - assume t: "t ∈ Dom f" have 1: "f ⋅ mkPoint (dom f) t = mkPoint (cod f) (Fun f t)" using assms t comp_arr_mkPoint by simp hence "img (f ⋅ mkPoint (dom f) t) = img (mkPoint (cod f) (Fun f t))" by simp thus ?thesis proof - have "Fun f t ∈ Cod f" using assms t Fun_mapsto by auto thus ?thesis using assms t 1 img_mkPoint by auto qed qed ultimately show "Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t" by auto qed text‹ We therefore obtain a rule for proving parallel arrows equal by showing that they have the same action by composition on points. › (* * TODO: Find out why attempts to use this as the main rule for a proof loop * unless the specific instance is given. *) lemma arr_eqI'⇩_{S}⇩_{C}: assumes "par f f'" and "⋀x. «x : unity → dom f» ⟹ f ⋅ x = f' ⋅ x" shows "f = f'" using assms Fun_in_terms_of_comp mkPoint_in_hom by (intro arr_eqI⇩_{S}⇩_{C}, auto) text‹ An arrow can therefore be specified by giving its action by composition on points. In many situations, this is more natural than specifying it as a function on the universe. › definition mkArr' where "mkArr' a b F = mkArr (set a) (set b) (img o F o mkPoint a)" lemma mkArr'_in_hom: assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b" shows "«mkArr' a b F : a → b»" proof - have "img o F o mkPoint a ∈ set a → set b" using assms(1,3) img_mkPoint(1) mkPoint_img(1) by fastforce thus ?thesis using assms mkArr'_def mkArr_in_hom [of "set a" "set b"] mkIde_set by simp qed lemma comp_point_mkArr': assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b" shows "⋀x. «x : unity → a» ⟹ mkArr' a b F ⋅ x = F x" proof - fix x assume x: "«x : unity → a»" have "Fun (mkArr' a b F) (img x) = img (F x)" unfolding mkArr'_def using assms x Fun_mkArr img_point_elem_set mkPoint_img mkPoint_in_hom by (simp add: Pi_iff) hence "mkArr' a b F ⋅ x = mkPoint b (img (F x))" using assms x mkArr'_in_hom [of a b F] comp_arr_point⇩_{S}⇩_{S}⇩_{C}by auto thus "mkArr' a b F ⋅ x = F x" using assms x mkPoint_img(2) by auto qed text‹ A third characterization of terminal objects is as those objects whose set of points is a singleton. › lemma terminal_char3: assumes "∃!x. «x : unity → a»" shows "terminal a" proof - have a: "ide a" using assms ide_cod mem_Collect_eq by blast hence "bij_betw img (hom unity a) (set a)" using assms bij_betw_points_and_set by auto hence "img ` (hom unity a) = set a" by (simp add: bij_betw_def) moreover have "hom unity a = {THE x. x ∈ hom unity a}" using assms theI' [of "λx. x ∈ hom unity a"] by auto ultimately have "set a = {img (THE x. x ∈ hom unity a)}" by (metis image_empty image_insert) thus ?thesis using a terminal_char1 by simp qed text‹ The following is an alternative formulation of functional completeness, which says that any function on points uniquely determines an arrow. › lemma fun_complete': assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b" shows "∃!f. «f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = F x)" proof have 1: "«mkArr' a b F : a → b»" using assms mkArr'_in_hom by auto moreover have 2: "⋀x. «x : unity → a» ⟹ mkArr' a b F ⋅ x = F x" using assms comp_point_mkArr' by auto ultimately show "«mkArr' a b F : a → b» ∧ (∀x. «x : unity → a» ⟶ mkArr' a b F ⋅ x = F x)" by blast fix f assume f: "«f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = F x)" show "f = mkArr' a b F" using f 1 2 by (intro arr_eqI'⇩_{S}⇩_{C}[of f "mkArr' a b F"], fastforce, auto) qed subsection "The `Determines Same Function' Relation on Arrows" text‹ An important part of understanding the structure of a category of sets and functions is to characterize when it is that two arrows ``determine the same function''. The following result provides one answer to this: two arrows with a common domain determine the same function if and only if they can be rendered equal by composing with a cospan of inclusions. › lemma eq_Fun_iff_incl_joinable: assumes "span f f'" shows "Fun f = Fun f' ⟷ (∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f')" proof assume ff': "Fun f = Fun f'" let ?b = "mkIde (Cod f ∪ Cod f')" let ?m = "incl_of (cod f) ?b" let ?m' = "incl_of (cod f') ?b" have incl_m: "incl ?m" using assms incl_incl_of [of "cod f" ?b] incl_in_def setp_respects_union by simp have incl_m': "incl ?m'" using assms incl_incl_of [of "cod f'" ?b] incl_in_def setp_respects_union by simp have m: "?m = mkArr (Cod f) (Cod f ∪ Cod f') (λx. x)" using setp_respects_union by (simp add: assms) have m': "?m' = mkArr (Cod f') (Cod f ∪ Cod f') (λx. x)" using setp_respects_union by (simp add: assms) have seq: "seq ?m f ∧ seq ?m' f'" using assms m m' using setp_respects_union by simp have "?m ⋅ f = ?m' ⋅ f'" by (metis assms comp_mkArr ff' incl_def incl_m incl_m' mkArr_Fun) hence "incl ?m ∧ incl ?m' ∧ seq ?m f ∧ seq ?m' f' ∧ ?m ⋅ f = ?m' ⋅ f'" using seq ‹incl ?m› ‹incl ?m'› by simp thus "∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f'" by auto next assume ff': "∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f'" show "Fun f = Fun f'" using ff' by (metis Fun_comp Fun_ide comp_cod_arr ide_cod seqE Fun_incl) qed text‹ Another answer to the same question: two arrows with a common domain determine the same function if and only if their corestrictions are equal. › lemma eq_Fun_iff_eq_corestr: assumes "span f f'" shows "Fun f = Fun f' ⟷ corestr f = corestr f'" using assms corestr_def Fun_corestr by metis subsection "Retractions, Sections, and Isomorphisms" text‹ An arrow is a retraction if and only if its image coincides with its codomain. › lemma retraction_if_Img_eq_Cod: assumes "arr g" and "Img g = Cod g" shows "retraction g" and "ide (g ⋅ mkArr (Cod g) (Dom g) (inv_into (Dom g) (Fun g)))" proof - let ?F = "inv_into (Dom g) (Fun g)" let ?f = "mkArr (Cod g) (Dom g) ?F" have f: "arr ?f" by (simp add: assms inv_into_into) show "ide (g ⋅ ?f)" proof - have "g = mkArr (Dom g) (Cod g) (Fun g)" using assms mkArr_Fun by auto hence "g ⋅ ?f = mkArr (Cod g) (Cod g) (Fun g o ?F)" using assms(1)