Theory SetCategory

(*  Title:       SetCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter SetCategory

theory SetCategory
imports Category Functor Subcategory
begin

  text‹
    This theory defines a locale set_category› that axiomatizes the notion
    ``category of @{typ 'a}-sets and functions between them'' in the context of HOL.
    A primary reason for doing this is to make it possible to prove results
    (such as the Yoneda Lemma) that use such categories without having to commit to a
    particular element type @{typ 'a} and without having the results depend on the
    concrete details of a particular construction.
    The axiomatization given here is categorical, in the sense that if categories
    @{term S} and @{term S'} each interpret the set_category› locale,
    then a bijection between the sets of terminal objects of @{term S} and @{term S'}
    extends to an isomorphism of @{term S} and @{term S'} as categories.

    The axiomatization is based on the following idea: if, for some type @{typ 'a},
    category @{term S} is the category of all @{typ 'a}-sets and functions between
    them, then the elements of type @{typ 'a} are in bijective correspondence with
    the terminal objects of category @{term S}.  In addition, if @{term unity}
    is an arbitrarily chosen terminal object of @{term S}, then for each object @{term a},
    the hom-set @{term "hom unity a"} (\emph{i.e.} the set of ``points'' or
    ``global elements'' of @{term a}) is in bijective correspondence with a subset
    of the terminal objects of @{term S}.  By making a specific, but arbitrary,
    choice of such a correspondence, we can then associate with each object @{term a}
    of @{term S} a set @{term "set a"} that consists of all terminal objects @{term t}
    that correspond to some point @{term x} of @{term a}.  Each arrow @{term f}
    then induces a function Fun f ∈ set (dom f) → set (cod f)›,
    defined on terminal objects of @{term S} by passing to points of @{term "dom f"},
    composing with @{term f}, then passing back from points of @{term "cod f"}
    to terminal objects.  Once we can associate a set with each object of @{term S}
    and a function with each arrow, we can force @{term S} to be isomorphic to the
    category of @{typ 'a}-sets by imposing suitable extensionality and completeness axioms.
›
 
  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_pointSC:
    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_eqISC:
    assumes "par f f'" and "Fun f = Fun f'"
    shows "f = f'"
      using assms comp_arr_pointSC extensional_arr by metis

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

    lemma ide_unity [simp]:
    shows "ide unity"
      using terminal_unitySC 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_pointSC 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_eqISC
          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_eqISC, 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_eqISC, 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_eqISC)
      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_unitySC 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_eqISC)
                  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')) = (λxset 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_unitySC 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_eqISC)
      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_eqISC)
      show par: "S'.par (Φ (Ψ f')) f'"
        using assms Φ.preserves_ide Ψ.preserves_ide Φ_ide INV.Φ_ide Φo_Ψo by auto
      show "S'.Fun (Φ (Ψ f')) = S'.Fun f'"
      proof -
        have "S'.arr (Φ (Ψ f'))" using assms by blast
        moreover have "Φ (Ψ f') =
                       S'.mkArr (S'.set (S'.dom f')) (S'.set (S'.cod f')) (Φa (Ψ f'))"
          using assms Φ_def INV.Φ_in_hom Φo_Ψo by simp
        moreover have "Φa (Ψ f') = (λx'  S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))"
          unfolding Φa_def
          using assms par Ψ.preserves_arr set_dom_Φ by metis
        ultimately have 1: "S'.Fun (Φ (Ψ f')) =
                            (λx'  S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))"
          using S'.Fun_mkArr by simp
        show ?thesis
        proof
          fix x'
          have "x'  S'.set (S'.dom f')  S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'"
            using 1 assms S'.Fun_mapsto extensional_def by (simp add: S'.Fun_def)
          moreover have "x'  S'.set (S'.dom f')  S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'"
          proof -
            assume x': "x'  S'.set (S'.dom f')"
            have "S'.Fun (Φ (Ψ f')) x' = φ (S.Fun (Ψ f') (ψ x'))"
              using x' 1 by auto
            also have "... = φ (Ψa f' (ψ x'))"
              using Fun_Ψ x' assms S'.setp_imp_subset_Univ bij_φ by metis
            also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))"
            proof -
              have "φ (Ψa f' (ψ x')) = φ (ψ (S'.Fun f' x'))"
              proof -
                have "x'  S'.Univ"
                  by (meson S'.ide_dom S'.setp_imp_subset_Univ S'.setp_set_ide assms subsetCE x')
                thus ?thesis
                  by (simp add: INV.Φa_def INV.ψ_φ x')
              qed
              also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))"
                using assms x' φ_ψ S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom
                by (metis subsetCE)
              finally show ?thesis by auto
            qed
            also have "... = S'.Fun f' x'"
            proof -
              have 2: "x'. x'  S'.Univ  φ (ψ x') = x'"
                using bij_φ bij_betw_inv_into_right by fast
              have "S'.Fun f' (φ (ψ x')) = S'.Fun f' x'"
                using assms x' 2 S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom
                by (metis subsetCE)
              moreover have "S'.Fun f' x'  S'.Univ"
                using x' assms S'.Fun_mapsto S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_cod
                by blast
              ultimately show ?thesis using 2 by auto
            qed
            finally show ?thesis by auto
          qed
          ultimately show "S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'" by auto
        qed
      qed
    qed
          
    lemma inverse_functors_Φ_Ψ:
    shows "inverse_functors S S' Ψ Φ"
    proof -
      interpret ΦΨ: composite_functor S S' S Φ Ψ ..
      have inv: "Ψ o Φ = S.map"
        using ΦΨ S.map_def ΦΨ.is_extensional by auto
    
      interpret ΨΦ: composite_functor S' S S' Ψ Φ ..
      have inv': "Φ o Ψ = S'.map"
        using ΨΦ S'.map_def ΨΦ.is_extensional by auto
    
      show ?thesis
        using inv inv' by (unfold_locales, auto)
    qed
      
    lemma are_isomorphic:
    shows "Φ. invertible_functor S S' Φ  (m. S.incl m  S'.incl (Φ m))"
    proof -
      interpret inverse_functors S S' Ψ Φ
        using inverse_functors_Φ_Ψ by auto
      have 1: "inverse_functors S S' Ψ Φ" ..
      interpret invertible_functor S S' Φ
        apply unfold_locales using 1 by auto
      have "invertible_functor S S' Φ" ..
      thus ?thesis using Φ_preserves_incl by auto
    qed
    
  end
  
  text‹
    The main result: @{locale set_category} is categorical, in the following (logical) sense:
    If S› and S'› are two "set categories", and if the sets of terminal objects of S› and S'›
    are in correspondence via a @{term setp}-preserving bijection, then S› and S'› are
    isomorphic as categories, via a functor that preserves inclusion maps, hence also the
    inclusion relation between sets.
›

  theorem set_category_is_categorical:
  assumes "set_category S setp" and "set_category S' setp'"
  and "bij_betw φ (set_category_data.Univ S) (set_category_data.Univ S')"
  and "A. A  set_category_data.Univ S  setp' (φ ` A)  setp A"
  shows "Φ. invertible_functor S S' Φ 
             (m. set_category.incl S setp m  set_category.incl S' setp' (Φ m))"
  proof -
    interpret S: set_category S setp using assms(1) by auto
    interpret S': set_category S' setp' using assms(2) by auto
    interpret two_set_categories_bij_betw_Univ S setp S' setp' φ
      apply (unfold_locales) using assms(3-4) by auto
    show ?thesis using are_isomorphic by auto
  qed
  
  section "Further Properties of Set Categories"

  text‹
    In this section we further develop the consequences of the set_category›
    axioms, and establish characterizations of a number of standard category-theoretic
    notions for a set_category›.
›

  context set_category
  begin
  
    abbreviation Dom
    where "Dom f  set (dom f)"
    
    abbreviation Cod
    where "Cod f  set (cod f)"

    subsection "Initial Object"

    text‹
      The object corresponding to the empty set is an initial object.
›

    definition empty
    where "empty = mkIde {}"

    lemma initial_empty:
    shows "initial empty"
    proof
      show 0: "ide empty"
        using empty_def by (simp add: setp_empty)
      show "b. ide b  ∃!f. «f : empty  b»"
      proof -
        fix b
        assume b: "ide b"
        show "∃!f. «f : empty  b»"
        proof
          show 1: "«mkArr {} (set b) (λx. x) : empty  b»"
            using 0 b empty_def mkArr_in_hom mkIde_set setp_imp_subset_Univ arr_mkIde
            by (metis Pi_I empty_iff ide_def mkIde_def)
          show "f. «f : empty  b»  f = mkArr {} (set b) (λx. x)"
            by (metis "1" arr_mkArr empty_iff in_homE empty_def mkArr_Fun mkArr_eqI set_mkIde)
        qed
      qed
    qed

    subsection "Identity Arrows"
    
    text‹
      Identity arrows correspond to restrictions of the identity function.
›

    lemma ide_charSC:
    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_charSC 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_eqISC)
        have 3: "arr (mkArr (Dom f) (Cod g) (λxDom 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) (λxDom f. x))"
          using assms 1 3 mkIde_set by auto
        show "Fun (g  f) = Fun (mkArr (Dom f) (Cod g) (λxDom 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_unitySC 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_eqISC)
      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_unitySC mkPoint_def)

    lemma Fun_mkPoint:
    assumes "ide a" and "t  set a"
    shows "Fun (mkPoint a t) = (λ_  {unity}. t)"
      using assms mkPoint_def terminal_unitySC 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_eqISC)
          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_unitySC)
        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_eqISC)
      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_unitySC 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_pointSSC:
    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_eqISC, 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_pointSSC 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)