Quelle  SetCategory.thy

(*  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_SC:
    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_SC:
    assumes "par f f'" and "Fun f = Fun f'"
    shows "f = f'"
      using assms comp_arr_point_SC extensional_arr by metis

    lemma terminal_unity_SC:
    shows "terminal unity"
      using unity_def nonempty_Univ by (simp add: someI_ex)

    lemma ide_unity [simp]:
    shows "ide unity"
      using terminal_unity_SC 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_SC 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_SC
          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_SC, 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_SC, 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_SC)
      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_SC 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_SC)
                  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_SC 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_SC)
      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_SC)
      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 ΦΨ.extensionality by auto
    
      interpret ΨΦ: composite_functor S' S S' Ψ Φ ..
      have inv': "Φ o Ψ = S'.map"
        using ΨΦ S'.map_def ΨΦ.extensionality 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_SC:
    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_SC 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_SC)
        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_SC 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_SC)
      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_SC 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_SC 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_SC)
          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_SC)
        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_SC)
      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_SC 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_SSC:
    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'_SC:
    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_SC, 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_SSC 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'_SC [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) f comp_mkArr by metis
        moreover have "mkArr (Cod g) (Cod g) (λy. y) = ..."
        proof (intro mkArr_eqI')
          show "arr (mkArr (Cod g) (Cod g) (λy. y))"
            using assms arr_cod_iff_arr by auto
          show "∧y. y ∈ Cod g ==> y = (Fun g o ?F) y"
            using assms by (simp add: f_inv_into_f)
        qed
        ultimately show ?thesis
          using assms f mkIde_as_mkArr by auto
      qed
      thus "retraction g" by auto
    qed

    lemma retraction_char:
    shows "retraction g ⟷ arr g ∧ Img g = Cod g"
    proof
      assume G: "retraction g"
      show "arr g ∧ Img g = Cod g"
      proof
        show "arr g" using G by blast
        show "Img g = Cod g"
        proof -
          from G obtain f where f: "ide (g ⋅ f)" by blast
          have "Fun g ` Fun f ` Cod g = Cod g"
          proof -
            have "restrict (Fun g o Fun f) (Cod g) = restrict (λx. x) (Cod g)"
              using f Fun_comp Fun_ide ide_compE by metis
            thus ?thesis
              by (metis image_comp image_ident image_restrict_eq)
          qed
          moreover have "Fun f ` Cod g ⊆ Dom g"
            using f Fun_mapsto arr_mkArr mkArr_Fun funcset_image
            by (metis seqE ide_compE ide_compE)
          moreover have "Img g ⊆ Cod g"
            using f Fun_mapsto by blast
          ultimately show ?thesis by blast
        qed
      qed
      next
      assume "arr g ∧ Img g = Cod g"
      thus "retraction g" using retraction_if_Img_eq_Cod by blast
    qed

    text‹
 Every corestriction is a retraction.
 ›

    lemma retraction_corestr:
    assumes "arr f"
    shows "retraction (corestr f)"
      using assms retraction_char Fun_corestr corestr_in_hom in_homE set_img
      by metis

    text‹
 An arrow is a section if and only if it induces an injective function on its
 domain, except in the special case that it has an empty domain set and a
 nonempty codomain set.
 ›

    lemma section_if_inj:
    assumes "arr f" and "inj_on (Fun f) (Dom f)" and "Dom f = {} ⟶ Cod f = {}"
    shows "section f"
    and "ide (mkArr (Cod f) (Dom f)
                    (λy. if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
                         else SOME x. x ∈ Dom f)
                ⋅ f)"
    proof -
      let ?P= "λy. λx. x ∈ Dom f ∧ Fun f x = y"
      let ?G = "λy. if y ∈ Img f then SOME x. ?P y x else SOME x. x ∈ Dom f"
      let ?g = "mkArr (Cod f) (Dom f) ?G"
      have g: "arr ?g"
      proof -
        have 1: "setp (Cod f)" using assms by simp
        have 2: "setp (Dom f)" using assms by simp
        have 3: "?G ∈ Cod f → Dom f"
        proof
          fix y
          assume Y: "y ∈ Cod f"
          show "?G y ∈ Dom f"
          proof (cases "y ∈ Img f")
            assume "y ∈ Img f"
            hence "(∃x. ?P y x) ∧ ?G y = (SOME x. ?P y x)" using Y by auto
            hence "?P y (?G y)" using someI_ex [of "?P y"] by argo
            thus "?G y ∈ Dom f" by auto
            next
            assume "y ∉ Img f"
            hence "(∃x. x ∈ Dom f) ∧ ?G y = (SOME x. x ∈ Dom f)" using assms Y by auto
            thus "?G y ∈ Dom f" using someI_ex [of "λx. x ∈ Dom f"] by argo
          qed
        qed
        show ?thesis using 1 2 3 by simp
      qed
      show "ide (?g ⋅ f)"
      proof -
        have "f = mkArr (Dom f) (Cod f) (Fun f)" using assms mkArr_Fun by auto
        hence "?g ⋅ f = mkArr (Dom f) (Dom f) (?G o Fun f)"
          using assms(1) g comp_mkArr [of "Dom f" "Cod f" "Fun f" "Dom f" ?G] by argo
        moreover have "mkArr (Dom f) (Dom f) (λx. x) = ..."
        proof (intro mkArr_eqI')
          show "arr (mkArr (Dom f) (Dom f) (λx. x))"
            using assms by auto
          show "∧x. x ∈ Dom f ==> x = (?G o Fun f) x"
          proof -
            fix x
            assume x: "x ∈ Dom f"
            have "Fun f x ∈ Img f" using x by blast
            hence *: "(∃x'. ?P (Fun f x) x') ∧ ?G (Fun f x) = (SOME x'. ?P (Fun f x) x')"
              by auto
            then have "?P (Fun f x) (?G (Fun f x))"
              using someI_ex [of "?P (Fun f x)"] by argo
            with * have "x = ?G (Fun f x)"
              using assms x inj_on_def [of "Fun f" "Dom f"] by simp
            thus "x = (?G o Fun f) x" by simp
          qed
        qed
        ultimately show ?thesis
          using assms mkIde_as_mkArr mkIde_set by auto
      qed
      thus "section f" by auto
    qed

    lemma section_char:
    shows "section f ⟷ arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
    proof
      assume f: "section f"
      from f obtain g where g: "ide (g ⋅ f)" using section_def by blast
      show "arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
      proof -
        have "arr f" using f by blast
        moreover have "Dom f = {} ⟶ Cod f = {}"
        proof -
          have "Cod f ≠ {} ⟶ Dom f ≠ {}"
          proof
            assume "Cod f ≠ {}"
            from this obtain y where "y ∈ Cod f" by blast
            hence "Fun g y ∈ Dom f"
              using g Fun_mapsto
              by (metis seqE ide_compE image_eqI retractionI retraction_char)
            thus "Dom f ≠ {}" by blast
          qed
          thus ?thesis by auto
        qed
        moreover have "inj_on (Fun f) (Dom f)"
          by (metis Fun_comp Fun_ide g ide_compE inj_on_id2 inj_on_imageI2 inj_on_restrict_eq)
        ultimately show ?thesis by auto
      qed
      next
      assume F: "arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
      thus "section f" using section_if_inj by auto
    qed

    text‹
 Section-retraction pairs can also be characterized by an inverse relationship
 between the functions they induce.
 ›

    lemma section_retraction_char:
    shows "ide (g ⋅ f) ⟷ antipar f g ∧ compose (Dom f) (Fun g) (Fun f) = (λx ∈ Dom f. x)"
      by (metis Fun_comp cod_comp compose_eq' dom_comp ide_char_SC ide_compE seqE)

    text‹
 Antiparallel arrows @{term f} and @{term g} are inverses if the functions
 they induce are inverses.
 ›

    lemma inverse_arrows_char:
    shows "inverse_arrows f g ⟷
             antipar f g ∧ compose (Dom f) (Fun g) (Fun f) = (λx ∈ Dom f. x)
                         ∧ compose (Dom g) (Fun f) (Fun g) = (λy ∈ Dom g. y)"
      using section_retraction_char by blast

    text‹
 An arrow is an isomorphism if and only if the function it induces is a bijection.
 ›

    lemma iso_char:
    shows "iso f ⟷ arr f ∧ bij_betw (Fun f) (Dom f) (Cod f)"
      by (metis bij_betw_def image_empty iso_iff_section_and_retraction retraction_char
          section_char)

    text‹
 The inverse of an isomorphism is constructed by inverting the induced function.
 ›

    lemma inv_char:
    assumes "iso f"
    shows "inv f = mkArr (Cod f) (Dom f) (inv_into (Dom f) (Fun f))"
    proof -
      let ?g = "mkArr (Cod f) (Dom f) (inv_into (Dom f) (Fun f))"
      have "ide (f ⋅ ?g)"
        using assms iso_is_retraction retraction_char retraction_if_Img_eq_Cod by simp
      moreover have "ide (?g ⋅ f)"
      proof -
        let ?g' = "mkArr (Cod f) (Dom f)
                         (λy. if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
                              else SOME x. x ∈ Dom f)"
        have 1: "ide (?g' ⋅ f)"
          using assms iso_is_section section_char section_if_inj by simp
        moreover have "?g' = ?g"
        proof
          show "arr ?g'" using 1 ide_compE by blast
          show "∧y. y ∈ Cod f ==> (if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
                                                  else SOME x. x ∈ Dom f)
                                     = inv_into (Dom f) (Fun f) y"
          proof -
            fix y
            assume "y ∈ Cod f"
            hence "y ∈ Img f" using assms iso_is_retraction retraction_char by metis
            thus "(if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
                   else SOME x. x ∈ Dom f)
                     = inv_into (Dom f) (Fun f) y"
              using inv_into_def by metis
          qed
        qed
        ultimately show ?thesis by auto
      qed
      ultimately have "inverse_arrows f ?g" by auto
      thus ?thesis using inverse_unique by blast
    qed

    lemma Fun_inv:
    assumes "iso f"
    shows "Fun (inv f) = restrict (inv_into (Dom f) (Fun f)) (Cod f)"
      using assms inv_in_hom inv_char iso_inv_iso iso_is_arr Fun_mkArr by metis

    subsection "Monomorphisms and Epimorphisms"

    text‹
 An arrow is a monomorphism if and only if the function it induces is injective.
 ›

    lemma mono_char:
    shows "mono f ⟷ arr f ∧ inj_on (Fun f) (Dom f)"
    proof
      assume f: "mono f"
      hence "arr f" using mono_def by auto
      moreover have "inj_on (Fun f) (Dom f)"
      proof (intro inj_onI)
        have 0: "inj_on (S f) (hom unity (dom f))"
        proof -
          have "hom unity (dom f) ⊆ {g. seq f g}"
            using f mono_def arrI by auto
          hence "∃A. hom unity (dom f) ⊆ A ∧ inj_on (S f) A"
            using f mono_def by auto
          thus ?thesis
            by (meson inj_on_subset)
        qed
        fix x x'
        assume x: "x ∈ Dom f" and x': "x' ∈ Dom f" and xx': "Fun f x = Fun f x'"
        have "mkPoint (dom f) x ∈ hom unity (dom f) ∧
              mkPoint (dom f) x' ∈ hom unity (dom f)"
          using x x' ‹arr f› mkPoint_in_hom by simp
        moreover have "f ⋅ mkPoint (dom f) x = f ⋅ mkPoint (dom f) x'"
          using ‹arr f› x x' xx' comp_arr_mkPoint by simp
        ultimately have "mkPoint (dom f) x = mkPoint (dom f) x'"
          using 0 inj_onD [of "S f" "hom unity (dom f)" "mkPoint (dom f) x"] by simp
        thus "x = x'"
          using ‹arr f› x x' img_mkPoint(2) img_mkPoint(2) ide_dom by metis
      qed
      ultimately show "arr f ∧ inj_on (Fun f) (Dom f)" by auto
      next
      assume f: "arr f ∧ inj_on (Fun f) (Dom f)"
      show "mono f"
      proof
        show "arr f" using f by auto
        show "∧g g'. [seq f g; f ⋅ g = f ⋅ g'] ==> g = g'"
        proof -
          fix g g'
          assume fg: "seq f g" and eq: "f ⋅ g = f ⋅ g'"
          show "g = g'"
          proof (intro arr_eqI_SC)
            show par: "par g g'"
              using fg eq dom_comp by (metis seqE)
            show "Fun g = Fun g'"
              by (metis empty_is_image eq f fg ide_dom incl_in_def incl_in_img_cod
                  initial_arr_unique initial_empty empty_def mono_cancel mkIde_set
                  section_if_inj(1) section_is_mono seqE set_img subset_empty)
          qed
        qed
      qed
    qed

    text‹
 Inclusions are monomorphisms.
 ›

    lemma mono_imp_incl:
    assumes "incl f"
    shows "mono f"
      using assms incl_def Fun_incl mono_char by auto

    text‹
 A monomorphism is a section, except in case it has an empty domain set and
 a nonempty codomain set.
 ›

    lemma mono_imp_section:
    assumes "mono f" and "Dom f = {} ⟶ Cod f = {}"
    shows "section f"
      using assms mono_char section_char by auto

    text‹
 An arrow is an epimorphism if and only if either its image coincides with its
 codomain, or else the universe has only a single element (in which case all arrows
 are epimorphisms).
 ›

    lemma epi_char:
    shows "epi f ⟷ arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
    proof
      assume epi: "epi f"
      show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
      proof -
        have f: "arr f" using epi epi_implies_arr by auto
        moreover have "¬(∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t') ==> Img f = Cod f"
        proof -
          assume "¬(∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')"
          from this obtain tt and ff
            where B: "tt ∈ Univ ∧ ff ∈ Univ ∧ tt ≠ ff" by blast
          show "Img f = Cod f"
          proof
            show "Img f ⊆ Cod f" using f Fun_mapsto by auto
            show "Cod f ⊆ Img f"
            proof
              let ?g = "mkArr (Cod f) {ff, tt} (λy. tt)"
              let ?g' = "mkArr (Cod f) {ff, tt} (λy. if ∃x. x ∈ Dom f ∧ Fun f x = y
                                                     then tt else ff)"
              let ?b = "mkIde {ff, tt}"
              have b: "ide ?b"
                by (metis B finite.emptyI finite_imp_setp finite_insert ide_mkIde
                    insert_subset setp_imp_subset_Univ setp_singleton mem_Collect_eq)
              have g: "«?g : cod f → ?b¬ ∧ Fun ?g = (λy ∈ Cod f. tt)"
                using f B in_homI [of ?g "cod f" "mkIde {ff, tt}"] finite_imp_setp by simp
              have g': "?g' ∈ hom (cod f) ?b ∧
                        Fun ?g' = (λy ∈ Cod f. if ∃x. x ∈ Dom f ∧ Fun f x = y then tt else ff)"
                using f B in_homI [of ?g'] finite_imp_setp by simp
              have "?g ⋅ f = ?g' ⋅ f"
              proof (intro arr_eqI_SC)
                show "par (?g ⋅ f) (?g' ⋅ f)"
                  using f g g' by auto
                show "Fun (?g ⋅ f) = Fun (?g' ⋅ f)"
                  using f g g' Fun_comp comp_mkArr by fastforce
              qed
              hence gg': "?g = ?g'"
                by (metis (no_types, lifting) epi_cancel epi f g in_homE seqI)
              fix y
              assume y: "y ∈ Cod f"
              have "Fun ?g' y = tt" using gg' g y by simp
              hence "(if ∃x. x ∈ Dom f ∧ Fun f x = y then tt else ff) = tt"
                using g' y by simp
              hence "∃x. x ∈ Dom f ∧ Fun f x = y"
                using B by argo
              thus "y ∈ Img f" by blast
            qed
          qed
        qed
        ultimately show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
          by fast
      qed
      next
      show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')) ==> epi f"
      proof -
        have "arr f ∧ Img f = Cod f ==> epi f"
          using retraction_char retraction_is_epi by presburger
        moreover have "arr f ∧ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t') ==> epi f"
        proof -
          assume f: "arr f ∧ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')"
          have "∧f f'. par f f' ==> f = f'"
          proof -
            fix f f'
            assume ff': "par f f'"
            show "f = f'"
            proof (intro arr_eqI_SC)
              show "par f f'" using ff' by simp
              have "∧t t'. t ∈ Cod f ∧ t' ∈ Cod f ==> t = t'"
                using f ff' setp_imp_subset_Univ setp_set_ide ide_cod subsetD by blast
              thus "Fun f = Fun f'"
                using ff' Fun_mapsto [of f] Fun_mapsto [of f']
                      extensional_arb [of "Fun f" "Dom f"] extensional_arb [of "Fun f'" "Dom f"]
                by fastforce
            qed
          qed
          moreover have "∧g g'. par (g ⋅ f) (g' ⋅ f) ==> par g g'"
            by force
          ultimately show "epi f"
            using f by (intro epiI; metis)
        qed
        ultimately show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))
                           ==> epi f"
          by auto
      qed
    qed

    text‹
 An epimorphism is a retraction, except in the case of a degenerate universe with only
 a single element.
 ›

    lemma epi_imp_retraction:
    assumes "epi f" and "∃t t'. t ∈ Univ ∧ t' ∈ Univ ∧ t ≠ t'"
    shows "retraction f"
      using assms epi_char retraction_char by auto

    text‹
 Retraction/inclusion factorization is unique (not just up to isomorphism -- remember
 that the notion of inclusion is not categorical but depends on the arbitrarily chosen
 @{term img}).
 ›

    lemma unique_retr_incl_fact:
    assumes "seq m e" and "seq m' e'" and "m ⋅ e = m' ⋅ e'"
    and "incl m" and "incl m'" and "retraction e" and "retraction e'"
    shows "m = m'" and "e = e'"
    proof -
      have 1: "cod m = cod m' ∧ dom e = dom e'"
        using assms(1-3) by (metis dom_comp cod_comp)
      hence 2: "span e e'" using assms(1-2) by blast
      hence 3: "Fun e = Fun e'"
        using assms eq_Fun_iff_incl_joinable by meson
      hence "img e = img e'" using assms 1 img_def by auto
      moreover have "img e = cod e ∧ img e' = cod e'"
        using assms(6-7) retraction_char img_def mkIde_set by simp
      ultimately have "par e e'" using 2 by simp
      thus "e = e'" using 3 arr_eqI_SC by blast
      hence "par m m'" using assms(1) assms(2) 1 by fastforce
      thus "m = m'" using assms(4) assms(5) incls_coherent by blast
    qed

  end

  section "Concrete Set Categories"

  text‹
 The ‹set_category› locale is useful for stating results that depend on a
 category of @{typ 'a}-sets and functions, without having to commit to a particular
 element type @{typ 'a}. However, in applications we often need to work with a
 category of sets and functions that is guaranteed to contain sets corresponding
 to the subsets of some extrinsically given type @{typ 'a}.
 A \emph{concrete set category} is a set category ‹S› that is equipped
 with an injective function @{term ι} from type @{typ 'a} to ‹S.Univ›.
 The following locale serves to facilitate some of the technical aspects of passing
 back and forth between elements of type @{typ 'a} and the elements of ‹S.Univ›.
 ›

  locale concrete_set_category = set_category S setp
    for S :: "'s comp"      (infixr ‹⋅_S› 55)
    and setp :: "'s set ==> bool"
    and U :: "'a set"
    and ι :: "'a ==> 's" +
    assumes UP_mapsto: "ι ∈ U → Univ"
    and inj_UP: "inj_on ι U"
  begin

    abbreviation UP
    where "UP ≡ ι"

    abbreviation DN
    where "DN ≡ inv_into U UP"

    lemma DN_mapsto:
    shows "DN ∈ UP ` U → U"
      by (simp add: inv_into_into)

    lemma DN_UP [simp]:
    assumes "x ∈ U"
    shows "DN (UP x) = x"
      using assms inj_UP inv_into_f_f by simp
      
    lemma UP_DN [simp]:
    assumes "t ∈ UP ` U"
    shows "UP (DN t) = t"
      using assms o_def inj_UP by auto

    lemma bij_UP:
    shows "bij_betw UP U (UP ` U)"
      using inj_UP inj_on_imp_bij_betw by blast

    lemma bij_DN:
    shows "bij_betw DN (UP ` U) U"
      using bij_UP bij_betw_inv_into by blast

  end

  locale replete_concrete_set_category =
    replete_set_category S +
    concrete_set_category S ‹λA. A ⊆ Univ› U UP
    for S :: "'s comp"      (infixr ‹⋅_S› 55)
    and U :: "'a set"
    and UP :: "'a ==> 's"

  section "Sub-Set Categories"

  text‹
 In this section, we show that a full subcategory of a set category, obtained
 by imposing suitable further restrictions on the subsets of the universe
 that correspond to objects, is again a set category.
 ›

  locale sub_set_category =
    S: set_category +
  fixes ssetp :: "'a set ==> bool"
  assumes ssetp_singleton: "∧t. t ∈ S.Univ ==> ssetp {t}"
  and subset_closed: "∧B A. [B ⊆ A; ssetp A] ==> ssetp B"
  and union_closed: "∧A B. [ssetp A; ssetp B] ==> ssetp (A ∪ B)"
  and containment: "∧A. ssetp A ==> setp A"
  begin

    sublocale full_subcategory S ‹λa. S.ide a ∧ ssetp (S.set a)›
      by unfold_locales auto

    lemma is_full_subcategory:
    shows "full_subcategory S (λa. S.ide a ∧ ssetp (S.set a))"
      ..

    lemma ide_char_SSC:
    shows "ide a ⟷ S.ide a ∧ ssetp (S.set a)"
      using ide_char_SbC arr_char_SbC by fastforce

    lemma terminal_unity_SSC:
    shows "terminal S.unity"
    proof
      show "ide S.unity"
        using S.terminal_unity_SC S.terminal_def [of S.unity] S.terminal_char2 ide_char_SSC
              ssetp_singleton
        by force
      thus "∧a. ide a ==> ∃!f. in_hom f a S.unity"
        using S.terminal_unity_SC S.terminal_def ide_char_SbC ide_char' in_hom_char_FSbC
        by (metis (no_types, lifting))
    qed

    lemma terminal_char:
    shows "terminal t ⟷ S.terminal t"
    proof
      fix t
      assume t: "S.terminal t"
      have "ide t"
        using t ssetp_singleton ide_char_SSC S.terminal_char2 by force
      thus "terminal t"
        using t in_hom_char_FSbC ide_char_SSC arr_char_SbC S.terminal_def terminalI by auto
      next
      assume t: "terminal t"
      have 1: "S.ide t"
        using t ide_char_SbC terminal_def by simp
      moreover have "card (S.set t) = 1"
      proof -
        have "card (S.set t) = card (S.hom S.unity t)"
          using S.set_def S.inj_img
          by (metis 1 S.bij_betw_points_and_set bij_betw_same_card)
        also have "... = card (hom S.unity t)"
          using t in_hom_char_FSbC terminal_def terminal_unity_SSC by auto
        also have "... = 1"
        proof -
          have "∃!f. f ∈ hom S.unity t"
            using t terminal_def terminal_unity_SSC by force
          moreover have "∧A. card A = 1 ⟷ (∃!a. a ∈ A)"
            apply (intro iffI)
               apply (metis card_1_singletonE empty_iff insert_iff)
            using card_1_singleton_iff by auto
          ultimately show ?thesis by auto
        qed
        finally show ?thesis by blast
      qed
      ultimately show "S.terminal t"
        using 1 S.terminal_char1 card_1_singleton_iff
        by (metis One_nat_def singleton_iff)
    qed

    sublocale set_category comp ssetp
    proof
      text‹
 Here things are simpler if we define ‹img› appropriately so that we have
 ‹set = T.set› after accounting for the definition ‹unity ≡ SOME t. terminal t›,
 which is different from that of S.unity.
 ›
      have 1: "terminal (SOME t. terminal t)"
        using terminal_unity_SSC someI_ex [of terminal] by blast
      obtain i where i: "«i : S.unity → SOME t. terminal t¬"
        using terminal_unity_SSC someI_ex [of terminal] in_hom_char_FSbC terminal_def
        by auto
      obtain i' where i': "«i' : (SOME t. terminal t) → S.unity¬"
        using terminal_unity_SSC someI_ex [of S.terminal] S.terminal_def
        by (metis (no_types, lifting) 1 terminal_def)
      have ii': "inverse_arrows i i'"
      proof
        have "i' ⋅ i = S.unity"
          using i i' terminal_unity_SSC
          by (metis (no_types, lifting) S.comp_in_homI' S.ide_in_hom S.ide_unity S.in_homE
              S.terminalE S.terminal_unity_SC in_hom_char_FSbC)
        thus 2: "ide (comp i' i)"
          by (metis (no_types, lifting) cod_comp comp_simp i i' ide_char' in_homE seqI')
        have "i ⋅ i' = (SOME t. terminal t)"
          using 1
          by (metis (no_types, lifting) 2 comp_simp i' ide_compE in_homE inverse_arrowsE
              iso_iff_mono_and_retraction point_is_mono retractionI section_retraction_of_iso(2))
        thus "ide (comp i i')"
          using comp_char
          by (metis (no_types, lifting) 2 ide_char' dom_comp i' ide_compE in_homE seq_char_SbC)
      qed
      interpret set_category_data comp ‹λx. S.some_img (x ⋅ i)› ..
      have i_in_hom: "«i : S.unity → unity¬"
        using i unity_def by simp
      have i'_in_hom: "«i' : unity → S.unity¬"
        using i' unity_def by simp
      have "∧a. ide a ==> set a = S.set a"
      proof -
        fix a
        assume a: "ide a"
        have "set a = (λx. S.some_img (x ⋅ i)) ` hom unity a"
          using set_def by simp
        also have "... = S.some_img ` S.hom S.unity a"
        proof
          show "(λx. S.some_img (x ⋅ i)) ` hom unity a ⊆ S.some_img ` S.hom S.unity a"
            using i in_hom_char_FSbC i_in_hom by auto
          show "S.some_img ` S.hom S.unity a ⊆ (λx. S.some_img (x ⋅ i)) ` hom unity a"
          proof
            fix b
            assume b: "b ∈ S.some_img ` S.hom S.unity a"
            obtain x where x: "x ∈ S.hom S.unity a ∧ S.some_img x = b"
              using b by blast
            have "x ⋅ i' ∈ hom unity a"
              using x in_hom_char<sub>FSbC</sub> S.comp_in_homI a i' ideD(1) unity_def by force
            moreover have "S.some_img ((x ⋅ i') ⋅ i) = b"
              by (metis (no_types, lifting) i ii' x S.comp_assoc calculation comp_simp
                  ide_compE in_homE inverse_arrowsE mem_Collect_eq S.comp_arr_ide seqI'
                  seq_char<sub>SbC</sub> S.ide_unity unity_def)
            ultimately show "b ∈ (λx. S.some_img (x ⋅ i)) ` hom unity a" by blast
          qed
        qed
        also have "... = S.set a"
          using S.set_def by auto
        finally show "set a = S.set a" by blast
      qed
      interpret T: set_category_given_img comp ‹λx. S.some_img (x ⋅ i)› ssetp
      proof
        show "Collect terminal ≠ {}"
          using terminal_unity_SSC by blast
        show "∧A' A. [A' ⊆ A; ssetp A] ==> ssetp A'"
          using subset_closed by blast
        show "∧A B. [ssetp A; ssetp B] ==> ssetp (A ∪ B)"
          using union_closed by simp
        show "∧A. ssetp A ==> A ⊆ Univ"
          using S.setp_imp_subset_Univ containment terminal_char by presburger
        show "∧a b. [ide a; ide b; set a = set b] ==> a = b"
          using ide_char_SbC ‹∧a. ide a ==> set a = S.set a› S.extensional_set by auto
        show "∧a. ide a ==> ssetp (set a)"
          using ‹∧a. ide a ==> set a = S.set a› ide_char_SSC by force
        show "∧A. ssetp A ==> ∃a. ide a ∧ set a = A"
          using S.set_complete ‹∧a. ide a ==> set a = S.set a› containment ide_char_SSC by blast
        show "∧t. terminal t ==> t ∈ (λx. S.some_img (x ⋅ i)) ` hom unity t"
          using S.set_def S.stable_img ‹∧a. ide a ==> set a = S.set a› set_def
                terminal_char terminal_def
          by force
        show "∧a. ide a ==> inj_on (λx. S.some_img (x ⋅ i)) (hom unity a)"
        proof -
          fix a
          assume a: "ide a"
          show "inj_on (λx. S.some_img (x ⋅ i)) (hom unity a)"
          proof
            fix x y
            assume x: "x ∈ hom unity a" and y: "y ∈ hom unity a"
            and eq: "S.some_img (x ⋅ i) = S.some_img (y ⋅ i)"
            have "x ⋅ i = y ⋅ i"
            proof -
              have "x ⋅ i ∈ S.hom S.unity a ∧ y ⋅ i ∈ S.hom S.unity a"
                using in_hom_char_FSbC ‹«i : S.unity → unity¬› x y by blast
              thus ?thesis
                using a eq ide_char_SbC S.inj_img [of a] inj_on_def [of S.some_img] by simp
            qed
            have "x = (x ⋅ i) ⋅ i'"
              by (metis (no_types, lifting) S.comp_arr_ide S.comp_assoc S.inverse_arrowsE
                  S.match_4 i i' ii' inclusion_preserves_inverse mem_Collect_eq seqI'
                  seq_char_SbC unity_def x)
            also have "... = (y ⋅ i) ⋅ i'"
              using ‹x ⋅ i = y ⋅ i› by simp
            also have "... = y"
              by (metis (no_types, lifting) S.comp_arr_ide S.comp_assoc S.inverse_arrowsE
                  S.match_4 i i' ii' inclusion_preserves_inverse mem_Collect_eq seqI'
                  seq_char_SbC unity_def y)
            finally show "x = y" by simp
          qed
        qed
        show "∧f f'. [par f f'; ∧x. in_hom x unity (dom f) ==> comp f x = comp f' x]
                        ==> f = f'"
        proof -
          fix f f'
          assume par: "par f f'"
          assume eq: "∧x. in_hom x unity (dom f) ==> comp f x = comp f' x"
          have "S.par f f'"
            using par arr_char_SbC dom_char_SbC cod_char_SbC by auto
          moreover have "∧x. S.in_hom x S.unity (S.dom f) ==> f ⋅ x = f' ⋅ x"
          proof -
            fix x
            assume x: "S.in_hom x S.unity (S.dom f)"
            have "S.in_hom (x ⋅ i') unity (S.dom f)"
              using i'_in_hom in_hom_char_FSbC x by blast
            hence 1: "in_hom (x ⋅ i') unity (dom f)"
              using arr_dom dom_simp i in_hom_char_FSbC par unity_def by force
            hence "comp f (x ⋅ i') = comp f' (x ⋅ i')"
              using eq by blast
            hence "(f ⋅ (x ⋅ i')) ⋅ i = (f' ⋅ (x ⋅ i')) ⋅ i"
              using comp_char
              by (metis (no_types, lifting) 1 comp_simp in_homE seqI par)
            thus "f ⋅ x = f' ⋅ x"
              by (metis (no_types, lifting) S.comp_arr_dom S.comp_assoc S.comp_inv_arr
                  S.in_homE i_in_hom ii' in_hom_char_FSbC inclusion_preserves_inverse x)
          qed
          ultimately show "f = f'"
            using S.extensional_arr by blast
        qed
        show "∧a b F. [ide a; ide b; F ∈ hom unity a → hom unity b]
                        ==> ∃f. in_hom f a b ∧
                                (∀x. in_hom x unity (dom f) ⟶ comp f x = F x)"
        proof -
          fix a b F
          assume a: "ide a" and b: "ide b" and F: "F ∈ hom unity a → hom unity b"
          have "S.ide a"
            using a ide_char_SbC by blast
          have "S.ide b"
            using b ide_char_SbC by blast
          have 1: "(λx. F (x ⋅ i') ⋅ i) ∈ S.hom S.unity a → S.hom S.unity b"
          proof
            fix x
            assume x: "x ∈ S.hom S.unity a"
            have "x ⋅ i' ∈ S.hom unity a"
              using i'_in_hom in_hom_char_FSbC x by blast
            hence "x ⋅ i' ∈ hom unity a"
              using a in_hom_char_FSbC
              by (metis (no_types, lifting) ideD(1) i'_in_hom in_hom_char_FSbC mem_Collect_eq)
            hence "F (x ⋅ i') ∈ hom unity b"
              using a b F by blast
            hence "F (x ⋅ i') ∈ S.hom unity b"
              using b in_hom_char_FSbC by blast
            thus "F (x ⋅ i') ⋅ i ∈ S.hom S.unity b"
              using i in_hom_char_FSbC unity_def by auto
          qed
          obtain f where f: "S.in_hom f a b ∧ (∀x. S.in_hom x S.unity (S.dom f)
                               ⟶ f ⋅ x = (λx. F (x ⋅ i') ⋅ i) x)"
            using 1 S.fun_complete_ax ‹S.ide a› ‹S.ide b› by presburger
          show "∃f. in_hom f a b ∧ (∀x. in_hom x unity (dom f) ⟶ comp f x = F x)"
          proof -
            have "in_hom f a b"
              using f in_hom_char_FSbC ideD(1) a b by presburger
            moreover have "∀x. in_hom x unity (dom f) ⟶ comp f x = F x"
            proof (intro allI impI)
              fix x
              assume x: "in_hom x unity (dom f)"
              have xi: "S.in_hom (x ⋅ i) S.unity (S.dom f)"
                using f x i in_hom_char_FSbC dom_char_SbC
                by (metis (no_types, lifting) in_homE unity_def calculation S.comp_in_homI)
              hence 1: "f ⋅ (x ⋅ i) = F ((x ⋅ i) ⋅ i') ⋅ i"
                using f by blast
              hence "((f ⋅ x) ⋅ i) ⋅ i' = (F x ⋅ i) ⋅ i'"
                by (metis (no_types, lifting) xi S.comp_assoc S.inverse_arrowsE
                    S.seqI' i' ii' in_hom_char_FSbC inclusion_preserves_inverse S.comp_arr_ide)
              hence "f ⋅ x = F x"
                by (metis (no_types, lifting) xi 1 S.invert_side_of_triangle(2) S.match_2 S.match_3
                    S.seqI arr_char_SbC calculation S.in_homE S.inverse_unique S.isoI
                    ii' in_homE inclusion_preserves_inverse)
              thus "comp f x = F x"
                using comp_char
                by (metis (no_types, lifting) comp_simp in_homE seqI calculation x)
            qed
            ultimately show ?thesis by blast
          qed
        qed
      qed
      show "∃img. set_category_given_img comp img ssetp"
        using T.set_category_given_img_axioms by blast
    qed

    lemma is_set_category:
    shows "set_category comp ssetp"
      ..

  end

end