Theory HF_SetCat

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

chapter "The Category of Hereditarily Finite Sets"

theory HF_SetCat
imports CategoryWithFiniteLimits CartesianClosedCategory HereditarilyFinite.HF
begin

  text‹
    This theory constructs a category whose objects are in bijective correspondence with
    the hereditarily finite sets and whose arrows correspond to the functions between such
    sets.  We show that this category is cartesian closed and has finite limits.
    Note that up to this point we have not constructed any other interpretation for the
    @{locale cartesian_closed_category} locale, but it is important to have one to ensure
    that the locale assumptions are consistent.
  ›

  section "Preliminaries"

  text‹
    We begin with some preliminary definitions and facts about hereditarily finite sets,
    which are better targeted toward what we are trying to do here than what already exists
    in @{theory HereditarilyFinite.HF}.
  ›

  text‹
    The following defines when a hereditarily finite set F› represents a function from
    a hereditarily finite set B› to a hereditarily finite set C›.  Specifically, F›
    must be a relation from B› to C›, whose domain is B›, whose range is contained in C›,
    and which is single-valued on its domain.
  ›

  definition hfun
  where "hfun B C F  F  B * C  hfunction F  hdomain F = B  hrange F  C"

  lemma hfunI [intro]:
  assumes "F  A * B"
  and "X. X  A  ∃!Y. X, Y  F"
  and "X Y. X, Y  F  Y  B"
  shows "hfun A B F"
    unfolding hfun_def
    using assms hfunction_def hrelation_def is_hpair_def hrange_def hconverse_def hdomain_def
    apply (intro conjI)
    apply auto
    by fast

  lemma hfunE [elim]:
  assumes "hfun B C F"
  and "(Y. Y  B  (∃!Z. Y, Z  F)  (Z. Y, Z  F  Z  C))  T"
  shows T
  proof -
    have "Y. Y  B  (∃!Z. Y, Z  F)  (Z. Y, Z  F  Z  C)"
    proof (intro allI impI conjI)
      fix Y
      assume Y: "Y  B"
      show "∃!Z. Y, Z  F"
      proof -
        have "Z. Y, Z  F"
          using assms Y hfun_def hdomain_def by auto
        moreover have "Z Z'.  Y, Z  F; Y, Z'  F   Z = Z'"
          using assms hfun_def hfunction_def by simp
        ultimately show ?thesis by blast
      qed
      show "Z. Y, Z  F  Z  C"
        using assms Y hfun_def by auto
    qed
    thus ?thesis
      using assms(2) by simp
  qed

  text‹
    The hereditarily finite set hexp B C› represents the collection of all functions
    from B› to C›.
  ›

  definition hexp
  where "hexp B C = F  HPow (B * C). hfun B C F"

  lemma hfun_in_hexp:
  assumes "hfun B C F"
  shows "F  hexp B C"
    using assms by (simp add: hexp_def hfun_def)

  text‹
    The function happ› applies a function F› from B› to C› to an element of B›,
    yielding an element of C›.
  ›

  abbreviation happ
  where "happ  app"

  lemma happ_mapsto:
  assumes "F  hexp B C" and "Y  B"
  shows "happ F Y  C" and "happ F Y  hrange F"
  proof -
    show "happ F Y  C"
      using assms app_def hexp_def app_equality hdomain_def hfun_def by auto
    show "happ F Y  hrange F"
    proof -
      have "Y, happ F Y  F"
        using assms app_def hexp_def app_equality hdomain_def hfun_def by auto
      thus ?thesis
        using hdomain_def hrange_def hconverse_def by auto
    qed
  qed

  lemma happ_expansion:
  assumes "hfun B C F"
  shows "F = XY  B * C. hsnd XY = happ F (hfst XY)"
  proof
    fix XY
    show "XY  F  XY  XY  B * C. hsnd XY = happ F (hfst XY)"
    proof
      show "XY  F  XY  XY  B * C. hsnd XY = happ F (hfst XY)"
      proof -
        assume XY: "XY  F"
        have "XY  B * C"
          using assms XY hfun_def by auto
        moreover have "hsnd XY = happ F (hfst XY)"
          using assms XY hfunE app_def [of F "hfst XY"] the1_equality [of "λy. hfst XY, y  F"]
                calculation
          by auto
        ultimately show "XY  XY  B * C. hsnd XY = happ F (hfst XY)" by simp
      qed
      show "XY  XY  B * C. hsnd XY = happ F (hfst XY)  XY  F"
      proof -
        assume XY: "XY  XY  B * C. hsnd XY = happ F (hfst XY)"
        show "XY  F"
          using assms XY app_def [of F "hfst XY"] the1_equality [of "λy. hfst XY, y  F"]
          by fastforce
      qed
    qed
  qed

  text‹
    Function hlam› takes a function F› from A * B› to C› to a function hlam F›
    from A› to hexp B C›.
  ›

  definition hlam
  where "hlam A B C F =
         XG  A * hexp B C.
            YZ. YZ  hsnd XG  is_hpair YZ  hfst XG, hfst YZ, hsnd YZ  F"

  lemma hfun_hlam:
  assumes "hfun (A * B) C F"
  shows "hfun A (hexp B C) (hlam A B C F)"
  proof
    show "hlam A B C F  A * hexp B C"
      using assms hlam_def by auto
    show "X. X  A  ∃!Y. X, Y  hlam A B C F"
    proof
      fix X
      assume X: "X  A"
      let ?G = "YZ  B * C. X, hfst YZ, hsnd YZ  F"
      have 1: "?G  hexp B C"
        using assms X hexp_def by fastforce
      show "X, ?G  hlam A B C F"
        using assms X 1 is_hpair_def hfun_def hlam_def by auto
      fix Y
      assume XY: "X, Y  hlam A B C F"
      show "Y = ?G"
        using assms X XY hlam_def hexp_def by fastforce
    qed
    show "X Y. X, Y  hlam A B C F  Y  hexp B C"
      using assms hlam_def hexp_def by simp
  qed

  lemma happ_hlam:
  assumes "X  A" and "hfun (A * B) C F"
  shows "∃!G. X, G  hlam A B C F"
  and "happ (hlam A B C F) X = (THE G. X, G  hlam A B C F)"
  and "happ (hlam A B C F) X = yz  B * C. X, hfst yz, hsnd yz  F"
  and "Y  B  happ (happ (hlam A B C F) X) Y = happ F X, Y"
  proof -
    show 1: "∃!G. X, G  hlam A B C F"
      using assms(1,2) hfun_hlam hfunE
      by (metis (full_types))
    show 2: "happ (hlam A B C F) X = (THE G. X, G  hlam A B C F)"
      using assms app_def by simp
    show "happ (happ (hlam A B C F) X) Y = happ F X, Y"
    proof -
      have 3: "X, happ (hlam A B C F) X  hlam A B C F"
        using assms(1) 1 2 theI' [of "λG. X, G  hlam A B C F"] by simp
      hence "∃!Z. happ (happ (hlam A B C F) X) = Z"
        by simp
      moreover have "happ (happ (hlam A B C F) X) Y = happ F X, Y"
        using assms(1-2) 3 hlam_def is_hpair_def app_def by simp
      ultimately show ?thesis by simp
    qed
    show "happ (hlam A B C F) X = YZ  B * C. X, hfst YZ, hsnd YZ  F"
    proof -
      let ?G = "YZ  B * C. X, hfst YZ, hsnd YZ  F"
      have 4: "hfun B C ?G"
      proof
        show "YZ  B * C. X, hfst YZ, hsnd YZ  F  B * C"
          using assms by auto
        show "Y. Y  B  ∃!Z. Y, Z  YZ  B * C. X, hfst YZ, hsnd YZ  F"
        proof -
          fix Y
          assume Y: "Y  B"
          have XY: "X, Y  A * B"
            using assms Y by simp
          hence 1: "∃!Z. X, Y, Z  F"
            using assms XY hfunE [of "A * B" C F] by metis
          obtain Z where Z: "X, Y, Z  F"
            using 1 by auto
          have "Z. Y, Z  YZ  B * C. X, hfst YZ, hsnd YZ  F"
          proof -
            have "Y, Z  B * C"
              using assms Y Z by blast
            moreover have "X, hfst Y, Z, hsnd Y, Z  F"
              using assms Y Z by simp
            ultimately show ?thesis by auto
          qed
          moreover have "Z Z'. Y, Z  YZ  B * C. X, hfst YZ, hsnd YZ  F;
                                 Y, Z'  YZ  B * C. X, hfst YZ, hsnd YZ  F  Z = Z'"
            using assms Y by auto
          ultimately show "∃!Z. Y, Z  YZ  B * C. X, hfst YZ, hsnd YZ  F"
            by auto
        qed
        show "Y Z. Y, Z  YZ  B * C. X, hfst YZ, hsnd YZ  F  Z  C"
          using assms by simp
      qed
      have "X, ?G  hlam A B C F"
      proof -
        have "X, ?G  A * hexp B C"
          using assms 4
          by (simp add: hfun_in_hexp)
        moreover have "YZ. YZ  ?G  is_hpair YZ  X, hfst YZ, hsnd YZ  F"
          using assms 1 is_hpair_def hfun_def by auto
        ultimately show ?thesis
          using assms 1 hlam_def by simp
      qed
      thus "happ (hlam A B C F) X = ?G"
        using assms 2 4 app_equality hfun_def hfun_hlam by auto
    qed
  qed

  section "Construction of the Category"

  locale hfsetcat
  begin

    text‹
      We construct the category of hereditarily finite sets and functions simply by applying
      the generic ``set category'' construction, using the hereditarily finite sets as the
      universe, and constraining the collections of such sets that determine objects of the
      category to those that are finite.
    ›

    interpretation setcat TYPE(hf) finite
      using finite_subset
      by unfold_locales blast+
    interpretation set_category comp λA. A  Collect terminal  finite (elem_of ` A)
      using is_set_category by blast

    lemma set_ide_char:
    shows "A  set ` Collect ide  A  Univ  finite A"
    proof
      assume A: "A  set ` Collect ide"
      show "A  Univ  finite A"
      proof
        show "A  Univ"
          using A setp_set' by auto
        obtain a where a: "ide a  A = set a"
          using A by blast
        have "finite (elem_of ` set a)"
          using a setp_set_ide by blast
        moreover have "inj_on elem_of (set a)"
        proof -
          have "inj_on elem_of Univ"
            using bij_elem_of bij_betw_imp_inj_on by auto
          moreover have "set a  Univ"
            using a setp_set' [of a] by blast
          ultimately show ?thesis
            using inj_on_subset by auto
        qed
        ultimately show "finite A"
          using a A finite_imageD [of elem_of "set a"] by blast
      qed
      next
      assume A: "A  Univ  finite A"
      have "ide (mkIde A)"
        using A ide_mkIde by simp
      moreover have "set (mkIde A) = A"
        using A finite_imp_setp set_mkIde by presburger
      ultimately show "A  set ` Collect ide" by blast
    qed

    lemma set_ideD:
    assumes "ide a"
    shows "set a  Univ" and "finite (set a)"
      using assms set_ide_char by auto

    lemma ide_mkIdeI [intro]:
    assumes "A  Univ" and "finite A"
    shows "ide (mkIde A)" and "set (mkIde A) = A"
      using assms ide_mkIde set_mkIde by auto

    interpretation category_with_terminal_object comp
      using terminal_unity by unfold_locales auto

    text‹
      We verify that the objects of HF are indeed in bijective correspondence with the
      hereditarily finite sets.
    ›

    definition ide_to_hf
    where "ide_to_hf a = HF (elem_of ` set a)"

    definition hf_to_ide
    where "hf_to_ide x = mkIde (arr_of ` hfset x)"

    lemma ide_to_hf_mapsto:
    shows "ide_to_hf  Collect ide  UNIV"
      by simp

    lemma hf_to_ide_mapsto:
    shows "hf_to_ide  UNIV  Collect ide"
    proof
      fix x :: hf
      have "finite (arr_of ` hfset x)"
        by simp
      moreover have "arr_of ` hfset x  Univ"
        by (metis (mono_tags, lifting) UNIV_I bij_arr_of bij_betw_def imageE image_eqI subsetI)
      ultimately have "ide (mkIde (arr_of ` hfset x))"
        using finite_imp_setp ide_mkIde by presburger
      thus "hf_to_ide x  Collect ide"
        using hf_to_ide_def by simp
    qed

    lemma hf_to_ide_ide_to_hf:
    assumes "a  Collect ide"
    shows "hf_to_ide (ide_to_hf a) = a"
    proof -
      have "hf_to_ide (ide_to_hf a) = mkIde (arr_of ` hfset (HF (elem_of ` set a)))"
        using hf_to_ide_def ide_to_hf_def by simp
      also have "... = a"
      proof -
        have "mkIde (arr_of ` hfset (HF (elem_of ` set a))) = mkIde (arr_of ` elem_of ` set a)"
        proof -
          have "finite (set a)"
            using assms set_ide_char by blast
          hence "finite (elem_of ` set a)"
            by simp
          hence "hfset (HF (elem_of ` set a)) = elem_of ` set a"
            using hfset_HF [of "elem_of ` set a"] by simp
          thus ?thesis by simp
        qed
        also have "... = a"
        proof -
          have "set a  Univ"
            using assms set_ide_char by blast
          hence "x. x  set a  arr_of (elem_of x) = x"
            using assms by auto
          hence "arr_of ` elem_of ` set a = set a"
            by force
          thus ?thesis
            using assms ide_char mkIde_set by simp
        qed
        finally show ?thesis by blast
      qed
      finally show "hf_to_ide (ide_to_hf a) = a" by blast
    qed

    lemma ide_to_hf_hf_to_ide:
    assumes "x  UNIV"
    shows "ide_to_hf (hf_to_ide x) = x"
    proof -
      have "HF (elem_of ` set (mkIde (arr_of ` hfset x))) = x"
      proof -
        have "HF (elem_of ` set (mkIde (arr_of ` hfset x))) = HF (elem_of ` arr_of ` hfset x)"
          using assms set_mkIde [of "arr_of ` hfset x"] arr_of_mapsto mkIde_def by auto
        also have "... = HF (hfset x)"
        proof -
          have "A. elem_of ` arr_of ` A = A"
            using elem_of_arr_of by force
          thus ?thesis by metis
        qed
        also have "... = x" by simp
        finally show ?thesis by blast
      qed
      thus ?thesis
        using assms ide_to_hf_def hf_to_ide_def by simp
    qed

    lemma bij_betw_ide_hf_set:
    shows "bij_betw ide_to_hf (Collect ide) (UNIV :: hf set)"
      using ide_to_hf_mapsto hf_to_ide_mapsto ide_to_hf_hf_to_ide hf_to_ide_ide_to_hf
      by (intro bij_betwI) auto

    lemma ide_implies_finite_set:
    assumes "ide a"
    shows "finite (set a)" and "finite (hom unity a)"
    proof -
      show 1: "finite (set a)"
        using assms set_ide_char by blast
      show "finite (hom unity a)"
        using assms 1 bij_betw_points_and_set finite_imageD inj_img set_def by auto
    qed

    text‹
      We establish the connection between the membership relation defined for hereditarily
      finite sets and the corresponding membership relation associated with the set category.
    ›

    lemma arr_of_membI [intro]:
    assumes "x  ide_to_hf a"
    shows "arr_of x  set a"
    proof -
      let ?X = "inv_into (set a) elem_of x"
      have "x = elem_of ?X  ?X  set a"
        using assms
        by (simp add: f_inv_into_f ide_to_hf_def inv_into_into)
      thus ?thesis
        by (metis (no_types, lifting) arr_of_elem_of elem_set_implies_incl_in
            elem_set_implies_set_eq_singleton incl_in_def mem_Collect_eq terminal_char2)
    qed

    lemma elem_of_membI [intro]:
    assumes "ide a" and "x  set a"
    shows "elem_of x  ide_to_hf a"
    proof -
      have "finite (elem_of ` set a)"
        using assms ide_implies_finite_set [of a] by simp
      hence "elem_of x  hfset (ide_to_hf a)"
        using assms ide_to_hf_def hfset_HF [of "elem_of ` set a"] by simp
      thus ?thesis
        using hmem_def by blast
    qed

    text‹
      We show that each hom-set hom a b› is in bijective correspondence with
      the elements of the hereditarily finite set hfun (ide_to_hf a) (ide_to_hf b)›.
    ›

    definition arr_to_hfun
    where "arr_to_hfun f = XY  ide_to_hf (dom f) * ide_to_hf (cod f).
                              hsnd XY = elem_of (Fun f (arr_of (hfst XY)))"

    definition hfun_to_arr
    where "hfun_to_arr B C F =
           mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x)))"

    lemma hfun_arr_to_hfun:
    assumes "arr f"
    shows "hfun (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f)"
    proof
      show "arr_to_hfun f  ide_to_hf (dom f) * ide_to_hf (cod f)"
        using assms arr_to_hfun_def by auto
      show "X. X  ide_to_hf (dom f)  ∃!Y. X, Y  arr_to_hfun f"
      proof
        fix X
        assume X: "X  ide_to_hf (dom f)"
        show "X, elem_of (Fun f (arr_of X))  arr_to_hfun f"
        proof -
          have "X, elem_of (Fun f (arr_of X))  XY  ide_to_hf (dom f) * ide_to_hf (cod f).
                     hsnd XY = elem_of (Fun f (arr_of (hfst XY)))"
          proof -
            have "hsnd X, elem_of (Fun f (arr_of X)) =
                  elem_of (Fun f (arr_of (hfst X, elem_of (Fun f (arr_of X)))))"
              using assms X by simp
            moreover have "X, elem_of (Fun f (arr_of X))  ide_to_hf (dom f) * ide_to_hf (cod f)"
            proof -
              have "elem_of (Fun f (arr_of X))  ide_to_hf (cod f)"
              proof (intro elem_of_membI)
                show "ide (cod f)"
                  using assms ide_cod by simp
                show "Fun f (arr_of X)  Cod f"
                  using assms X Fun_mapsto arr_of_membI by auto
              qed
              thus ?thesis
                using X by simp
            qed
            ultimately show ?thesis by simp
          qed
          thus ?thesis
            using arr_to_hfun_def by simp
        qed
        fix Y
        assume XY: "X, Y  arr_to_hfun f"
        show "Y = elem_of (Fun f (arr_of X))"
          using assms X XY arr_to_hfun_def by auto
      qed
      show "X Y. X, Y  arr_to_hfun f  Y  ide_to_hf (cod f)"
        using assms arr_to_hfun_def ide_to_hf_def
              arr_to_hfun f  ide_to_hf (dom f) * ide_to_hf (cod f)
        by blast
    qed

    lemma arr_to_hfun_in_hexp:
    assumes "arr f"
    shows "arr_to_hfun f  hexp (ide_to_hf (dom f)) (ide_to_hf (cod f))"
      using assms arr_to_hfun_def hfun_arr_to_hfun hexp_def by auto

    lemma hfun_to_arr_in_hom:
    assumes "hfun B C F"
    shows "«hfun_to_arr B C F : hf_to_ide B  hf_to_ide C»"
    proof
      let ?f = "mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x)))"
      have 0: "arr ?f"
      proof -
        have "arr_of ` hfset B  Univ  arr_of ` hfset C  Univ"
          using arr_of_mapsto by auto
        moreover have "(λx. arr_of (happ F (elem_of x)))  arr_of ` hfset B  arr_of ` hfset C"
        proof
          fix x
          assume x: "x  arr_of ` hfset B"
          have "happ F (elem_of x)  hfset C"
            using assms x happ_mapsto hfun_in_hexp
            by (metis elem_of_arr_of HF_hfset finite_hfset hmem_HF_iff imageE)
          thus "arr_of (happ F (elem_of x))  arr_of ` hfset C"
            by simp
        qed
        ultimately show ?thesis
          using arr_mkArr
          by (meson finite_hfset finite_iff_ordLess_natLeq finite_imageI)
      qed
      show 1: "arr (hfun_to_arr B C F)"
        using 0 hfun_to_arr_def by simp
      show "dom (hfun_to_arr B C F) = hf_to_ide B"
        using 1 hfun_to_arr_def hf_to_ide_def dom_mkArr by auto
      show "cod (hfun_to_arr B C F) = hf_to_ide C"
        using 1 hfun_to_arr_def hf_to_ide_def cod_mkArr by auto
    qed

    text‹
      The comprehension notation from @{theory HereditarilyFinite.HF} interferes in an
      unfortunate way with the restriction notation from @{theory "HOL-Library.FuncSet"},
      making it impossible to use both in the present context.
    ›

    lemma Fun_char:
    assumes "arr f"
    shows "Fun f = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f)"
    proof
      fix x
      show "Fun f x = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x"
      proof (cases "x  Dom f")
        show "x  Dom f  ?thesis"
          using assms Fun_mapsto Fun_def restrict_apply by simp
        show "x  Dom f  ?thesis"
        proof -
          assume x: "x  Dom f"
          have 1: "hfun (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f)"
            using assms app_def arr_to_hfun_def hfun_arr_to_hfun
                  the1_equality [of "λy. elem_of x, y  arr_to_hfun f" "elem_of (Fun f x)"]
            by simp
          have 2: "∃!Y. elem_of x, Y  arr_to_hfun f"
            using assms x 1 hfunE elem_of_membI ide_dom
            by (metis (no_types, lifting))
          have "Fun f x = arr_of (elem_of (Fun f x))"
          proof -
            have "Fun f x  Univ"
              using assms x ide_cod Fun_mapsto [of f] set_ide_char by blast
            thus ?thesis
              using arr_of_elem_of by simp
          qed
          also have "... = arr_of (happ (arr_to_hfun f) (elem_of x))"
          proof -
            have "elem_of x, elem_of (Fun f x)  arr_to_hfun f"
            proof -
              have "elem_of x, elem_of (Fun f x)  ide_to_hf (dom f) * ide_to_hf (cod f)"
                using assms x ide_dom ide_cod Fun_mapsto by fast
              moreover have "elem_of (Fun f x) = elem_of (Fun f (arr_of (elem_of x)))"
                by (metis (no_types, lifting) arr_of_elem_of setp_set_ide assms ide_dom subsetD x)
              ultimately show ?thesis
                using arr_to_hfun_def by auto
            qed
            moreover have "elem_of x, happ (arr_to_hfun f) (elem_of x)  arr_to_hfun f"
              using assms x 1 2 app_equality hfun_def by blast
            ultimately show ?thesis
              using 2 by fastforce
          qed
          also have "... = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x"
            using assms x ide_dom by auto
          finally show ?thesis by simp
        qed
      qed
    qed

    lemma Fun_hfun_to_arr:
    assumes "hfun B C F"
    shows "Fun (hfun_to_arr B C F) = restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B)"
    proof -
      have "arr (hfun_to_arr B C F)"
        using assms hfun_to_arr_in_hom by blast
      hence "arr (mkArr (arr_of ` hfset B) (arr_of ` hfset C) (λx. arr_of (happ F (elem_of x))))"
        using hfun_to_arr_def by simp
      thus ?thesis
        using assms hfun_to_arr_def Fun_mkArr by simp
    qed

    lemma arr_of_img_hfset_ide_to_hf:
    assumes "ide a"
    shows "arr_of ` hfset (ide_to_hf a) = set a"
    proof -
      have "arr_of ` hfset (ide_to_hf a) = arr_of ` hfset (HF (elem_of ` set a))"
        using ide_to_hf_def by simp
      also have "... = arr_of ` elem_of ` set a"
        using assms ide_implies_finite_set(1) ide_char by auto
      also have "... = set a"
      proof -
        have "x. x  set a  arr_of (elem_of x) = x"
          using assms ide_char arr_of_elem_of setp_set_ide by blast
        thus ?thesis by force
      qed
      finally show ?thesis by blast
    qed

    lemma hfun_to_arr_arr_to_hfun:
    assumes "arr f"
    shows "hfun_to_arr (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f) = f"
    proof -
      have 0: "hfun_to_arr (ide_to_hf (dom f)) (ide_to_hf (cod f)) (arr_to_hfun f) =
               mkArr (arr_of ` hfset (ide_to_hf (dom f))) (arr_of ` hfset (ide_to_hf (cod f)))
                     (λx. arr_of (happ (arr_to_hfun f) (elem_of x)))"
        unfolding hfun_to_arr_def by blast
      also have "... = mkArr (Dom f) (Cod f)
                             (restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f))"
      proof (intro mkArr_eqI)
        show 1: "arr_of ` hfset (ide_to_hf (dom f)) = Dom f"
          using assms arr_of_img_hfset_ide_to_hf ide_dom by simp
        show 2: "arr_of ` hfset (ide_to_hf (cod f)) = Cod f"
          using assms arr_of_img_hfset_ide_to_hf ide_cod by simp
        show "arr (mkArr (arr_of ` hfset (ide_to_hf (dom f))) (arr_of ` hfset (ide_to_hf (cod f)))
                         (λx. arr_of (happ (arr_to_hfun f) (elem_of x))))"
          using 0 1 2
          by (metis (no_types, lifting) arrI assms hfun_arr_to_hfun hfun_to_arr_in_hom)
        show "x. x  arr_of ` hfset (ide_to_hf (dom f)) 
                     arr_of (happ (arr_to_hfun f) (elem_of x)) =
                     restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f) x"
          using assms 1 by simp
      qed
      also have "... = mkArr (Dom f) (Cod f) (Fun f)"
        using assms Fun_char mkArr_eqI by simp
      also have "... = f"
        using assms mkArr_Fun by blast
      finally show ?thesis by simp
    qed

    lemma arr_to_hfun_hfun_to_arr:
    assumes "hfun B C F"
    shows "arr_to_hfun (hfun_to_arr B C F) = F"
    proof -
      have "arr_to_hfun (hfun_to_arr B C F) =
            XY  ide_to_hf (dom (hfun_to_arr B C F)) * ide_to_hf (cod (hfun_to_arr B C F)).
               hsnd XY = elem_of (Fun (hfun_to_arr B C F) (arr_of (hfst XY)))"
        unfolding arr_to_hfun_def by blast
      also have
          "... = XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)).
                    hsnd XY = elem_of (Fun (hfun_to_arr B C F) (arr_of (hfst XY)))"
        using assms hfun_to_arr_in_hom [of B C F] hf_to_ide_def
        by (metis (no_types, lifting) in_homE)
      also have
          "... = XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)).
                    hsnd XY = elem_of (restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B)
                                   (arr_of (hfst XY)))"
        using assms Fun_hfun_to_arr by simp
      also have
          "... = XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)).
                    hsnd XY = elem_of (arr_of (happ F (elem_of (arr_of (hfst XY)))))"
      proof -
        have
          1: "XY. XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C))
                      arr_of (hfst XY)  arr_of ` hfset B"
        proof -
          fix XY
          assume
            XY: "XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C))"
          have "hfst XY  ide_to_hf (mkIde (arr_of ` hfset B))"
            using XY by auto
          thus "arr_of (hfst XY)  arr_of ` hfset B"
            using assms arr_of_membI [of "hfst XY" "mkIde (arr_of ` hfset B)"] set_mkIde
            by (metis (mono_tags, lifting) arrI arr_mkArr hfun_to_arr_def hfun_to_arr_in_hom)
        qed
        show ?thesis
        proof -
          have
            "XY. (XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)) 
                     hsnd XY = elem_of (restrict (λx. arr_of (happ F (elem_of x))) (arr_of ` hfset B)
                                       (arr_of (hfst XY))))
                   
                   (XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)) 
                     hsnd XY = elem_of (arr_of (happ F (elem_of (arr_of (hfst XY))))))"
            using 1 by auto
          thus ?thesis by blast
        qed
      qed
      also have
        "... = XY  ide_to_hf (mkIde (arr_of ` hfset B)) * ide_to_hf (mkIde (arr_of ` hfset C)).
                  hsnd XY = happ F (hfst XY)"
        by simp
      also have "... = XY  B * C. hsnd XY = happ F (hfst XY)"
        using assms hf_to_ide_def ide_to_hf_hf_to_ide by force
      also have "... = F"
        using assms happ_expansion by simp
      finally show ?thesis by simp
    qed

    lemma bij_betw_hom_hfun:
    assumes "ide a" and "ide b"
    shows "bij_betw arr_to_hfun (hom a b) {F. hfun (ide_to_hf a) (ide_to_hf b) F}"
    proof (intro bij_betwI)
      show "arr_to_hfun  hom a b  {F. hfun (ide_to_hf a) (ide_to_hf b) F}"
        using assms arr_to_hfun_in_hexp hexp_def hfun_arr_to_hfun by blast
      show "hfun_to_arr (ide_to_hf a) (ide_to_hf b)
               {F. hfun (ide_to_hf a) (ide_to_hf b) F}  hom a b"
        using assms hfun_to_arr_in_hom
        by (metis (no_types, lifting) Pi_I hf_to_ide_ide_to_hf mem_Collect_eq)
      show "x. x  hom a b  hfun_to_arr (ide_to_hf a) (ide_to_hf b) (arr_to_hfun x) = x"
        using assms hfun_to_arr_arr_to_hfun by blast
      show "y. y  {F. hfun (ide_to_hf a) (ide_to_hf b) F} 
                  arr_to_hfun (hfun_to_arr (ide_to_hf a) (ide_to_hf b) y) = y"
        using assms arr_to_hfun_hfun_to_arr by simp
    qed

    text‹
      We next relate composition of arrows in the category to the corresponding operation
      on hereditarily finite sets.
    ›

    definition hcomp
    where "hcomp G F =
           XZ  hdomain F * hrange G. hsnd XZ = happ G (happ F (hfst XZ))"

    lemma hfun_hcomp:
    assumes "hfun A B F" and "hfun B C G"
    shows "hfun A C (hcomp G F)"
    proof
      show "hcomp G F  A * C"
        using assms hcomp_def hfun_def by auto
      show "X. X  A  ∃!Y. X, Y  hcomp G F"
      proof
        fix X
        assume X: "X  A"
        show "X, happ G (happ F X)  hcomp G F"
          unfolding hcomp_def
          using assms X hfunE happ_mapsto hfun_in_hexp
          by (metis (mono_tags, lifting) HCollect_iff hfst_conv hfun_def hsnd_conv timesI)
        show "X Y. X  A; X, Y  hcomp G F  Y = happ G (happ F X)"
          unfolding hcomp_def by simp
      qed
      show "X Y. X, Y  hcomp G F  Y  C"
        unfolding hcomp_def
        using assms hfunE happ_mapsto hfun_in_hexp
        by (metis HCollectE hfun_def hsubsetCE timesD2)
    qed

    lemma arr_to_hfun_comp:
    assumes "seq g f"
    shows "arr_to_hfun (comp g f) = hcomp (arr_to_hfun g) (arr_to_hfun f)"
    proof -
      have 1: "hdomain (arr_to_hfun f) = ide_to_hf (dom f)"
        using assms hfun_arr_to_hfun hfun_def by blast
      have "arr_to_hfun (comp g f) =
            XZ  ide_to_hf (dom f) * ide_to_hf (cod g).
               hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))"
        unfolding arr_to_hfun_def comp_def
        using assms by fastforce
      also have "... = XZ  hdomain (arr_to_hfun f) * hrange (arr_to_hfun g).
                          hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
      proof
        fix XZ
        have "hfst XZ  hdomain (arr_to_hfun f)
                  hsnd XZ  ide_to_hf (cod g) 
                       hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))
                      
                     hsnd XZ  hrange (arr_to_hfun g) 
                       hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
        proof
          assume XZ: "hfst XZ  hdomain (arr_to_hfun f)"
          have 2: "arr_of (hfst XZ)  Dom f"
            using XZ 1 hfsetcat.arr_of_membI by auto
          have 3: "arr_of (happ (arr_to_hfun f) (hfst XZ))  Dom g"
            using assms XZ 2
            by (metis (no_types, lifting) "1" happ_mapsto(1) hfsetcat.arr_of_membI
                arr_to_hfun_in_hexp seqE)
          have 4: "elem_of (Fun (comp g f) (arr_of (hfst XZ))) =
                   happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
          proof -
            have "elem_of (Fun (comp g f) (arr_of (hfst XZ))) =
                  elem_of (restrict (Fun g o Fun f) (Dom f) (arr_of (hfst XZ)))"
              using assms Fun_comp Fun_char by simp
            also have "... = elem_of ((Fun g o Fun f) (arr_of (hfst XZ)))"
              using XZ 2 by auto
            also have "... = elem_of (Fun g (Fun f (arr_of (hfst XZ))))"
              by simp
            also have
              "... = elem_of (Fun g (restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f)
                                           (arr_of (hfst XZ))))"
            proof -
              have "Fun f = restrict (λx. arr_of (happ (arr_to_hfun f) (elem_of x))) (Dom f)"
                using assms Fun_char [of f] by blast
              thus ?thesis by simp
            qed
            also have "... = elem_of (Fun g (arr_of (happ (arr_to_hfun f) (hfst XZ))))"
              using 2 by simp
            also have "... = elem_of (restrict (λx. arr_of (happ (arr_to_hfun g) (elem_of x))) (Dom g)
                                            (arr_of (happ (arr_to_hfun f) (hfst XZ))))"
            proof -
              have "Fun g = restrict (λx. arr_of (happ (arr_to_hfun g) (elem_of x))) (Dom g)"
                using assms Fun_char [of g] by blast
              thus ?thesis by simp
            qed
            also have "... = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
              using 3 by simp
            finally show ?thesis by blast
          qed
          have 5: "elem_of (Fun (comp g f) (arr_of (hfst XZ)))  hrange (arr_to_hfun g)"
          proof -
            have "happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))  hrange (arr_to_hfun g)"
              using assms 1 3 XZ hfun_arr_to_hfun happ_mapsto arr_to_hfun_in_hexp arr_to_hfun_def
              by (metis (no_types, lifting) seqE)
            thus ?thesis
              using XZ 4 by simp
          qed
          show "hsnd XZ  ide_to_hf (cod g) 
                  hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))
                          
                hsnd XZ  hrange (arr_to_hfun g) 
                  hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
            using XZ 4 5 by simp
          show "hsnd XZ  hrange (arr_to_hfun g) 
                  hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))
                          
                hsnd XZ  ide_to_hf (cod g) 
                  hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))"
            using assms XZ 1 4
            by (metis (no_types, lifting) arr_to_hfun_in_hexp happ_mapsto(1) seqE)
        qed
        thus "XZ  XZ  ide_to_hf (dom f) * ide_to_hf (cod g).
                      hsnd XZ = elem_of (Fun (comp g f) (arr_of (hfst XZ)))
                
              XZ  XZ  hdomain (arr_to_hfun f) * hrange (arr_to_hfun g).
                      hsnd XZ = happ (arr_to_hfun g) (happ (arr_to_hfun f) (hfst XZ))"
          using 1 is_hpair_def by auto
      qed
      also have "... = hcomp (arr_to_hfun g) (arr_to_hfun f)"
        using assms arr_to_hfun_def hcomp_def by simp
      finally show ?thesis by simp
    qed

    lemma hfun_to_arr_hcomp:
    assumes "hfun A B F" and "hfun B C G"
    shows "hfun_to_arr A C (hcomp G F) = comp (hfun_to_arr B C G) (hfun_to_arr A B F)"
    proof -
      have 1: "arr_to_hfun (hfun_to_arr A C (hcomp G F)) =
               arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F))"
      proof -
        have "arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F)) =
              hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))"
          using assms arr_to_hfun_comp hfun_to_arr_in_hom by blast
        also have "... = hcomp G F"
          using assms by (simp add: arr_to_hfun_hfun_to_arr)
        also have "... = arr_to_hfun (hfun_to_arr A C (hcomp G F))"
        proof -
          have "hfun A C (hcomp G F)"
            using assms hfun_hcomp by simp
          thus ?thesis
            by (simp add: arr_to_hfun_hfun_to_arr)
        qed
        finally show ?thesis by simp
      qed
      show ?thesis
      proof -
        have "hfun_to_arr A C (hcomp G F)  hom (hf_to_ide A) (hf_to_ide C)"
          using assms hfun_hcomp hf_to_ide_def hfun_to_arr_in_hom by auto
        moreover have "comp (hfun_to_arr B C G) (hfun_to_arr A B F)
                           hom (hf_to_ide A) (hf_to_ide C)"
          using assms hfun_to_arr_in_hom hf_to_ide_def
          by (metis (no_types, lifting) comp_in_homI mem_Collect_eq)
        moreover have "inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))"
        proof -
          have "ide (hf_to_ide A)  ide (hf_to_ide C)"
            using assms hf_to_ide_mapsto by auto
          thus ?thesis
            using bij_betw_hom_hfun [of "hf_to_ide A" "hf_to_ide C"] bij_betw_imp_inj_on
            by auto
        qed
        ultimately show ?thesis
          using 1 inj_on_def [of arr_to_hfun "hom (hf_to_ide A) (hf_to_ide C)"] by simp
      qed
    qed

    section "Binary Products"

    text‹
      The category of hereditarily finite sets has binary products,
      given by cartesian product of sets in the usual way.
    ›

    definition prod
    where "prod a b = hf_to_ide (ide_to_hf a * ide_to_hf b)"

    definition pr0
    where "pr0 a b = (if ide a  ide b then
                         mkArr (set (prod a b)) (set b) (λx. arr_of (hsnd (elem_of x)))
                      else null)"

    definition pr1
    where "pr1 a b = (if ide a  ide b then
                         mkArr (set (prod a b)) (set a) (λx. arr_of (hfst (elem_of x)))
                      else null)"

    definition tuple
    where "tuple f g = mkArr (set (dom f)) (set (prod (cod f) (cod g)))
                             (λx. arr_of (hpair (elem_of (Fun f x)) (elem_of (Fun g x))))"

    lemma ide_prod:
    assumes "ide a" and "ide b"
    shows "ide (prod a b)"
      using assms prod_def hf_to_ide_mapsto ide_to_hf_mapsto by auto

    lemma pr1_in_hom [intro]:
    assumes "ide a" and "ide b"
    shows "«pr1 a b : prod a b  a»"
    proof
      show 0: "arr (pr1 a b)"
      proof -
        have "set (prod a b)  Univ  finite (set (prod a b))"
          using assms ide_implies_finite_set(1) set_ideD(1) ide_prod by presburger
        moreover have "set a  Univ  finite (set a)"
          using assms ide_char set_ide_char by blast
        moreover have "(λx. arr_of (hfst (elem_of x)))  set (prod a b)  set a"
        proof (unfold prod_def)
          show "(λx. arr_of (hfst (elem_of x)))  set (hf_to_ide (ide_to_hf a * ide_to_hf b))  set a"
          proof
            fix x
              assume x: "x  set (hf_to_ide (ide_to_hf a * ide_to_hf b))"
              have "elem_of x  hfset (ide_to_hf a * ide_to_hf b)"
                using assms ide_char x
                by (metis (no_types, lifting) prod_def elem_of_membI HF_hfset UNIV_I hmem_HF_iff
                    ide_prod ide_to_hf_hf_to_ide)
              hence "hfst (elem_of x)  ide_to_hf a"
                by (metis HF_hfset finite_hfset hfst_conv hmem_HF_iff timesE)
              thus "arr_of (hfst (elem_of x))  set a"
                using arr_of_membI by simp
          qed
        qed
        ultimately show ?thesis
          unfolding pr1_def
          using assms arr_mkArr finite_imp_setp by presburger
      qed
      show "dom (pr1 a b) = prod a b"
        using assms 0 ide_char ide_prod dom_mkArr
        by (metis (no_types, lifting) mkIde_set pr1_def)
      show "cod (pr1 a b) = a"
        using assms 0 ide_char ide_prod cod_mkArr
        by (metis (no_types, lifting) mkIde_set pr1_def)
    qed

    lemma pr1_simps [simp]:
    assumes "ide a" and "ide b"
    shows "arr (pr1 a b)" and "dom (pr1 a b) = prod a b" and "cod (pr1 a b) = a"
      using assms pr1_in_hom by blast+

    lemma pr0_in_hom [intro]:
    assumes "ide a" and "ide b"
    shows "«pr0 a b : prod a b  b»"
    proof
      show 0: "arr (pr0 a b)"
      proof -
        have "set (prod a b)  Univ  finite (set (prod a b))"
          using setp_set_ide assms ide_implies_finite_set(1) ide_prod by presburger
        moreover have "set b  Univ  finite (set b)"
          using assms ide_char set_ide_char by blast
        moreover have "(λx. arr_of (hsnd (elem_of x)))  set (prod a b)  set b"
        proof (unfold prod_def)
          show "(λx. arr_of (hsnd (elem_of x)))  set (hf_to_ide (ide_to_hf a * ide_to_hf b))  set b"
          proof
            fix x
              assume x: "x  set (hf_to_ide (ide_to_hf a * ide_to_hf b))"
              have "elem_of x  hfset (ide_to_hf a * ide_to_hf b)"
                using assms ide_char x
                by (metis (no_types, lifting) prod_def elem_of_membI HF_hfset UNIV_I hmem_HF_iff
                    ide_prod ide_to_hf_hf_to_ide)
              hence "hsnd (elem_of x)  ide_to_hf b"
                by (metis HF_hfset finite_hfset hsnd_conv hmem_HF_iff timesE)
              thus "arr_of (hsnd (elem_of x))  set b"
                using arr_of_membI by simp
          qed
        qed
        ultimately show ?thesis
          unfolding pr0_def
          using assms arr_mkArr finite_imp_setp by presburger
      qed
      show "dom (pr0 a b) = prod a b"
        using assms 0 ide_char ide_prod dom_mkArr
        by (metis (no_types, lifting) mkIde_set pr0_def)
      show "cod (pr0 a b) = b"
        using assms 0 ide_char ide_prod cod_mkArr
        by (metis (no_types, lifting) mkIde_set pr0_def)
    qed

    lemma pr0_simps [simp]:
    assumes "ide a" and "ide b"
    shows "arr (pr0 a b)" and "dom (pr0 a b) = prod a b" and "cod (pr0 a b) = b"
      using assms pr0_in_hom by blast+

    lemma arr_of_tuple_elem_of_membI:
    assumes "span f g" and "x  Dom f"
    shows "arr_of elem_of (Fun f x), elem_of (Fun g x)  set (prod (cod f) (cod g))"
    proof -
      have "Fun f x  set (cod f)"
        using assms Fun_mapsto by blast
      moreover have "Fun g x  set (cod g)"
        using assms Fun_mapsto by auto
      ultimately have "elem_of (Fun f x), elem_of (Fun g x)
                           ide_to_hf (cod f) * ide_to_hf (cod g)"
        using assms ide_cod by auto
      moreover have "set (prod (cod f) (cod g))  Univ"
        using setp_set_ide assms(1) ide_cod ide_prod by presburger
      ultimately show ?thesis
        using prod_def arr_of_membI ide_to_hf_hf_to_ide by auto
    qed

    lemma tuple_in_hom [intro]:
    assumes "span f g"
    shows "«tuple f g : dom f  prod (cod f) (cod g)»"
    proof
      show 1: "arr (tuple f g)"
      proof -
        have "Dom f  Univ  finite (Dom f)"
          using assms set_ideD(1) ide_dom ide_implies_finite_set(1) by presburger
        moreover have "set (prod (cod f) (cod g))  Univ  finite (set (prod (cod f) (cod g)))"
          using assms set_ideD(1) ide_cod ide_prod ide_implies_finite_set(1) by presburger
        moreover have "(λx. arr_of elem_of (Fun f x), elem_of (Fun g x))
                           Dom f  set (prod (cod f) (cod g))"
          using assms arr_of_tuple_elem_of_membI by simp
        ultimately show ?thesis
          using assms ide_prod tuple_def arr_mkArr ide_dom ide_cod by simp
      qed
      show "dom (tuple f g) = dom f"
        using assms 1 dom_mkArr ide_dom mkIde_set tuple_def by auto
      show "cod (tuple f g) = prod (cod f) (cod g)"
        using assms 1 cod_mkArr ide_cod mkIde_set tuple_def ide_prod by auto
    qed

    lemma tuple_simps [simp]:
    assumes "span f g"
    shows "arr (tuple f g)" and "dom (tuple f g) = dom f"
    and "cod (tuple f g) = prod (cod f) (cod g)"
      using assms tuple_in_hom by blast+

    lemma Fun_pr1:
    assumes "ide a" and "ide b"
    shows "Fun (pr1 a b) = restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b))"
      using assms pr1_def Fun_mkArr arr_char pr1_simps(1) by presburger

    lemma Fun_pr0:
    assumes "ide a" and "ide b"
    shows "Fun (pr0 a b) = restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b))"
      using assms pr0_def Fun_mkArr arr_char pr0_simps(1) by presburger

    lemma Fun_tuple:
    assumes "span f g"
    shows "Fun (tuple f g) = restrict (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)) (Dom f)"
    proof -
      have "arr (tuple f g)"
        using assms tuple_in_hom by blast
      thus ?thesis
        using assms tuple_def Fun_mkArr by simp
    qed

    lemma pr1_tuple:
    assumes "span f g"
    shows "comp (pr1 (cod f) (cod g)) (tuple f g) = f"
    proof (intro arr_eqISC)
      have pr1: "«pr1 (cod f) (cod g) : prod (cod f) (cod g)  cod f»"
        using assms ide_cod by blast
      have tuple: "«tuple f g : dom f  prod (cod f) (cod g)»"
        using assms by blast
      show par: "par (comp (pr1 (cod f) (cod g)) (tuple f g)) f"
        using assms pr1_in_hom tuple_in_hom
        by (metis (no_types, lifting) comp_in_homI' ide_cod in_homE)
      show "Fun (comp (pr1 (cod f) (cod g)) (tuple f g)) = Fun f"
      proof -
        have seq: "seq (pr1 (cod f) (cod g)) (tuple f g)"
          using par by blast
        have "Fun (comp (pr1 (cod f) (cod g)) (tuple f g)) =
              restrict (Fun (pr1 (cod f) (cod g))  Fun (tuple f g)) (Dom (tuple f g))"
          using pr1 tuple seq Fun_comp by simp
        also have "... = restrict
                           (Fun (mkArr (set (prod (cod f) (cod g))) (Cod f)
                                       (λx. arr_of (hfst (elem_of x)))) 
                            Fun (mkArr (Dom f) (set (prod (cod f) (cod g)))
                                       (λx. arr_of elem_of (Fun f x), elem_of (Fun g x))))
                           (Dom (tuple f g))"
          unfolding pr1_def tuple_def
          using assms ide_cod by presburger
        also have
          "... = restrict
                   (restrict (λx. arr_of (hfst (elem_of x))) (set (prod (cod f) (cod g))) o
                      restrict (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)) (Dom f))
                   (Dom f)"
        proof -
          have "Fun (mkArr (set (prod (cod f) (cod g))) (Cod f) (λx. arr_of (hfst (elem_of x)))) =
                restrict (λx. arr_of (hfst (elem_of x))) (set (prod (cod f) (cod g)))"
            using assms Fun_mkArr ide_prod pr1
            by (metis (no_types, lifting) arrI ide_cod pr1_def)
          moreover have "Fun (mkArr (Dom f) (set (prod (cod f) (cod g)))
                                    (λx. arr_of elem_of (Fun f x), elem_of (Fun g x))) =
                         restrict (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)) (Dom f)"
            using assms Fun_mkArr ide_prod ide_cod tuple_def tuple arrI by simp
          ultimately show ?thesis
            using assms tuple_simps(2) by simp
        qed
        also have
          "... = restrict
                   ((λx. arr_of (hfst (elem_of x))) o (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                   (Dom f)"
          using assms tuple tuple_def arr_of_tuple_elem_of_membI by auto
        also have "... = restrict (Fun f) (Dom f)"
        proof
          fix x
          have "restrict ((λx. arr_of (hfst (elem_of x))) o (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                         (Dom f) x =
                restrict (λx. arr_of (elem_of (Fun f x))) (Dom f) x"
            by simp
          also have "... = restrict (Fun f) (Dom f) x"
          proof (cases "x  Dom f")
            show "x  Dom f  ?thesis" by simp
            assume x: "x  Dom f"
            have "Fun f x  Cod f"
              using assms x Fun_mapsto arr_char by blast
            moreover have "Cod f  Univ"
              using setp_set_ide assms ide_cod by blast
            ultimately show ?thesis
              using assms arr_of_elem_of Fun_mapsto by auto
          qed
          finally show "restrict ((λx. arr_of (hfst (elem_of x))) 
                                    (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                                 (Dom f) x =
                        restrict (Fun f) (Dom f) x"
            by blast
        qed
        also have "... = Fun f"
          using assms par Fun_mapsto Fun_mkArr mkArr_Fun
          by (metis (no_types, lifting))
        finally show ?thesis by blast
      qed
    qed

    lemma pr0_tuple:
    assumes "span f g"
    shows "comp (pr0 (cod f) (cod g)) (tuple f g) = g"
    proof (intro arr_eqISC)
      have pr0: "«pr0 (cod f) (cod g) : prod (cod f) (cod g)  cod g»"
        using assms ide_cod by blast
      have tuple: "«tuple f g : dom f  prod (cod f) (cod g)»"
        using assms by blast
      show par: "par (comp (pr0 (cod f) (cod g)) (tuple f g)) g"
        using assms pr0_in_hom tuple_in_hom
        by (metis (no_types, lifting) comp_in_homI' ide_cod in_homE)
      show "Fun (comp (pr0 (cod f) (cod g)) (tuple f g)) = Fun g"
      proof -
        have seq: "seq (pr0 (cod f) (cod g)) (tuple f g)"
          using par by blast
        have "Fun (comp (pr0 (cod f) (cod g)) (tuple f g)) =
              restrict (Fun (pr0 (cod f) (cod g))  Fun (tuple f g)) (Dom (tuple f g))"
          using pr0 tuple seq Fun_comp by simp
        also have
          "... = restrict
                   (Fun (mkArr (set (prod (cod f) (cod g))) (Cod g)
                               (λx. arr_of (hsnd (elem_of x)))) 
                    Fun (mkArr (Dom f) (set (prod (cod f) (cod g)))
                               (λx. arr_of elem_of (Fun f x), elem_of (Fun g x))))
                   (Dom (tuple f g))"
          unfolding pr0_def tuple_def
          using assms ide_cod by presburger
        also have "... = restrict
                           (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod (cod f) (cod g))) o
                            restrict (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)) (Dom g))
                           (Dom g)"
        proof -
          have "Fun (mkArr (set (prod (cod f) (cod g))) (Cod g) (λx. arr_of (hsnd (elem_of x)))) =
                restrict (λx. arr_of (hsnd (elem_of x))) (set (prod (cod f) (cod g)))"
            using assms Fun_mkArr ide_prod arrI
            by (metis (no_types, lifting) ide_cod pr0 pr0_def)
          moreover have "Fun (mkArr (Dom f) (set (prod (cod f) (cod g)))
                                    (λx. arr_of elem_of (Fun f x), elem_of (Fun g x))) =
                         restrict (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)) (Dom f)"
            using assms Fun_mkArr ide_prod ide_cod tuple_def tuple arrI by simp
          ultimately show ?thesis
            using assms tuple_simps(2) by simp
        qed
        also have "... = restrict
                           ((λx. arr_of (hsnd (elem_of x))) o (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                           (Dom g)"
          using assms tuple tuple_def arr_of_tuple_elem_of_membI by auto
        also have "... = restrict (Fun g) (Dom g)"
        proof
          fix x
          have "restrict ((λx. arr_of (hsnd (elem_of x)))
                            o (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                         (Dom g) x =
                restrict (λx. arr_of (elem_of (Fun g x))) (Dom g) x"
            by simp
          also have "... = restrict (Fun g) (Dom g) x"
          proof (cases "x  Dom g")
            show "x  Dom g  ?thesis" by simp
            assume x: "x  Dom g"
            have "Fun g x  Cod g"
              using assms x Fun_mapsto arr_char by blast
            moreover have "Cod g  Univ"
              using assms set_ideD(1) ide_cod by blast
            ultimately show ?thesis
              using assms arr_of_elem_of Fun_mapsto by auto
          qed
          finally show "restrict ((λx. arr_of (hsnd (elem_of x))) 
                                    (λx. arr_of elem_of (Fun f x), elem_of (Fun g x)))
                                 (Dom g) x =
                        restrict (Fun g) (Dom g) x"
            by blast
        qed
        also have "... = Fun g"
          using assms par Fun_mapsto Fun_mkArr mkArr_Fun
          by (metis (no_types, lifting))
        finally show ?thesis by blast
      qed
    qed

    lemma tuple_pr:
    assumes "ide a" and "ide b" and "«h : dom h  prod a b»"
    shows "tuple (comp (pr1 a b) h) (comp (pr0 a b) h) = h"
    proof (intro arr_eqISC)
      have pr0: "«pr0 a b : prod a b  b»"
        using assms pr0_in_hom ide_cod by blast
      have pr1: "«pr1 a b : prod a b  a»"
        using assms pr1_in_hom ide_cod by blast
      have tuple: "«tuple (comp (pr1 a b) h) (comp (pr0 a b) h) : dom h  prod a b»"
        using assms pr0 pr1
        by (metis (no_types, lifting) cod_comp dom_comp pr0_simps(3) pr1_simps(3)
            seqI' tuple_in_hom)
      show par: "par (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) h"
        using assms tuple by (metis (no_types, lifting) in_homE)
      show "Fun (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) = Fun h"
      proof -
        have 1: "Fun (comp (pr1 a b) h) =
                 restrict (restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b))  Fun h) (Dom h)"
          using assms pr1 Fun_comp Fun_pr1 seqI' by auto
        have 2: "Fun (comp (pr0 a b) h) =
                 restrict (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b))  Fun h) (Dom h)"
          using assms pr0 Fun_comp Fun_pr0 seqI' by auto
        have "Fun (tuple (comp (pr1 a b) h) (comp (pr0 a b) h)) =
              restrict (λx. arr_of elem_of (restrict
                                       (restrict (λx. arr_of (hfst (elem_of x))) (set (prod a b))  Fun h)
                                                 (Dom h) x),
                                elem_of (restrict
                                       (restrict (λx. arr_of (hsnd (elem_of x))) (set (prod a b))  Fun h)
                                                 (Dom h) x))
                       (Dom h)"
        proof -
          have "Dom (comp (pr1 a b) h) = Dom h"
            using assms pr1_in_hom
            by (metis (no_types, lifting) in_homE dom_comp seqI)
          moreover have "arr (mkArr (Dom (comp (pr1 a b) h))
                             (set (prod (cod (comp (pr1 a b) h)) (cod (comp (pr0 a b) h))))
                             (λx. arr_of elem_of (Fun (comp (pr1 a b) h) x),
                                      elem_of (Fun (comp (pr0 a b) h) x)))"
            using tuple unfolding tuple_def by blast
          ultimately show ?thesis
            using 1 2 tuple tuple_def
                  Fun_mkArr [of "Dom (comp (pr1 a b) h)"
                                 "set (prod (cod (comp (pr1 a b) h))
                                            (cod (comp (pr0 a b) h)))"
                                 "λx. arr_of elem_of (Fun (comp (pr1 a b) h) x),
                                          elem_of (Fun (comp (pr0 a b) h) x)"]
            by simp
        qed
        also have "... = Fun h"
        proof
          let ?f = "..."
          fix x
          show "?f x = Fun h x"
          proof -
            have "x  Dom h  ?f x = Fun h x"
            proof -
              assume x: "x  Dom h"
              have "restrict ?f (Dom h) x = undefined"
                using assms x restrict_apply by auto
              also have "... = Fun h x"
              proof -
                have "arr h"
                  using assms by blast
                thus ?thesis
                  using assms x Fun_mapsto [of h] extensional_arb [of "Fun h" "Dom h" x]
                  by simp
              qed
              finally show ?thesis by auto
            qed
            moreover have "x  Dom h  ?f x = Fun h x"
            proof -
              assume x: "x  Dom h"
              have 1: "Fun h x  set (prod a b)"
              proof -
                have "Fun h x  Cod h"
                  using assms x Fun_mapsto [of h] by blast
                moreover have "Cod h = set (prod a b)"
                  using assms ide_prod
                  by (metis (no_types, lifting) in_homE)
                ultimately show ?thesis by fast
              qed
              have "?f x = arr_of hfst (elem_of (Fun h x)), hsnd (elem_of (Fun h x))"
                using x 1 by simp
              also have "... = arr_of (elem_of (Fun h x))"
              proof -
                have "elem_of (Fun h x)  ide_to_hf a * ide_to_hf b"
                  using assms x 1 par
                  by (metis (no_types, lifting) prod_def elem_of_membI UNIV_I ide_prod
                      ide_to_hf_hf_to_ide)
                thus ?thesis
                  using x is_hpair_def by auto
              qed
              also have "... = Fun h x"
                using 1 arr_of_elem_of assms set_ideD(1) ide_prod by blast
              finally show ?thesis by blast
            qed
            ultimately show ?thesis by blast
          qed
        qed
        finally show ?thesis by blast
      qed
    qed

    interpretation HF': elementary_category_with_binary_products comp pr0 pr1
    proof
      show "a b. ide a; ide b  span (pr1 a b) (pr0 a b)"
        using pr0_simps(1) pr0_simps(2) pr1_simps(1) pr1_simps(2) by auto
      show "a b. ide a; ide b  cod (pr0 a b) = b"
        using pr0_simps(1-3) by blast
      show "a b. ide a; ide b  cod (pr1 a b) = a"
        using pr1_simps(1-3) by blast
      show "f g. span f g 
                    ∃!l. comp (pr1 (cod f) (cod g)) l = f  comp (pr0 (cod f) (cod g)) l = g"
      proof
        fix f g
        assume fg: "span f g"
        show "comp (pr1 (cod f) (cod g)) (tuple f g) = f 
              comp (pr0 (cod f) (cod g)) (tuple f g) = g"
          using fg pr0_simps pr1_simps tuple_simps pr0_tuple pr1_tuple by presburger
        show "l. comp (pr1 (cod f) (cod g)) l = f  comp (pr0 (cod f) (cod g)) l = g
                       l = tuple f g "
        proof -
          fix l
          assume l: "comp (pr1 (cod f) (cod g)) l = f  comp (pr0 (cod f) (cod g)) l = g"
          show "l = tuple f g"
            using fg l tuple_pr
            by (metis (no_types, lifting) arr_iff_in_hom ide_cod seqE pr0_simps(2))
        qed
      qed
    qed

    text‹
      For reasons of economy of locale parameters, the notion prod› is a defined notion
      of the @{locale elementary_category_with_binary_products} locale.
      However, we need to be able to relate this notion to that of cartesian product of
      hereditarily finite sets, which we have already used to give a definition of prod›.
      The locale assumptions for @{locale elementary_cartesian_closed_category} refer
      specifically to HF'.prod›, even though in the end the notion itself does not depend
      on that choice.  To be able to show that the locale assumptions of
      @{locale elementary_cartesian_closed_category} are satisfied, we need to use a choice
      of products that we can relate to the cartesian product of hereditarily
      finite sets.  We therefore need to show that our previously defined prod› coincides
      (on objects) with the one defined in the @{locale elementary_category_with_binary_products} locale;
      \emph{i.e.}~HF'.prod›.  Note that the latter is defined for all arrows,
      not just identity arrows, so we need to use that for the subsequent definitions and proofs.
    ›

    lemma prod_ide_eq:
    assumes "ide a" and "ide b"
    shows "prod a b = HF'.prod a b"
      using assms prod_def HF'.pr_simps(2) HF'.prod_def pr0_simps(2) by presburger

    lemma tuple_span_eq:
    assumes "span f g"
    shows "tuple f g = HF'.tuple f g"
      using assms tuple_def HF'.tuple_def
      by (metis (no_types, lifting) HF'.tuple_eqI ide_cod pr0_tuple pr1_tuple)

    section "Exponentials"

    text‹
      We now turn our attention to exponentials.
    ›

    definition exp
    where "exp b c = hf_to_ide (hexp (ide_to_hf b) (ide_to_hf c))"

    definition eval
    where "eval b c = mkArr (set (HF'.prod (exp b c) b)) (set c)
                            (λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x))))"

    definition Λ
    where "Λ a b c f = mkArr (set a) (set (exp b c))
                             (λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c)
                                                 (arr_to_hfun f))
                                           (elem_of x)))"

    lemma ide_exp:
    assumes "ide b" and "ide c"
    shows "ide (exp b c)"
      using assms exp_def hf_to_ide_mapsto ide_to_hf_mapsto by auto

    lemma hfset_ide_to_hf:
    assumes "ide a"
    shows "hfset (ide_to_hf a) = elem_of ` set a"
      using assms ide_to_hf_def ide_implies_finite_set(1) by auto

    lemma eval_in_hom [intro]:
    assumes "ide b" and "ide c"
    shows "in_hom (eval b c) (HF'.prod (exp b c) b) c"
    proof
      show 1: "arr (eval b c)"
      proof (unfold eval_def arr_mkArr, intro conjI)
        show "set (HF'.prod (exp b c) b)  Univ"
          using HF'.ide_prod assms set_ideD(1) ide_exp by presburger
        show "set c  Univ"
          using assms set_ideD(1) by blast
        show "(λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x))))
                  set (HF'.prod (exp b c) b)  set c"
        proof
          fix x
          assume "x  set (HF'.prod (exp b c) b)"
          hence x: "x  set (prod (exp b c) b)"
            using assms prod_ide_eq ide_exp by auto
          show "arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x)))  set c"
          proof (intro arr_of_membI)
            show "happ (hfst (elem_of x)) (hsnd (elem_of x))  ide_to_hf c"
            proof -
              have 1: "elem_of x  ide_to_hf (exp b c) * ide_to_hf b"
              proof -
                have "elem_of x  ide_to_hf (prod (exp b c) b)"
                  using assms x elem_of_membI ide_prod ide_exp by simp
                thus ?thesis
                  using assms x prod_def ide_to_hf_hf_to_ide by auto
              qed
              have "hfst (elem_of x)  hexp (ide_to_hf b) (ide_to_hf c)"
                using assms 1 x exp_def ide_to_hf_hf_to_ide by auto
              moreover have "hsnd (elem_of x)  ide_to_hf b"
                using assms 1 by auto
              ultimately show ?thesis
                using happ_mapsto [of "hfst (elem_of x)" "ide_to_hf b" "ide_to_hf c"
                                      "hsnd (elem_of x)"]
                by simp
            qed
          qed
        qed
        show "finite (elem_of ` set (HF'.prod (exp b c) b))"
          using HF'.ide_prod setp_set_ide assms ide_exp by presburger
        show "finite (elem_of ` set c)"
          using setp_set_ide assms(2) by blast
      qed
      show "dom (eval b c) = HF'.prod (exp b c) b"
        using assms 1 ide_char HF'.ide_prod ide_exp dom_mkArr eval_def
        by (metis (no_types, lifting) mkIde_set)
      show "cod (eval b c) = c"
        using assms 1 ide_char cod_mkArr eval_def
        by (metis (no_types, lifting) mkIde_set)
    qed

    lemma eval_simps [simp]:
    assumes "ide b" and "ide c"
    shows "arr (eval b c)"
    and "dom (eval b c) = HF'.prod (exp b c) b"
    and "cod (eval b c) = c"
      using assms eval_in_hom by blast+

    lemma hlam_arr_to_hfun_in_hexp:
    assumes "ide a" and "ide b" and "ide c"
    and "in_hom f (prod a b) c"
    shows "hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f)
              hexp (ide_to_hf a) (ide_to_hf (exp b c))"
      using assms hfun_in_hexp hfun_hlam
      by (metis (no_types, lifting) prod_def HCollect_iff in_homE UNIV_I
          arr_to_hfun_in_hexp exp_def hexp_def ide_to_hf_hf_to_ide)

    lemma lam_in_hom [intro]:
    assumes "ide a" and "ide b" and "ide c"
    and "in_hom f (prod a b) c"
    shows "in_hom (Λ a b c f) a (exp b c)"
    proof
      show 1: "arr (Λ a b c f)"
      proof (unfold Λ_def arr_mkArr, intro conjI)
        show "set a  Univ"
          using assms(1) set_ideD(1) by blast
        show "set (exp b c)  Univ"
          using assms(2-3) set_ideD(1) ide_exp ide_char by blast
        show "finite (elem_of ` set a)"
          using assms(1) set_ideD(1) setp_set_ide by presburger
        show "finite (elem_of ` set (exp b c))"
          using assms(2-3) set_ideD(1) setp_set_ide ide_exp by presburger
        show "(λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f))
                            (elem_of x)))
                  set a  set (exp b c)"
        proof
          fix x
          assume x: "x  set a"
          show "arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f))
                         (elem_of x))
                      set (exp b c)"
            using assms x hlam_arr_to_hfun_in_hexp ide_to_hf_def elem_of_membI happ_mapsto
                  arr_of_membI
            by meson
        qed
      qed
      show "dom (Λ a b c f) = a"
        using assms(1) 1 Λ_def ide_char dom_mkArr mkIde_set by auto
      show "cod (Λ a b c f) = exp b c"
        using assms(2-3) 1 Λ_def cod_mkArr ide_exp mkIde_set by auto
    qed

    lemma lam_simps [simp]:
    assumes "ide a" and "ide b" and "ide c"
    and "in_hom f (prod a b) c"
    shows "arr (Λ a b c f)"
    and "dom (Λ a b c f) = a"
    and "cod (Λ a b c f) = exp b c"
      using assms lam_in_hom by blast+

    lemma Fun_lam:
    assumes "ide a" and "ide b" and "ide c"
    and "in_hom f (prod a b) c"
    shows "Fun (Λ a b c f) =
           restrict (λx. arr_of (happ (hlam (ide_to_hf a) (ide_to_hf b) (ide_to_hf c) (arr_to_hfun f))
                                  (elem_of x)))
                    (set a)"
      using assms arr_char lam_simps(1) Λ_def Fun_mkArr by simp

    lemma Fun_eval:
    assumes "ide b" and "ide c"
    shows "Fun (eval b c) = restrict (λx. arr_of (happ (hfst (elem_of x)) (hsnd (elem_of x))))
                                     (set (HF'.prod (exp b c) b))"
      using assms arr_char eval_simps(1) eval_def Fun_mkArr by force

    lemma Fun_prod:
    assumes "arr f" and "arr g" and "x  set (prod (dom f) (dom g))"
    shows "Fun (HF'.prod f g) x = arr_of elem_of (Fun f (arr_of (hfst (elem_of x)))),
                                     elem_of (Fun g (arr_of (hsnd (elem_of x))))"
    proof -
      have 1: "span (comp f (pr1 (dom f) (dom g))) (comp g (pr0 (dom f) (dom g)))"
        using assms
        by (metis (no_types, lifting) HF'.prod_def HF'.prod_simps(1) HF'.tuple_ext not_arr_null)
      have 2: "Dom (comp f (pr1 (dom f) (dom g))) = set (prod (dom f) (dom g))"
        using assms
        by (metis (mono_tags, lifting) 1 dom_comp ide_dom pr0_simps(2))
      have 3: "Dom (comp g (pr0 (dom f) (dom g))) = set (prod (dom f) (dom g))"
        using assms 1 2 by force
      have "Fun (HF'.prod f g) x =
            Fun (HF'.tuple (comp f (pr1 (dom f) (dom g))) (comp g (pr0 (dom f) (dom g)))) x"
        using assms(3) HF'.prod_def by simp
      also have "... = restrict (λx. arr_of elem_of (Fun (comp f (pr1 (dom f) (dom g))