# 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
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
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_eqI⇩S⇩C)
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_eqI⇩S⇩C)
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_eqI⇩S⇩C)
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))