Quelle  SetCat.thy

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

chapter SetCat

theory SetCat
imports SetCategory ConcreteCategory
begin

  text‹
 This theory proves the consistency of the ‹set_category› locale by giving
 a particular concrete construction of an interpretation for it.
 Applying the general construction given by @{locale concrete_category},
 we define arrows to be terms ‹MkArr A B F›, where ‹A› and ‹B› are sets
 and ‹F› is an extensional function that maps ‹A› to ‹B›.
 ›

  text‹
 This locale uses an extra dummy parameter just to fix the element type for sets.
 Without this, a type is used for each interpretation, which makes it impossible to
 construct set categories whose element types are related to the context.
 An additional parameter, @{term Setp}, allows some control over which subsets of
 the element type are assumed to correspond to objects of the category.
 ›

  locale setcat =
  fixes elem_type :: "'e itself"
  and Setp :: "'e set ==> bool"
  assumes Setp_singleton: "Setp {x}"
  and Setp_respects_subset: "A' ⊆ A ==> Setp A ==> Setp A'"
  and union_preserves_Setp: "[ Setp A; Setp B ] ==> Setp (A ∪ B)"
  begin

    lemma finite_imp_Setp: "finite A ==> Setp A"
      using Setp_singleton
      by (metis finite_induct insert_is_Un Setp_respects_subset singleton_insert_inj_eq
          union_preserves_Setp)

    type_synonym 'b arr = "('b set, 'b ==> 'b) concrete_category.arr"

    interpretation S: concrete_category ‹Collect Setp› ‹λA B. extensional A ∩ (A → B)›
                        ‹λA. λx ∈ A. x› ‹λC B A g f. compose A g f›
      using compose_Id Id_compose
      apply unfold_locales
          apply auto[3]
       apply blast
      by (metis IntD2 compose_assoc)

    abbreviation comp :: "'e setcat.arr comp"     (infixr ‹⋅› 55)
    where "comp ≡ S.COMP"
    notation S.in_hom                               (‹«_ : _ → _¬›)

    lemma is_category:
    shows "category comp"
      using S.category_axioms by simp

    lemma MkArr_expansion:
    assumes "S.arr f"
    shows "f = S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x)"
    proof (intro S.arr_eqI)
      show "S.arr f" by fact
      show "S.arr (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))"
        using assms S.arr_char
        by (metis (mono_tags, lifting) Int_iff S.MkArr_Map extensional_restrict)
      show "S.Dom f = S.Dom (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))"
        by simp
      show "S.Cod f = S.Cod (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))"
        by simp
      show "S.Map f = S.Map (S.MkArr (S.Dom f) (S.Cod f) (λx ∈ S.Dom f. S.Map f x))"
        using assms S.arr_char
        by (metis (mono_tags, lifting) Int_iff S.MkArr_Map extensional_restrict)
    qed

    lemma arr_char:
    shows "S.arr f ⟷ f ≠ S.Null ∧ Setp (S.Dom f) ∧ Setp (S.Cod f) ∧
                       S.Map f ∈ extensional (S.Dom f) ∩ (S.Dom f → S.Cod f)"
      using S.arr_char by auto

    lemma terminal_char:
    shows "S.terminal a ⟷ (∃x. a = S.MkIde {x})"
    proof
      show "∃x. a = S.MkIde {x} ==> S.terminal a"
      proof -
        assume a: "∃x. a = S.MkIde {x}"
        from this obtain x where x: "a = S.MkIde {x}" by blast
        have "S.terminal (S.MkIde {x})"
        proof
          show 1: "S.ide (S.MkIde {x})"
            using finite_imp_Setp S.ide_MkIde by auto
          show "∧a. S.ide a ==> ∃!f. «f : a → S.MkIde {x}¬"
          proof
            fix a :: "'e setcat.arr"
            assume a: "S.ide a"
            show "«S.MkArr (S.Dom a) {x} (λ_∈S.Dom a. x) : a → S.MkIde {x}¬"
              using a 1 S.arr_MkArr S.dom_MkArr S.cod_MkArr S.ide_char_CC S.MkArr_in_hom
              by (intro S.MkArr_in_hom) auto
            fix f :: "'e setcat.arr"
            assume f: "«f : a → S.MkIde {x}¬"
            show "f = S.MkArr (S.Dom a) {x} (λ_ ∈ S.Dom a. x)"
            proof -
              have 1: "S.Dom f = S.Dom a ∧ S.Cod f = {x}"
                using a f by (metis (mono_tags, lifting) S.Dom.simps(1) S.in_hom_char)
              moreover have "S.Map f = (λ_ ∈ S.Dom a. x)"
              proof
                fix z
                have "z ∉ S.Dom a ==> S.Map f z = (λ_ ∈ S.Dom a. x) z"
                  using f 1 MkArr_expansion
                  by (metis (mono_tags, lifting) S.Map.simps(1) S.in_homE restrict_apply)
                moreover have "z ∈ S.Dom a ==> S.Map f z = (λ_ ∈ S.Dom a. x) z"
                  using f 1 arr_char [of f] by fastforce
                ultimately show "S.Map f z = (λ_ ∈ S.Dom a. x) z" by auto
              qed
              ultimately show ?thesis
               using f MkArr_expansion [of f] by fastforce
            qed
          qed
        qed
        thus "S.terminal a" using x by simp
      qed
      show "S.terminal a ==> ∃x. a = S.MkIde {x}"
      proof -
        assume a: "S.terminal a"
        hence ide_a: "S.ide a" using S.terminal_def by auto
        have 1: "∃!x. x ∈ S.Dom a"
        proof -
          have "S.Dom a = {} ==> ¬S.terminal a"
          proof -
            assume "S.Dom a = {}"
            hence 1: "a = S.MkIde {}"
              using S.MkIde_Dom' ‹S.ide a› by fastforce
            have "∧f. f ∈ S.hom (S.MkIde {undefined}) (S.MkIde ({} :: 'e set))
                         ==> S.Map f ∈ {undefined} → {}"
            proof -
              fix f
              assume f: "f ∈ S.hom (S.MkIde {undefined}) (S.MkIde ({} :: 'e set))"
              show "S.Map f ∈ {undefined} → {}"
                using f MkArr_expansion arr_char [of f] S.in_hom_char by auto
            qed
            hence "S.hom (S.MkIde {undefined}) a = {}" using 1 by auto
            moreover have "S.ide (S.MkIde {undefined})"
              using finite_imp_Setp
              by (metis (mono_tags, lifting) finite.intros(1-2) S.ide_MkIde mem_Collect_eq)
            ultimately show "¬S.terminal a" by blast
          qed
          moreover have "∧x x'. x ∈ S.Dom a ∧ x' ∈ S.Dom a ∧ x ≠ x' ==> ¬S.terminal a"
          proof -
            fix x x'
            assume 1: "x ∈ S.Dom a ∧ x' ∈ S.Dom a ∧ x ≠ x'"
            let ?f = "S.MkArr {undefined} (S.Dom a) (λ_ ∈ {undefined}. x)"
            let ?f' = "S.MkArr {undefined} (S.Dom a) (λ_ ∈ {undefined}. x')"
            have "S.par ?f ?f'"
              using 1 S.Dom_in_Obj S.arr_MkArr S.cod_MkArr S.dom_MkArr S.ideD(1)
                    Setp_singleton ide_a
              by force
            moreover have "?f ≠ ?f'"
              using 1 by (metis S.arr.inject restrict_apply' singletonI)
            ultimately show "¬S.terminal a"
              using S.cod_MkArr ide_a S.terminal_arr_unique [of ?f ?f'] by auto
          qed
          ultimately show ?thesis
            using a by auto
        qed
        hence "S.Dom a = {THE x. x ∈ S.Dom a}"
          using theI [of "λx. x ∈ S.Dom a"] by auto
        hence "a = S.MkIde {THE x. x ∈ S.Dom a}"
          using a S.terminal_def by (metis (mono_tags, lifting) S.MkIde_Dom')
        thus "∃x. a = S.MkIde {x}"
          by auto
      qed
    qed

    definition IMG :: "'e setcat.arr ==> 'e setcat.arr"
    where "IMG f = S.MkIde (S.Map f ` S.Dom f)"
  
    interpretation S: set_category_data comp IMG
      ..

    lemma terminal_unity:
    shows "S.terminal S.unity"
      using terminal_char S.unity_def someI_ex [of S.terminal]
      by (metis (mono_tags, lifting))
  
    text‹
 The inverse maps @{term arr_of} and @{term elem_of} are used to pass back and forth
 between the inhabitants of type @{typ 'a} and the corresponding terminal objects.
 These are exported so that a client of the theory can relate the concrete
 element type @{typ 'a} to the otherwise abstract arrow type.
 ›

    definition arr_of :: "'e ==> 'e setcat.arr"
    where "arr_of x ≡ S.MkIde {x}"
  
    definition elem_of :: "'e setcat.arr ==> 'e"
    where "elem_of t ≡ the_elem (S.Dom t)"

    abbreviation U
    where "U ≡ elem_of S.unity"
  
    lemma arr_of_mapsto:
    shows "arr_of ∈ UNIV → S.Univ"
      using terminal_char arr_of_def by fast
    
    lemma elem_of_mapsto:
    shows "elem_of ∈ Univ → UNIV"
      by auto
    
    lemma elem_of_arr_of [simp]:
    shows "elem_of (arr_of x) = x"
      by (simp add: elem_of_def arr_of_def)
    
    lemma arr_of_elem_of [simp]:
    assumes "t ∈ S.Univ"
    shows "arr_of (elem_of t) = t"
      using assms terminal_char arr_of_def elem_of_def
      by (metis (mono_tags, lifting) mem_Collect_eq elem_of_arr_of)
  
    lemma inj_arr_of:
    shows "inj arr_of"
      by (metis elem_of_arr_of injI)
  
    lemma bij_arr_of:
    shows "bij_betw arr_of UNIV S.Univ"
    proof (intro bij_betwI)
      show "∧x :: 'e. elem_of (arr_of x) = x" by simp
      show "∧t. t ∈ S.Univ ==> arr_of (elem_of t) = t" by simp
      show "arr_of ∈ UNIV → S.Univ" using arr_of_mapsto by auto
      show "elem_of ∈ Collect S.terminal → UNIV" by auto
    qed
  
    lemma bij_elem_of:
    shows "bij_betw elem_of S.Univ UNIV"
      using elem_of_mapsto arr_of_mapsto
      by (intro bij_betwI) auto

    lemma elem_of_img_arr_of_img [simp]:
    shows "elem_of ` arr_of ` A = A"
      by force

    lemma arr_of_img_elem_of_img [simp]:
    assumes "A ⊆ S.Univ"
    shows "arr_of ` elem_of ` A = A"
      using assms by force

    lemma Dom_terminal:
    assumes "S.terminal t"
    shows "S.Dom t = {elem_of t}"
      using assms arr_of_def
      by (metis (mono_tags, lifting) S.Dom.simps(1) elem_of_def terminal_char the_elem_eq)

    text‹
 The image of a point @{term "p ∈ hom unity a"} is a terminal object, which is given
 by the formula @{term "(arr_of o Fun p o elem_of) unity"}.
 ›

    lemma IMG_point:
    assumes "«p : S.unity → a¬"
    shows "IMG ∈ S.hom S.unity a → S.Univ"
    and "IMG p = (arr_of o S.Map p o elem_of) S.unity"
    proof -
      show "IMG ∈ S.hom S.unity a → S.Univ"
      proof
        fix f
        assume f: "f ∈ S.hom S.unity a"
        have "S.terminal (S.MkIde (S.Map f ` S.Dom S.unity))"
          using terminal_char terminal_unity by force
        hence "S.MkIde (S.Map f ` S.Dom S.unity) ∈ S.Univ" by simp
        moreover have "S.MkIde (S.Map f ` S.Dom S.unity) = IMG f"
          using f IMG_def S.in_hom_char
          by (metis (mono_tags, lifting) mem_Collect_eq)
        ultimately show "IMG f ∈ S.Univ" by auto
      qed
      have "IMG p = S.MkIde (S.Map p ` S.Dom p)" using IMG_def by blast
      also have "... = S.MkIde (S.Map p ` {U})"
        using assms S.in_hom_char terminal_unity Dom_terminal
        by (metis (mono_tags, lifting))
      also have "... = (arr_of o S.Map p o elem_of) S.unity" by (simp add: arr_of_def)
      finally show "IMG p = (arr_of o S.Map p o elem_of) S.unity" using assms by auto
    qed
  
    text‹
 The function @{term IMG} is injective on @{term "hom unity a"} and its inverse takes
 a terminal object @{term t} to the arrow in @{term "hom unity a"} corresponding to the
 constant-@{term t} function.
 ›

    abbreviation MkElem :: "'e setcat.arr => 'e setcat.arr => 'e setcat.arr"
    where "MkElem t a ≡ S.MkArr {U} (S.Dom a) (λ_ ∈ {U}. elem_of t)"

    lemma MkElem_in_hom:
    assumes "S.arr f" and "x ∈ S.Dom f"
    shows "«MkElem (arr_of x) (S.dom f) : S.unity → S.dom f¬"
    proof -
      have "(λ_ ∈ {U}. elem_of (arr_of x)) ∈ {U} → S.Dom (S.dom f)"
        using assms S.dom_char [of f] by simp
      moreover have "S.MkIde {U} = S.unity"
        using terminal_char terminal_unity
        by (metis (mono_tags, lifting) elem_of_arr_of arr_of_def)
      moreover have "S.MkIde (S.Dom (S.dom f)) = S.dom f"
        using assms S.dom_char S.MkIde_Dom' S.ide_dom by blast
      ultimately show ?thesis
        using assms S.MkArr_in_hom [of "{U}" "S.Dom (S.dom f)" "λ_ ∈ {U}. elem_of (arr_of x)"]
        by (metis (no_types, lifting) S.Dom.simps(1) S.Dom_in_Obj IntI S.arr_dom S.ideD(1)
            restrict_extensional S.terminal_def terminal_unity)
    qed

    lemma MkElem_IMG:
    assumes "p ∈ S.hom S.unity a"
    shows "MkElem (IMG p) a = p"
    proof -
      have 0: "IMG p = arr_of (S.Map p U)"
        using assms IMG_point(2) by auto
      have 1: "S.Dom p = {U}"
        using assms terminal_unity Dom_terminal
        by (metis (mono_tags, lifting) S.in_hom_char mem_Collect_eq)
      moreover have "S.Cod p = S.Dom a"
        using assms
        by (metis (mono_tags, lifting) S.in_hom_char mem_Collect_eq)
      moreover have "S.Map p = (λ_ ∈ {U}. elem_of (IMG p))"
      proof
        fix e
        show "S.Map p e = (λ_ ∈ {U}. elem_of (IMG p)) e"
        proof -
          have "S.Map p e = (λx ∈ S.Dom p. S.Map p x) e"
            using assms MkArr_expansion [of p]
            by (metis (mono_tags, lifting) CollectD S.Map.simps(1) S.in_homE)
          also have "... = (λ_ ∈ {U}. elem_of (IMG p)) e"
            using assms 0 1 by simp
          finally show ?thesis by blast
        qed
      qed
      ultimately show "MkElem (IMG p) a = p"
        using assms S.MkArr_Map CollectD
        by (metis (mono_tags, lifting) S.in_homE mem_Collect_eq)
    qed

    lemma inj_IMG:
    assumes "S.ide a"
    shows "inj_on IMG (S.hom S.unity a)"
    proof (intro inj_onI)
      fix x y
      assume x: "x ∈ S.hom S.unity a"
      assume y: "y ∈ S.hom S.unity a"
      assume eq: "IMG x = IMG y"
      show "x = y"
      proof (intro S.arr_eqI)
        show "S.arr x" using x by blast
        show "S.arr y" using y by blast
        show "S.Dom x = S.Dom y"
          using x y S.in_hom_char by (metis (mono_tags, lifting) CollectD)
        show "S.Cod x = S.Cod y"
          using x y S.in_hom_char by (metis (mono_tags, lifting) CollectD)
        show "S.Map x = S.Map y"
        proof -
          have "∧a. y ∈ S.hom S.unity a ==> S.MkArr {U} (S.Dom a) (λe∈{U}. elem_of (IMG x)) = y"
            using MkElem_IMG eq by presburger
          hence "y = x"
            using MkElem_IMG x y by blast
          thus ?thesis by meson
        qed
      qed
    qed

    lemma set_char:
    assumes "S.ide a"
    shows "S.set a = arr_of ` S.Dom a"
    proof
      show "S.set a ⊆ arr_of ` S.Dom a"
      proof
        fix t
        assume "t ∈ S.set a"
        from this obtain p where p: "«p : S.unity → a¬ ∧ t = IMG p"
          using S.set_def by blast
        have "t = (arr_of o S.Map p o elem_of) S.unity"
          using p IMG_point(2) by blast
        moreover have "(S.Map p o elem_of) S.unity ∈ S.Dom a"
          using p arr_char S.in_hom_char Dom_terminal terminal_unity
          by (metis (mono_tags, lifting) IntD2 Pi_split_insert_domain o_apply)
        ultimately show "t ∈ arr_of ` S.Dom a" by simp
      qed
      show "arr_of ` S.Dom a ⊆ S.set a"
      proof
        fix t
        assume "t ∈ arr_of ` S.Dom a"
        from this obtain x where x: "x ∈ S.Dom a ∧ t = arr_of x" by blast
        let ?p = "MkElem (arr_of x) a"
        have p: "?p ∈ S.hom S.unity a"
          using assms x MkElem_in_hom [of "S.dom a"] S.ideD(1-2) by force
        moreover have "IMG ?p = t"
          using p x elem_of_arr_of IMG_def arr_of_def
          by (metis (no_types, lifting) S.Dom.simps(1) S.Map.simps(1) image_empty
              image_insert image_restrict_eq)
        ultimately show "t ∈ S.set a" using S.set_def by blast
      qed
    qed
  
    lemma Map_via_comp:
    assumes "S.arr f"
    shows "S.Map f = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U)"
    proof
      fix x
      have "x ∉ S.Dom f ==> S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x"
        using assms arr_char [of f] IntD1 extensional_arb restrict_apply by fastforce
      moreover have
           "x ∈ S.Dom f ==> S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x"
      proof -
        assume x: "x ∈ S.Dom f"
        let ?X = "MkElem (arr_of x) (S.dom f)"
        have "«?X : S.unity → S.dom f¬"
          using assms x MkElem_in_hom by auto
        moreover have "S.Dom ?X = {U} ∧ S.Map ?X = (λ_ ∈ {U}. x)"
          using x by simp
        ultimately have
          "S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) = compose {U} (S.Map f) (λ_ ∈ {U}. x)"
          using assms x S.Map_comp [of "MkElem (arr_of x) (S.dom f)" f]
          by (metis (mono_tags, lifting) S.Cod.simps(1) S.Dom_dom S.arr_iff_in_hom S.seqE S.seqI')
        thus ?thesis
          using x by (simp add: compose_eq restrict_apply' singletonI)
      qed
      ultimately show "S.Map f x = (λx ∈ S.Dom f. S.Map (f ⋅ MkElem (arr_of x) (S.dom f)) U) x"
        by auto
    qed

    lemma arr_eqI':
    assumes "S.par f f'" and "∧t. «t : S.unity → S.dom f¬ ==> f ⋅ t = f' ⋅ t"
    shows "f = f'"
    proof (intro S.arr_eqI)
      show "S.arr f" using assms by simp
      show "S.arr f'" using assms by simp
      show "S.Dom f = S.Dom f'"
        using assms by (metis (mono_tags, lifting) S.Dom_dom)
      show "S.Cod f = S.Cod f'"
        using assms by (metis (mono_tags, lifting) S.Cod_cod)
      show "S.Map f = S.Map f'"
      proof
        have 1: "∧x. x ∈ S.Dom f ==> «MkElem (arr_of x) (S.dom f) : S.unity → S.dom f¬"
          using MkElem_in_hom by (metis (mono_tags, lifting) assms(1))
        fix x
        show "S.Map f x = S.Map f' x"
          using assms 1 ‹S.Dom f = S.Dom f'› by (simp add: Map_via_comp)
      qed
    qed

    lemma Setp_elem_of_img:
    assumes "A ∈ S.set ` Collect S.ide"
    shows "Setp (elem_of ` A)"
    proof -
      obtain a where a: "S.ide a ∧ S.set a = A"
        using assms by blast
      have "elem_of ` S.set a = S.Dom a"
      proof -
        have "S.set a = arr_of ` S.Dom a"
        using a set_char by blast
        moreover have "elem_of ` arr_of ` S.Dom a = S.Dom a"
          using elem_of_arr_of by force
        ultimately show ?thesis by presburger
      qed
      thus ?thesis
        using a S.ide_char_CC by auto
    qed

    lemma set_MkIde_elem_of_img:
    assumes "A ⊆ S.Univ" and "S.ide (S.MkIde (elem_of ` A))"
    shows "S.set (S.MkIde (elem_of ` A)) = A"
    proof -
      have "S.Dom (S.MkIde (elem_of ` A)) = elem_of ` A"
        by simp
      moreover have "arr_of ` elem_of ` A = A"
        using assms arr_of_elem_of by force
      ultimately show ?thesis
        using assms Setp_elem_of_img set_char S.ide_MkIde by auto
    qed

    (*
     * We need this result, which characterizes what sets of terminals correspond
     * to sets.
     *)
    lemma set_img_Collect_ide_iff:
    shows "A ∈ S.set ` Collect S.ide ⟷ A ⊆ S.Univ ∧ Setp (elem_of ` A)"
    proof
      show "A ∈ S.set ` Collect S.ide ==> A ⊆ S.Univ ∧ Setp (elem_of ` A)"
        using set_char arr_of_mapsto Setp_elem_of_img by auto
      assume A: "A ⊆ S.Univ ∧ Setp (elem_of ` A)"
      have "S.ide (S.MkIde (elem_of ` A))"
        using A S.ide_MkIde by blast
      moreover have "S.set (S.MkIde (elem_of ` A)) = A"
        using A calculation set_MkIde_elem_of_img by presburger
      ultimately show "A ∈ S.set ` Collect S.ide" by blast
    qed

    text‹
 The main result, which establishes the consistency of the ‹set_category› locale
 and provides us with a way of obtaining ``set categories'' at arbitrary types.
 ›

    theorem is_set_category:
    shows "set_category comp (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))"
    proof
      show "∃img :: 'e setcat.arr ==> 'e setcat.arr.
                       set_category_given_img comp img (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))"
      proof
        show "set_category_given_img comp IMG (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A))"
        proof
          show "S.Univ ≠ {}" using terminal_char by blast
          fix a :: "'e setcat.arr"
          assume a: "S.ide a"
          show "S.set a ⊆ S.Univ ∧ Setp (elem_of ` S.set a)"
            using a set_img_Collect_ide_iff by auto
          show "inj_on IMG (S.hom S.unity a)" using a inj_IMG terminal_unity by blast
          next
          fix t :: "'e setcat.arr"
          assume t: "S.terminal t"
          show "t ∈ IMG ` S.hom S.unity t"
          proof -
            have "t ∈ S.set t"
              using t set_char [of t]
              by (metis (mono_tags, lifting) S.Dom.simps(1) image_insert insertI1 arr_of_def
                  terminal_char S.terminal_def)
            thus ?thesis
              using t S.set_def [of t] by simp
          qed
          next
          show "∧A. A ⊆ S.Univ ∧ Setp (elem_of ` A) ==> ∃a. S.ide a ∧ S.set a = A"
            using set_img_Collect_ide_iff by fast
          next
          fix a b :: "'e setcat.arr"
          assume a: "S.ide a" and b: "S.ide b" and ab: "S.set a = S.set b"
          show "a = b"
            using a b ab set_char inj_arr_of inj_image_eq_iff S.dom_char S.in_homE S.ide_in_hom
            by (metis (mono_tags, lifting))
          next
          fix f f' :: "'e setcat.arr"
          assume par: "S.par f f'" and ff': "∧x. «x : S.unity → S.dom f¬ ==> f ⋅ x = f' ⋅ x"
          show "f = f'" using par ff' arr_eqI' by blast
          next
          fix a b :: "'e setcat.arr" and F :: "'e setcat.arr ==> 'e setcat.arr"
          assume a: "S.ide a" and b: "S.ide b" and F: "F ∈ S.hom S.unity a → S.hom S.unity b"
          show "∃f. «f : a → b¬ ∧ (∀x. «x : S.unity → S.dom f¬ ⟶ f ⋅ x = F x)"
          proof
            let ?f = "S.MkArr (S.Dom a) (S.Dom b) (λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U)"
            have 1: "«?f : a → b¬"
            proof -
              have "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U)
                      ∈ extensional (S.Dom a) ∩ (S.Dom a → S.Dom b)"
              proof
                show "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U) ∈ extensional (S.Dom a)"
                  using a F by simp
                show "(λx ∈ S.Dom a. S.Map (F (MkElem (arr_of x) a)) U) ∈ S.Dom a → S.Dom b"
                proof
                  fix x
                  assume x: "x ∈ S.Dom a"
                  show "S.Map (F (MkElem (arr_of x) a)) U ∈ S.Dom b"
                  proof -
                    have 1: "F (MkElem (arr_of x) a) ∈ S.hom S.unity b"
                      using x a F MkElem_in_hom S.ide_char S.ideD(1-2)
                      by force
                    moreover have "S.Dom (F (MkElem (arr_of x) a)) = {U}"
                      using 1 MkElem_IMG
                      by (metis (mono_tags, lifting) S.Dom.simps(1))
                    moreover have "S.Cod (F (MkElem (arr_of x) a)) = S.Dom b"
                      using 1 by (metis (mono_tags, lifting) CollectD S.in_hom_char)
                    ultimately have "S.Map (F (MkElem (arr_of x) a)) ∈ {U} → S.Dom b"
                      using arr_char by blast
                    thus ?thesis by blast
                  qed
                qed
              qed
              hence "«?f : S.MkIde (S.Dom a) → S.MkIde (S.Dom b)¬"
                using a b S.MkArr_in_hom S.ide_char_CC by blast
              thus ?thesis
                using a b by simp
            qed
            moreover have "∧x. «x : S.unity → S.dom ?f¬ ==> ?f ⋅ x = F x"
            proof -
              fix x
              assume x: "«x : S.unity → S.dom ?f¬"
              have 2: "x = MkElem (IMG x) a"
                using a x 1 MkElem_IMG [of x a]
                by (metis (mono_tags, lifting) S.in_homE mem_Collect_eq)
              moreover have 5: "S.Dom x = {U} ∧ S.Cod x = S.Dom a ∧
                                S.Map x = (λ_ ∈ {U}. elem_of (IMG x))"
                using x 2
                by (metis (no_types, lifting) S.Cod.simps(1) S.Dom.simps(1) S.Map.simps(1))
              moreover have "S.Cod ?f = S.Dom b" using 1 by simp
              ultimately have
                   3: "?f ⋅ x =
                       S.MkArr {U} (S.Dom b) (compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)))"
                by (metis (no_types, lifting) "1" S.Map.simps(1) S.comp_MkArr S.in_homE x)
              have 4: "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) = S.Map (F x)"
              proof
                fix y
                have "y ∉ {U} ==>
                        compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y"
                proof -
                  assume y: "y ∉ {U}"
                  have "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = undefined"
                    using y compose_def by simp
                  also have "... = S.Map (F x) y"
                  proof -
                    have 6: "F x ∈ S.hom S.unity b" using x F 1 by fastforce
                    hence "S.Dom (F x) = {U}"
                      by (metis (mono_tags, lifting) x 2 CollectD S.Dom.simps(1) S.in_hom_char)
                    thus ?thesis
                      using x y F 6 arr_char extensional_arb [of "S.Map (F x)" "{U}" y]
                      by (metis (mono_tags, lifting) CollectD Int_iff S.in_hom_char)
                  qed
                  ultimately show ?thesis by auto
                qed
                moreover have
                    "y ∈ {U} ==>
                       compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y"
                proof -
                  assume y: "y ∈ {U}"
                  have "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y =
                        S.Map ?f (elem_of (IMG x))"
                    using y by (simp add: compose_eq restrict_apply')
                  also have "... = (λx. S.Map (F (MkElem (arr_of x) a)) U) (elem_of (IMG x))"
                  proof -
                    have "elem_of (IMG x) ∈ S.Dom a"
                      using x y a 5 arr_char S.in_homE restrict_apply by force
                    thus ?thesis
                      using restrict_apply by simp
                  qed
                  also have "... = S.Map (F x) y"
                    using x y 1 2 MkElem_IMG by simp
                  finally show
                      "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y"
                    by auto
                qed
                ultimately show
                    "compose {U} (S.Map ?f) (λ_ ∈ {U}. elem_of (IMG x)) y = S.Map (F x) y"
                  by auto
              qed
              show "?f ⋅ x = F x"
              proof (intro S.arr_eqI)
                have 5: "?f ⋅ x ∈ S.hom S.unity b" using 1 x by blast
                have 6: "F x ∈ S.hom S.unity b"
                  using x F 1
                  by (metis (mono_tags, lifting) PiE S.in_homE mem_Collect_eq)
                show "S.arr (comp ?f x)" using 5 by blast
                show "S.arr (F x)" using 6 by blast
                show "S.Dom (comp ?f x) = S.Dom (F x)"
                  using 5 6 by (metis (mono_tags, lifting) CollectD S.in_hom_char)
                show "S.Cod (comp ?f x) = S.Cod (F x)"
                  using 5 6 by (metis (mono_tags, lifting) CollectD S.in_hom_char)
                show "S.Map (comp ?f x) = S.Map (F x)"
                  using 3 4 by simp
              qed
            qed
            thus "«?f : a → b¬ ∧ (∀x. «x : S.unity → S.dom ?f¬ ⟶ comp ?f x = F x)"
              using 1 by blast
          qed
          next
          show "∧A. A ⊆ S.Univ ∧ Setp (elem_of ` A) ==> A ⊆ S.Univ"
            by simp
          show "∧A' A. [A' ⊆ A; A ⊆ S.Univ ∧ Setp (elem_of ` A)]
                           ==> A' ⊆ S.Univ ∧ Setp (elem_of ` A')"
            by (meson image_mono setcat.Setp_respects_subset setcat_axioms subset_trans)
          show "∧A B. [A ⊆ S.Univ ∧ Setp (elem_of ` A); B ⊆ S.Univ ∧ Setp (elem_of ` B)]
                         ==> A ∪ B ⊆ S.Univ ∧ Setp (elem_of ` (A ∪ B))"
            by (simp add: image_Un union_preserves_Setp)
        qed
      qed
    qed

    text‹
 ‹SetCat› can be viewed as a concrete set category over its own element type
 @{typ 'a}, using @{term arr_of} as the required injection from @{typ 'a} to the universe
 of ‹SetCat›.
 ›

    corollary is_concrete_set_category:
    shows "concrete_set_category comp (λA. A ⊆ S.Univ ∧ Setp (elem_of ` A)) UNIV arr_of"
    proof -
      interpret S': set_category comp ‹λA. A ⊆ S.Univ ∧ Setp (elem_of ` A)›
        using is_set_category by auto
      show ?thesis
      proof
        show 1: "arr_of ∈ UNIV → S'.Univ"
          using arr_of_def terminal_char by force
        show "inj_on arr_of UNIV"
          using inj_arr_of by blast
      qed
    qed

    text‹
 As a consequence of the categoricity of the ‹set_category› axioms,
 if @{term S} interprets ‹set_category›, and if @{term φ} is a bijection between
 the universe of @{term S} and the elements of type @{typ 'a}, then @{term S} is isomorphic
 to the category ‹setcat› of @{typ 'a} sets and functions between them constructed here.
 ›

    corollary set_category_iso_SetCat:
    fixes S :: "'s comp" and φ :: "'s ==> 'e"
    assumes "set_category S S"
    and "bij_betw φ (set_category_data.Univ S) UNIV"
    and "∧A. S A ⟷ A ⊆ set_category_data.Univ S ∧ (arr_of ∘ φ) ` A ∈ S.set ` Collect S.ide"
    shows "∃Φ. invertible_functor S comp Φ
                 ∧ (∀m. set_category.incl S S m
                           ⟶ set_category.incl comp (λA. A ∈ S.set ` Collect S.ide) (Φ m))"
    proof -
      interpret S': set_category S S using assms by auto
      let ?ψ = "inv_into S'.Univ φ"
      have "bij_betw (arr_of o φ) S'.Univ S.Univ"
      proof (intro bij_betwI)
        show "arr_of o φ ∈ S'.Univ → Collect S.terminal"
          using assms(2) arr_of_mapsto by auto
        show "?ψ o elem_of ∈ S.Univ → S'.Univ"
        proof
          fix x :: "'e setcat.arr"
          assume x: "x ∈ S.Univ"
          show "(inv_into S'.Univ φ ∘ elem_of) x ∈ S'.Univ"
            using x assms(2) bij_betw_def comp_apply inv_into_into
            by (metis UNIV_I)
        qed
        fix t
        assume "t ∈ S'.Univ"
        thus "(?ψ o elem_of) ((arr_of o φ) t) = t"
          using assms(2) bij_betw_inv_into_left
          by (metis comp_apply elem_of_arr_of)
        next
        fix t' :: "'e setcat.arr"
        assume "t' ∈ S.Univ"
        thus "(arr_of o φ) ((?ψ o elem_of) t') = t'"
          using assms(2) by (simp add: bij_betw_def f_inv_into_f)
      qed
      thus ?thesis
        using assms is_set_category set_img_Collect_ide_iff
              set_category_is_categorical
                [of S S comp "λA. A ∈ S.set ` Collect S.ide" "arr_of o φ"]
        by simp
    qed

    sublocale category comp
      using is_category by blast
    sublocale set_category comp ‹λA. A ⊆ Collect S.terminal ∧ Setp (elem_of ` A)›
      using is_set_category set_img_Collect_ide_iff by simp
    interpretation concrete_set_category comp ‹λA. A ⊆ Collect S.terminal ∧ Setp (elem_of ` A)›
                       UNIV arr_of
      using is_concrete_set_category by simp
 
  end
(*
  interpretation SetCat: setcat undefined \<open>\<lambda>S. True\<close>
    by unfold_locales auto
 *)
  text‹
 Here we discard the temporary interpretations ‹S›, leaving only the exported
 definitions and facts.
 ›

  context setcat
  begin

    text‹
 We establish mappings to pass back and forth between objects and arrows of the category
 and sets and functions on the underlying elements.
 ›

    interpretation set_category comp ‹λA. A ⊆ Collect terminal ∧ Setp (elem_of ` A)›
      using is_set_category by blast
    interpretation concrete_set_category comp ‹λA. A ⊆ Univ ∧ Setp (elem_of ` A)› UNIV arr_of
      using is_concrete_set_category by blast

    definition set_of_ide :: "'e setcat.arr ==> 'e set"
    where "set_of_ide a ≡ elem_of ` set a"

    definition ide_of_set :: "'e set ==> 'e setcat.arr"
    where "ide_of_set A ≡ mkIde (arr_of ` A)"

    lemma bij_betw_ide_set:
    shows "set_of_ide ∈ Collect ide → Collect Setp"
    and "ide_of_set ∈ Collect Setp → Collect ide"
    and [simp]: "ide a ==> ide_of_set (set_of_ide a) = a"
    and [simp]: "Setp A ==> set_of_ide (ide_of_set A) = A"
    and "bij_betw set_of_ide (Collect ide) (Collect Setp)"
    and "bij_betw ide_of_set (Collect Setp) (Collect ide)"
    proof -
      show 1: "set_of_ide ∈ Collect ide → Collect Setp"
        using setp_set_ide set_of_ide_def by auto
      show 2: "ide_of_set ∈ Collect Setp → Collect ide"
      proof
        fix A :: "'e set"
        assume A: "A ∈ Collect Setp"
        have "arr_of ` A ⊆ Univ"
          using A arr_of_mapsto by auto
        moreover have "Setp (elem_of ` arr_of ` A)"
          using A elem_of_arr_of Setp_respects_subset by simp
        ultimately have "ide (mkIde (arr_of ` A))"
          using ide_mkIde by blast
        thus "ide_of_set A ∈ Collect ide"
          using ide_of_set_def by simp
      qed
      show 3: "∧a. ide a ==> ide_of_set (set_of_ide a) = a"
        using arr_of_img_elem_of_img ide_of_set_def mkIde_set set_of_ide_def setp_set_ide
        by presburger
      show 4: "∧A. Setp A ==> set_of_ide (ide_of_set A) = A"
      proof -
        fix A :: "'e set"
        assume A: "Setp A"
        have "elem_of ` set (mkIde (arr_of ` A)) = elem_of ` arr_of ` A"
        proof -
          have "arr_of ` A ⊆ Univ"
            using A arr_of_mapsto by blast
          moreover have "Setp (elem_of ` arr_of ` A)"
            using A by simp
          ultimately have "set (mkIde (arr_of ` A)) = arr_of ` A"
            using A set_mkIde by blast
          thus ?thesis by auto
        qed
        also have "... = A"
          using A elem_of_arr_of by force
        finally show "set_of_ide (ide_of_set A) = A"
          using ide_of_set_def set_of_ide_def by simp
      qed
      show "bij_betw set_of_ide (Collect ide) (Collect Setp)"
        using 1 2 3 4
        by (intro bij_betwI) blast+
      show "bij_betw ide_of_set (Collect Setp) (Collect ide)"
        using 1 2 3 4
        by (intro bij_betwI) blast+
    qed

    definition fun_of_arr :: "'e setcat.arr ==> 'e ==> 'e"
    where "fun_of_arr f ≡ restrict (elem_of o Fun f o arr_of) (elem_of `Dom f)"

    definition arr_of_fun :: "'e set ==> 'e set ==> ('e ==> 'e) ==> 'e setcat.arr"
    where "arr_of_fun A B F ≡ mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of)"

    lemma bij_betw_hom_fun:
    shows "fun_of_arr ∈ hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)"
    and "[Setp A; Setp B] ==> arr_of_fun A B ∈ (A → B) → hom (ide_of_set A) (ide_of_set B)"
    and "f ∈ hom a b ==> arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f"
    and "[Setp A; Setp B; F ∈ A → B; F ∈ extensional A] ==> fun_of_arr (arr_of_fun A B F) = F"
    and "[ide a; ide b] ==> bij_betw fun_of_arr (hom a b)
                             (extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b))"
    and "[Setp A; Setp B] ==>
            bij_betw (arr_of_fun A B)
                     (extensional A ∩ (A → B)) (hom (ide_of_set A) (ide_of_set B))"
    proof -
      show 1: "∧a b. fun_of_arr ∈
                        hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)"
      proof
        fix a b f
        assume f: "f ∈ hom a b"
        have Dom: "Dom f = arr_of ` set_of_ide a"
          using f set_of_ide_def
          by (metis (mono_tags, lifting) arr_dom arr_mkIde bij_betw_ide_set(3)
              ide_dom ide_of_set_def in_homE mem_Collect_eq set_mkIde)
        have Cod: "Cod f = arr_of ` set_of_ide b"
          using f set_of_ide_def
          by (metis (mono_tags, lifting) arr_cod arr_mkIde bij_betw_ide_set(3)
              ide_cod ide_of_set_def in_homE mem_Collect_eq set_mkIde)
        have "fun_of_arr f ∈ set_of_ide a → set_of_ide b"
        proof
          fix x
          assume x: "x ∈ set_of_ide a"
          have 1: "arr_of x ∈ Dom f"
            using x Dom by blast
          hence "Fun f (arr_of x) ∈ Cod f"
            using f Fun_mapsto Cod by blast
          hence "elem_of (Fun f (arr_of x)) ∈ set_of_ide b"
            using Cod by auto
          hence "restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f) x ∈ set_of_ide b"
            using 1 by force
          thus "fun_of_arr f x ∈ set_of_ide b"
            unfolding fun_of_arr_def by auto
        qed
        moreover have "fun_of_arr f ∈ extensional (set_of_ide a)"
          unfolding fun_of_arr_def
          using set_of_ide_def f by blast
        ultimately show "fun_of_arr f ∈ extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)"
          by blast
      qed
      show 2: "∧A B. [Setp A; Setp B] ==>
                        arr_of_fun A B ∈ (A → B) → hom (ide_of_set A) (ide_of_set B)"
      proof
        fix x and A B :: "'e set"
        assume A: "Setp A" and B: "Setp B"
        assume x: "x ∈ A → B"
        show "arr_of_fun A B x ∈ hom (ide_of_set A) (ide_of_set B)"
        proof
          show "«arr_of_fun A B x : ide_of_set A → ide_of_set B¬"
          proof
            show 1: "arr (arr_of_fun A B x)"
            proof -
              have "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)"
                using A arr_of_mapsto elem_of_arr_of
                by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2)
                    ide_implies_incl ide_of_set_def incl_def mem_Collect_eq)
              moreover have "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)"
                using B arr_of_mapsto elem_of_arr_of
                by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2)
                    ide_implies_incl ide_of_set_def incl_def mem_Collect_eq)
              moreover have "arr_of ∘ x ∘ elem_of ∈ arr_of ` A → arr_of ` B"
                using x by auto
              ultimately show ?thesis
                unfolding arr_of_fun_def by blast
            qed
            show "dom (arr_of_fun A B x) = ide_of_set A"
              using 1 dom_mkArr ide_of_set_def arr_of_fun_def by simp
            show "cod (arr_of_fun A B x) = ide_of_set B"
              using 1 cod_mkArr ide_of_set_def arr_of_fun_def by simp
          qed
        qed
      qed
      show 3: "∧a b f. f ∈ hom a b ==> arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f"
      proof -
        fix a b f
        assume f: "f ∈ hom a b"
        have 1: "Dom f = set a ∧ Cod f = set b"
          using f by blast
        have Dom: "Dom f ⊆ Univ ∧ Setp (elem_of ` Dom f)"
          using setp_set_ide f ide_dom by blast
        have Cod: "Cod f ⊆ Univ ∧ Setp (elem_of ` Cod f)"
          using setp_set_ide f ide_cod by blast
        have "mkArr (set a) (set b)
                    (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) =
              mkArr (Dom f) (Cod f)
                    (arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of)"
          using 1 by simp
        also have "... = mkArr (Dom f) (Cod f) (Fun f)"
        proof (intro mkArr_eqI')
          show 2: "∧x. x ∈ Dom f ==>
                         (arr_of ∘
                            restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘
                              elem_of) x =
                         Fun f x"
          proof -
            fix x
            assume x: "x ∈ Dom f"
            hence 1: "elem_of x ∈ elem_of ` Dom f"
              by blast
            have "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x =
                  arr_of (restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f) (elem_of x))"
              by auto
            also have "... = arr_of ((elem_of o Fun f o arr_of) (elem_of x))"
              using 1 by auto
            also have "... = arr_of (elem_of (Fun f (arr_of (elem_of x))))"
              by auto
            also have "... = arr_of (elem_of (Fun f x))"
              using x arr_of_elem_of ‹Dom f ⊆ Univ ∧ Setp (elem_of ` Dom f)› by auto
            also have "... = Fun f x"
              using x f Dom Cod Fun_mapsto arr_of_elem_of [of "Fun f x"] by blast
            finally show "(arr_of ∘
                             restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘
                               elem_of) x =
                          Fun f x"
              by blast
          qed
          have "arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of
                  ∈ Dom f → Cod f"
          proof
            fix x
            assume x: "x ∈ Dom f"
            have "(arr_of ∘ restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘ elem_of) x =
                  Fun f x"
              using 2 x by blast
            moreover have "... ∈ Cod f"
              using f x Fun_mapsto by blast
            ultimately show "(arr_of ∘
                                restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘
                                  elem_of) x
                               ∈ Cod f"
              by argo
          qed
          thus "arr (mkArr (Dom f) (Cod f)
                           (arr_of ∘
                              restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘
                                elem_of))"
            using Dom Cod by blast
        qed
        finally have "mkArr (set a) (set b)
                            (arr_of ∘
                               restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) ∘
                                 elem_of) = f"
          using f mkArr_Fun
          by (metis (no_types, lifting) in_homE mem_Collect_eq)
        thus "arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f"
          using 1 f
          by (metis (no_types, lifting) Cod Dom arr_of_img_elem_of_img arr_of_fun_def
              fun_of_arr_def set_of_ide_def)
      qed
      show 4: "∧A B F. [Setp A; Setp B; F ∈ A → B; F ∈ extensional A]
                          ==> fun_of_arr (arr_of_fun A B F) = F"
      proof
        fix F and A B :: "'e set"
        assume A: "Setp A" and B: "Setp B"
        assume F: "F ∈ A → B" and ext: "F ∈ extensional A"
        have 4: "arr (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of))"
        proof -
          have "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)"
            using A
            by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl
                ide_of_set_def incl_def mem_Collect_eq)
          moreover have "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)"
            using B
            by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl
                ide_of_set_def incl_def mem_Collect_eq)
          moreover have "arr_of ∘ F ∘ elem_of ∈ arr_of ` A → arr_of ` B"
            using F by auto
          ultimately show ?thesis by blast
        qed
        show "∧x. fun_of_arr (arr_of_fun A B F) x = F x"
        proof -
          fix x
          have "fun_of_arr (arr_of_fun A B F) x =
                restrict (elem_of ∘
                            Fun (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) ∘
                              arr_of) A x"
          proof -
            have "elem_of ` Dom (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) = A"
              using A 4 elem_of_arr_of dom_mkArr set_of_ide_def bij_betw_ide_set(4) ide_of_set_def
              by auto
            thus ?thesis
              using arr_of_fun_def fun_of_arr_def by auto
          qed
          also have "... = F x"
          proof (cases "x ∈ A")
            show "x ∉ A ==> ?thesis"
              using ext extensional_arb by fastforce
            assume x: "x ∈ A"
            show "restrict
                    (elem_of ∘
                       Fun (mkArr (arr_of ` A) (arr_of ` B) (arr_of ∘ F ∘ elem_of)) ∘
                         arr_of) A x =
                  F x"
              using x 4 Fun_mkArr by simp
          qed
          finally show "fun_of_arr (arr_of_fun A B F) x = F x"
            by blast
        qed
      qed
      show "[Setp A; Setp B] ==>
               bij_betw (arr_of_fun A B) (extensional A ∩ (A → B))
                        (hom (ide_of_set A) (ide_of_set B))"
      proof -
        assume A: "Setp A" and B: "Setp B"
        have "ide (ide_of_set A) ∧ ide (ide_of_set B)"
          using A B bij_betw_ide_set(2) by auto
        have "set_of_ide (ide_of_set A) = A ∧ set_of_ide (ide_of_set B) = B"
          using A B by simp
        show ?thesis
          using A B 1 [of "ide_of_set A" "ide_of_set B"] 2 3 4
          apply (intro bij_betwI)
             apply auto
           apply blast
          by fastforce
      qed
      show "[ide a; ide b] ==> bij_betw fun_of_arr (hom a b)
                                (extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b))"
      proof (intro bij_betwI)
        assume a: "ide a" and b: "ide b"
        show "fun_of_arr ∈ hom a b → extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b)"
          using 1 by blast
        show "arr_of_fun (set_of_ide a) (set_of_ide b) ∈
               extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b) → hom a b"
          using a b 2 [of "set_of_ide a" "set_of_ide b"] setp_set_ide set_of_ide_def
                bij_betw_ide_set(3)
          by auto
        show "∧f. f ∈ hom a b ==> arr_of_fun (set_of_ide a) (set_of_ide b) (fun_of_arr f) = f"
          using a b 3 by blast
        show "∧F. F ∈ extensional (set_of_ide a) ∩ (set_of_ide a → set_of_ide b) ==>
                    fun_of_arr (arr_of_fun (set_of_ide a) (set_of_ide b) F) = F"
          using a b 4 [of "set_of_ide a" "set_of_ide b"]
          by (metis (no_types, lifting) IntE set_of_ide_def setp_set_ide)
      qed
    qed

    lemma fun_of_arr_ide:
    assumes "ide a"
    shows "fun_of_arr a = restrict id (elem_of ` Dom a)"
    proof
      fix x
      show "fun_of_arr a x = restrict id (elem_of ` Dom a) x"
      proof (cases "x ∈ elem_of ` Dom a")
        show "x ∉ elem_of ` Dom a ==> ?thesis"
          using fun_of_arr_def extensional_arb by auto
        assume x: "x ∈ elem_of ` Dom a"
        have "fun_of_arr a x = restrict (elem_of ∘ Fun a ∘ arr_of) (elem_of ` Dom a) x"
          using x fun_of_arr_def by simp
        also have "... = elem_of (Fun a (arr_of x))"
          using x by auto
        also have "... = elem_of ((λx∈set a. x) (arr_of x))"
          using assms x Fun_ide by auto
        also have "... = elem_of (arr_of x)"
        proof -
          have "x ∈ elem_of ` set a"
            using assms x ideD(2) by force
          hence "arr_of x ∈ set a"
            by (metis (mono_tags, lifting) arr_of_img_elem_of_img assms image_eqI setp_set_ide)
          thus ?thesis by simp
        qed
        also have "... = x"
          by simp
        also have "... = restrict id (elem_of ` Dom a) x"
          using x by auto
        finally show ?thesis by blast
      qed
    qed

    lemma arr_of_fun_id:
    assumes "Setp A"
    shows "arr_of_fun A A (restrict id A) = ide_of_set A"
    proof -
      have A: "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)"
        using assms elem_of_arr_of
        by (metis (no_types, lifting) PiE arr_mkIde bij_betw_ide_set(2) ide_implies_incl
            ide_of_set_def incl_def mem_Collect_eq)
      have "arr_of_fun A A (restrict id A) =
            mkArr (arr_of ` A) (arr_of ` A) (arr_of ∘ restrict id A ∘ elem_of)"
        unfolding arr_of_fun_def by simp
      also have "... = mkArr (arr_of ` A) (arr_of ` A) (λx. x)"
        using A arr_mkArr
        by (intro mkArr_eqI') auto
      also have "... = ide_of_set A"
        using A ide_of_set_def mkIde_as_mkArr by simp
      finally show ?thesis by blast
    qed

    lemma fun_of_arr_comp:
    assumes "f ∈ hom a b" and "g ∈ hom b c"
    shows "fun_of_arr (comp g f) = restrict (fun_of_arr g ∘ fun_of_arr f) (set_of_ide a)"
    proof -
      have 1: "seq g f"
        using assms by blast
      have "fun_of_arr (comp g f) =
            restrict (elem_of ∘ Fun (comp g f) ∘ arr_of) (elem_of ` Dom (comp g f))"
        unfolding fun_of_arr_def by blast
      also have "... = restrict (elem_of ∘ Fun (comp g f) ∘ arr_of) (elem_of ` Dom f)"
        using assms dom_comp seqI' by auto
      also have "... = restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of)
                                (elem_of ` Dom f)"
        using 1 Fun_comp by auto
      also have "... = restrict (restrict (elem_of o Fun g o arr_of) (elem_of ` Dom g) ∘
                                   restrict (elem_of o Fun f o arr_of) (elem_of ` Dom f))
                                (elem_of ` Dom f)"
      proof
        fix x
        show "restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of) (elem_of ` Dom f) x =
              restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘
                          restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f))
                       (elem_of ` Dom f) x"
        proof (cases "x ∈ elem_of ` Dom f")
          show "x ∉ elem_of ` Dom f ==> ?thesis"
            by auto
          assume x: "x ∈ elem_of ` Dom f"
          have 2: "arr_of x ∈ Dom f"
          proof -
            have "arr_of x ∈ arr_of ` elem_of ` Dom f"
              using x by simp
            thus ?thesis
              by (metis (no_types, lifting) 1 arr_of_img_elem_of_img ide_dom seqE setp_set_ide)
          qed
          have 3: "Dom g = Cod f"
            using assms by fastforce
          have "restrict (elem_of ∘ restrict (Fun g ∘ Fun f) (Dom f) ∘ arr_of) (elem_of ` Dom f) x =
                elem_of (Fun g (Fun f (arr_of x)))"
            using x 2 by simp
          also have "... = restrict
                             (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘
                                restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f))
                             (elem_of ` Dom f) x"
          proof -
            have "restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘
                              restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f))
                           (elem_of ` Dom f) x =
                  elem_of (Fun g (Fun f (arr_of x)))"
            proof -
              have "restrict (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) ∘
                                restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f))
                             (elem_of ` Dom f) x =
                    (restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g) o
                       restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f)) x"
                using 2 by force
              also have "... = restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g)
                                 (restrict (elem_of ∘ Fun f ∘ arr_of) (elem_of ` Dom f) x)"
                by simp
              also have "... = restrict (elem_of ∘ Fun g ∘ arr_of) (elem_of ` Dom g)
                                 (elem_of (Fun f (arr_of x)))"
                using 2 by force
              also have "... = (elem_of o Fun g o arr_of) (elem_of (Fun f (arr_of x)))"
              proof -
                have "elem_of (Fun f (arr_of x)) ∈ elem_of ` Dom g"
                  using assms 2 3 Fun_mapsto [of f] by blast
                thus ?thesis by simp
              qed
              also have "... = elem_of (Fun g (arr_of (elem_of (Fun f (arr_of x)))))"
                by simp
              also have "... = elem_of (Fun g (Fun f (arr_of x)))"
              proof -
                have "Fun f (arr_of x) ∈ Univ"
                  using assms 2 setp_set_ide ide_cod Fun_mapsto by blast
                thus ?thesis
                  using 2 by simp
              qed
              finally show ?thesis by blast
            qed
            thus ?thesis by simp
          qed
          finally show ?thesis by blast
        qed
      qed
      also have "... = restrict (fun_of_arr g o fun_of_arr f) (elem_of ` Dom f)"
        unfolding fun_of_arr_def by blast
      finally show ?thesis
        unfolding set_of_ide_def
        using assms by blast
    qed

    lemma arr_of_fun_comp:
    assumes "Setp A" and "Setp B" and "Setp C"
    and "F ∈ extensional A ∩ (A → B)" and "G ∈ extensional B ∩ (B → C)"
    shows "arr_of_fun A C (G o F) = comp (arr_of_fun B C G) (arr_of_fun A B F)"
    proof -
      have A: "arr_of ` A ⊆ Univ ∧ Setp (elem_of ` arr_of ` A)"
        using assms elem_of_arr_of
        by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2)
            ide_implies_incl ide_of_set_def incl_def mem_Collect_eq)
      have B: "arr_of ` B ⊆ Univ ∧ Setp (elem_of ` arr_of ` B)"
        using assms elem_of_arr_of
        by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2)
            ide_implies_incl ide_of_set_def incl_def mem_Collect_eq)
      have C: "arr_of ` C ⊆ Univ ∧ Setp (elem_of ` arr_of ` C)"
        using assms elem_of_arr_of
        by (metis (no_types, lifting) Pi_iff arr_mkIde bij_betw_ide_set(2)
            ide_implies_incl ide_of_set_def incl_def mem_Collect_eq)
      have "arr_of_fun A C (G o F) = mkArr (arr_of ` A) (arr_of ` C) (arr_of ∘ (G ∘ F) ∘ elem_of)"
        unfolding arr_of_fun_def by simp
      also have "... = mkArr (arr_of ` A) (arr_of ` C)
                             ((arr_of ∘ G ∘ elem_of) o (arr_of o F ∘ elem_of))"
      proof (intro mkArr_eqI')
        show "arr (mkArr (arr_of ` A) (arr_of ` C) (arr_of ∘ (G ∘ F) ∘ elem_of))"
        proof -
          have "arr_of ∘ (G ∘ F) ∘ elem_of ∈ arr_of ` A → arr_of ` C"
            using assms by force
          thus ?thesis
            using A B C by blast
        qed
        show "∧x. x ∈ arr_of ` A ==>
                    (arr_of ∘ (G ∘ F) ∘ elem_of) x =
                    ((arr_of ∘ G ∘ elem_of) o (arr_of o F ∘ elem_of)) x"
          by simp
      qed
      also have "... = comp (mkArr (arr_of ` B) (arr_of ` C) (arr_of ∘ G ∘ elem_of))
                            (mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of))"
      proof -
        have "arr (mkArr (arr_of ` B) (arr_of ` C) (arr_of ∘ G ∘ elem_of))"
          using assms B C elem_of_arr_of by fastforce
        moreover have "arr (mkArr (arr_of ` A) (arr_of ` B) (arr_of o F o elem_of))"
          using assms A B elem_of_arr_of by fastforce
        ultimately show ?thesis
          using comp_mkArr by auto
      qed
      also have "... = comp (arr_of_fun B C G) (arr_of_fun A B F)"
        using arr_of_fun_def by presburger
      finally show ?thesis by blast
    qed

  end

  text‹
 When there is no restriction on the sets that determine objects, the resulting set category
 is replete. This is the normal use case, which we want to streamline as much as possible,
 so it is useful to introduce a special locale for this purpose.
 ›

  locale replete_setcat =
  fixes elem_type :: "'e itself"
  begin

    interpretation SC: setcat elem_type ‹λ_. True›
      by unfold_locales blast

    definition comp
    where "comp ≡ SC.comp"

    definition arr_of
    where "arr_of ≡ SC.arr_of"

    definition elem_of
    where "elem_of ≡ SC.elem_of"

    sublocale replete_set_category comp
      unfolding comp_def
      using SC.is_set_category replete_set_category_def set_category_def by auto

    lemma is_replete_set_category:
    shows "replete_set_category comp"
      ..

    lemma is_set_category_RSC:
    shows "set_category comp (λA. A ⊆ Univ)"
      using is_set_category by blast

    sublocale concrete_set_category comp setp UNIV arr_of
      using SC.is_concrete_set_category comp_def SC.set_img_Collect_ide_iff arr_of_def
      by auto

    lemma is_concrete_set_category:
    shows "concrete_set_category comp setp UNIV arr_of"
      ..

    lemma bij_arr_of:
    shows "bij_betw arr_of UNIV Univ"
      using SC.bij_arr_of comp_def arr_of_def by presburger

    lemma bij_elem_of:
    shows "bij_betw elem_of Univ UNIV"
      using SC.bij_elem_of comp_def elem_of_def by auto

  end
(*
  interpretation RepleteSetCat: replete_setcat undefined .
 *)
end