# Theory SetCategory

(*  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.
›

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

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"

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
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"
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"
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)`