Theory Exponential_Objects
section ‹Exponential Objects, Transposes and Evaluation›
theory Exponential_Objects
imports Initial
begin
text ‹The axiomatization below corresponds to Axiom 9 (Exponential Objects) in Halvorson.›
axiomatization
exp_set :: "cset ⇒ cset ⇒ cset" ("_⇗_⇖" [100,100]100) and
eval_func :: "cset ⇒ cset ⇒ cfunc" and
transpose_func :: "cfunc ⇒ cfunc" ("_⇧♯" [100]100)
where
exp_set_inj: "X⇗A⇖ = Y⇗B⇖ ⟹ X = Y ∧ A = B" and
eval_func_type[type_rule]: "eval_func X A : A×⇩c X⇗A⇖ → X" and
transpose_func_type[type_rule]: "f : A ×⇩c Z → X ⟹ f⇧♯ : Z → X⇗A⇖" and
transpose_func_def: "f : A ×⇩c Z → X ⟹ (eval_func X A) ∘⇩c (id A ×⇩f f⇧♯) = f" and
transpose_func_unique:
"f : A×⇩cZ → X ⟹ g: Z → X⇗A⇖ ⟹ (eval_func X A) ∘⇩c (id A ×⇩f g) = f ⟹ g = f⇧♯"
lemma eval_func_surj:
assumes "nonempty(A)"
shows "surjective((eval_func X A))"
unfolding surjective_def
proof(clarify)
fix x
assume x_type: "x ∈⇩c codomain (eval_func X A)"
then have x_type2[type_rule]: "x ∈⇩c X"
using cfunc_type_def eval_func_type by auto
obtain a where a_def[type_rule]: "a ∈⇩c A"
using assms nonempty_def by auto
have needed_type: "⟨a, (x ∘⇩c right_cart_proj A 𝟭)⇧♯⟩ ∈⇩c domain (eval_func X A)"
using cfunc_type_def by (typecheck_cfuncs, auto)
have "(eval_func X A) ∘⇩c ⟨a, (x ∘⇩c right_cart_proj A 𝟭)⇧♯⟩ =
(eval_func X A) ∘⇩c ((id(A) ×⇩f (x ∘⇩c right_cart_proj A 𝟭)⇧♯) ∘⇩c ⟨a, id(𝟭)⟩)"
by (typecheck_cfuncs, smt a_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 x_type2)
also have "... = ((eval_func X A) ∘⇩c (id(A) ×⇩f (x ∘⇩c right_cart_proj A 𝟭)⇧♯)) ∘⇩c ⟨a, id(𝟭)⟩"
by (typecheck_cfuncs, meson a_def comp_associative2 x_type2)
also have "... = (x ∘⇩c right_cart_proj A 𝟭) ∘⇩c ⟨a, id(𝟭)⟩"
by (metis comp_type right_cart_proj_type transpose_func_def x_type2)
also have "... = x ∘⇩c (right_cart_proj A 𝟭 ∘⇩c ⟨a, id(𝟭)⟩)"
using a_def cfunc_type_def comp_associative x_type2 by (typecheck_cfuncs, auto)
also have "... = x"
using a_def id_right_unit2 right_cart_proj_cfunc_prod x_type2 by (typecheck_cfuncs, auto)
ultimately show "∃y. y ∈⇩c domain (eval_func X A) ∧ eval_func X A ∘⇩c y = x"
using needed_type by (typecheck_cfuncs, auto)
qed
text ‹The lemma below corresponds to a note above Definition 2.5.1 in Halvorson.›
lemma exponential_object_identity:
"(eval_func X A)⇧♯ = id⇩c(X⇗A⇖)"
by (metis cfunc_type_def eval_func_type id_cross_prod id_right_unit id_type transpose_func_unique)
lemma eval_func_X_empty_injective:
assumes "is_empty Y"
shows "injective (eval_func X Y)"
unfolding injective_def
by (typecheck_cfuncs,metis assms cfunc_type_def comp_type left_cart_proj_type is_empty_def)
subsection ‹Lifting Functions›
text ‹The definition below corresponds to Definition 2.5.1 in Halvorson.›
definition exp_func :: "cfunc ⇒ cset ⇒ cfunc" ("(_)⇗_⇖⇩f" [100,100]100) where
"exp_func g A = (g ∘⇩c eval_func (domain g) A)⇧♯"
lemma exp_func_def2:
assumes "g : X → Y"
shows "exp_func g A = (g ∘⇩c eval_func X A)⇧♯"
using assms cfunc_type_def exp_func_def by auto
lemma exp_func_type[type_rule]:
assumes "g : X → Y"
shows "g⇗A⇖⇩f : X⇗A⇖ → Y⇗A⇖"
using assms by (unfold exp_func_def2, typecheck_cfuncs)
lemma exp_of_id_is_id_of_exp:
"id(X⇗A⇖) = (id(X))⇗A⇖⇩f"
by (metis (no_types) eval_func_type exp_func_def exponential_object_identity id_domain id_left_unit2)
text ‹The lemma below corresponds to a note below Definition 2.5.1 in Halvorson.›
lemma exponential_square_diagram:
assumes "g : Y → Z"
shows "(eval_func Z A) ∘⇩c (id⇩c(A)×⇩f g⇗A⇖⇩f) = g ∘⇩c (eval_func Y A)"
using assms by (typecheck_cfuncs, simp add: exp_func_def2 transpose_func_def)
text ‹The lemma below corresponds to Proposition 2.5.2 in Halvorson.›
lemma transpose_of_comp:
assumes f_type: "f: A ×⇩c X → Y" and g_type: "g: Y → Z"
shows "f: A ×⇩c X → Y ∧ g: Y → Z ⟹ (g ∘⇩c f)⇧♯ = g⇗A⇖⇩f ∘⇩c f⇧♯"
proof clarify
have left_eq: "(eval_func Z A) ∘⇩c(id(A) ×⇩f (g ∘⇩c f)⇧♯) = g ∘⇩c f"
using comp_type f_type g_type transpose_func_def by blast
have right_eq: "(eval_func Z A) ∘⇩c (id⇩c A ×⇩f (g⇗A⇖⇩f ∘⇩c f⇧♯)) = g ∘⇩c f"
proof -
have "(eval_func Z A) ∘⇩c (id⇩c A ×⇩f (g⇗A⇖⇩f ∘⇩c f⇧♯)) =
(eval_func Z A) ∘⇩c ((id⇩c A ×⇩f (g⇗A⇖⇩f)) ∘⇩c (id⇩c A ×⇩f f⇧♯))"
by (typecheck_cfuncs, smt identity_distributes_across_composition assms)
also have "... = (g ∘⇩c eval_func Y A) ∘⇩c (id⇩c A ×⇩f f⇧♯)"
by (typecheck_cfuncs, smt comp_associative2 exp_func_def2 transpose_func_def assms)
also have "... = g ∘⇩c f"
by (typecheck_cfuncs, smt (verit, best) comp_associative2 transpose_func_def assms)
finally show ?thesis.
qed
show "(g ∘⇩c f)⇧♯ = g⇗A⇖⇩f ∘⇩c f⇧♯"
using assms by (typecheck_cfuncs, metis right_eq transpose_func_unique)
qed
lemma exponential_object_identity2:
"id(X)⇗A⇖⇩f = id⇩c(X⇗A⇖)"
by (metis eval_func_type exp_func_def exponential_object_identity id_domain id_left_unit2)
text ‹The lemma below corresponds to comments below Proposition 2.5.2 and above Definition 2.5.3 in Halvorson.›
lemma eval_of_id_cross_id_sharp1:
"(eval_func (A ×⇩c X) A) ∘⇩c (id(A) ×⇩f (id(A ×⇩c X))⇧♯) = id(A ×⇩c X)"
using id_type transpose_func_def by blast
lemma eval_of_id_cross_id_sharp2:
assumes "a : Z → A" "x : Z → X"
shows "((eval_func (A ×⇩c X) A) ∘⇩c (id(A) ×⇩f (id(A ×⇩c X))⇧♯)) ∘⇩c ⟨a,x⟩ = ⟨a,x⟩"
by (smt assms cfunc_cross_prod_comp_cfunc_prod eval_of_id_cross_id_sharp1 id_cross_prod id_left_unit2 id_type)
lemma transpose_factors:
assumes "f: X → Y"
assumes "g: Y → Z"
shows "(g ∘⇩c f)⇗A⇖⇩f = (g⇗A⇖⇩f) ∘⇩c (f⇗A⇖⇩f)"
using assms by (typecheck_cfuncs, smt comp_associative2 comp_type eval_func_type exp_func_def2 transpose_of_comp)
subsection ‹Inverse Transpose Function (flat)›
text ‹The definition below corresponds to Definition 2.5.3 in Halvorson.›
definition inv_transpose_func :: "cfunc ⇒ cfunc" ("_⇧♭" [100]100) where
"f⇧♭ = (THE g. ∃ Z X A. domain f = Z ∧ codomain f = X⇗A⇖ ∧ g = (eval_func X A) ∘⇩c (id A ×⇩f f))"
lemma inv_transpose_func_def2:
assumes "f : Z → X⇗A⇖"
shows "∃ Z X A. domain f = Z ∧ codomain f = X⇗A⇖ ∧ f⇧♭ = (eval_func X A) ∘⇩c (id A ×⇩f f)"
unfolding inv_transpose_func_def
proof (rule theI)
show "∃Z Y B. domain f = Z ∧ codomain f = Y⇗B⇖ ∧ eval_func X A ∘⇩c id⇩c A ×⇩f f = eval_func Y B ∘⇩c id⇩c B ×⇩f f"
using assms cfunc_type_def by blast
next
fix g
assume "∃Z X A. domain f = Z ∧ codomain f = X⇗A⇖ ∧ g = eval_func X A ∘⇩c id⇩c A ×⇩f f"
then show "g = eval_func X A ∘⇩c id⇩c A ×⇩f f"
by (metis assms cfunc_type_def exp_set_inj)
qed
lemma inv_transpose_func_def3:
assumes f_type: "f : Z → X⇗A⇖"
shows "f⇧♭ = (eval_func X A) ∘⇩c (id A ×⇩f f)"
by (metis cfunc_type_def exp_set_inj f_type inv_transpose_func_def2)
lemma flat_type[type_rule]:
assumes f_type[type_rule]: "f : Z → X⇗A⇖"
shows "f⇧♭ : A ×⇩c Z → X"
by (etcs_subst inv_transpose_func_def3, typecheck_cfuncs)
text ‹The lemma below corresponds to Proposition 2.5.4 in Halvorson.›
lemma inv_transpose_of_composition:
assumes "f: X → Y" "g: Y → Z⇗A⇖"
shows "(g ∘⇩c f)⇧♭ = g⇧♭ ∘⇩c (id(A) ×⇩f f)"
using assms comp_associative2 identity_distributes_across_composition
by ((etcs_subst inv_transpose_func_def3)+, typecheck_cfuncs, auto)
text ‹The lemma below corresponds to Proposition 2.5.5 in Halvorson.›
lemma flat_cancels_sharp:
"f : A ×⇩c Z → X ⟹ (f⇧♯)⇧♭ = f"
using inv_transpose_func_def3 transpose_func_def transpose_func_type by fastforce
text ‹The lemma below corresponds to Proposition 2.5.6 in Halvorson.›
lemma sharp_cancels_flat:
"f: Z → X⇗A⇖ ⟹ (f⇧♭)⇧♯ = f"
proof -
assume f_type: "f : Z → X⇗A⇖"
then have uniqueness: "∀ g. g : Z → X⇗A⇖ ⟶ eval_func X A ∘⇩c (id A ×⇩f g) = f⇧♭ ⟶ g = (f⇧♭)⇧♯"
by (typecheck_cfuncs, simp add: transpose_func_unique)
have "eval_func X A ∘⇩c (id A ×⇩f f) = f⇧♭"
by (metis f_type inv_transpose_func_def3)
then show "f⇧♭⇧♯ = f"
using f_type uniqueness by auto
qed
lemma same_evals_equal:
assumes "f : Z → X⇗A⇖" "g: Z → X⇗A⇖"
shows "eval_func X A ∘⇩c (id A ×⇩f f) = eval_func X A ∘⇩c (id A ×⇩f g) ⟹ f = g"
by (metis assms inv_transpose_func_def3 sharp_cancels_flat)
lemma sharp_comp:
assumes f_type[type_rule]: "f : A ×⇩c Z → X" and g_type[type_rule]: "g : W → Z"
shows "f⇧♯ ∘⇩c g = (f ∘⇩c (id A ×⇩f g))⇧♯"
proof (etcs_rule same_evals_equal[where X=X, where A=A])
have "eval_func X A ∘⇩c (id A ×⇩f (f⇧♯ ∘⇩c g)) = eval_func X A ∘⇩c (id A ×⇩f f⇧♯) ∘⇩c (id A ×⇩f g)"
using assms by (typecheck_cfuncs, simp add: identity_distributes_across_composition)
also have "... = f ∘⇩c (id A ×⇩f g)"
using assms by (typecheck_cfuncs, simp add: comp_associative2 transpose_func_def)
also have "... = eval_func X A ∘⇩c (id⇩c A ×⇩f (f ∘⇩c (id⇩c A ×⇩f g))⇧♯)"
using assms by (typecheck_cfuncs, simp add: transpose_func_def)
finally show "eval_func X A ∘⇩c (id A ×⇩f (f⇧♯ ∘⇩c g)) = eval_func X A ∘⇩c (id⇩c A ×⇩f (f ∘⇩c (id⇩c A ×⇩f g))⇧♯)".
qed
lemma flat_pres_epi:
assumes "nonempty(A)"
assumes "f : Z → X⇗A⇖"
assumes "epimorphism f"
shows "epimorphism(f⇧♭)"
proof -
have equals: "f⇧♭ = (eval_func X A) ∘⇩c (id(A) ×⇩f f)"
using assms(2) inv_transpose_func_def3 by auto
have idA_f_epi: "epimorphism((id(A) ×⇩f f))"
using assms(2) assms(3) cfunc_cross_prod_surj epi_is_surj id_isomorphism id_type iso_imp_epi_and_monic surjective_is_epimorphism by blast
have eval_epi: "epimorphism((eval_func X A))"
by (simp add: assms(1) eval_func_surj surjective_is_epimorphism)
have "codomain ((id(A) ×⇩f f)) = domain ((eval_func X A))"
using assms(2) cfunc_type_def by (typecheck_cfuncs, auto)
then show ?thesis
by (simp add: composition_of_epi_pair_is_epi equals eval_epi idA_f_epi)
qed
lemma transpose_inj_is_inj:
assumes "g: X → Y"
assumes "injective g"
shows "injective(g⇗A⇖⇩f)"
unfolding injective_def
proof(clarify)
fix x y
assume x_type[type_rule]: "x ∈⇩c domain (g⇗A⇖⇩f)"
assume y_type[type_rule]:"y ∈⇩c domain (g⇗A⇖⇩f)"
assume eqs: "g⇗A⇖⇩f ∘⇩c x = g⇗A⇖⇩f ∘⇩c y"
have mono_g: "monomorphism g"
by (meson CollectI assms(2) injective_imp_monomorphism)
have x_type'[type_rule]: "x ∈⇩c X⇗A⇖"
using assms(1) cfunc_type_def exp_func_type by (typecheck_cfuncs, force)
have y_type'[type_rule]: "y ∈⇩c X⇗A⇖"
using cfunc_type_def x_type x_type' y_type by presburger
have "(g ∘⇩c eval_func X A)⇧♯ ∘⇩c x = (g ∘⇩c eval_func X A)⇧♯ ∘⇩c y"
unfolding exp_func_def using assms eqs exp_func_def2 by force
then have "g ∘⇩c (eval_func X A ∘⇩c(id(A) ×⇩f x)) = g ∘⇩c (eval_func X A ∘⇩c (id(A) ×⇩f y))"
by (smt (z3) assms(1) comp_type eqs flat_cancels_sharp flat_type inv_transpose_func_def3 sharp_cancels_flat transpose_of_comp x_type' y_type')
then have "eval_func X A ∘⇩c(id(A) ×⇩f x) = eval_func X A ∘⇩c (id(A) ×⇩f y)"
by (metis assms(1) mono_g flat_type inv_transpose_func_def3 monomorphism_def2 x_type' y_type')
then show "x = y"
by (meson same_evals_equal x_type' y_type')
qed
lemma eval_func_X_one_injective:
"injective (eval_func X 𝟭)"
proof (cases "∃ x. x ∈⇩c X")
assume "∃x. x ∈⇩c X"
then obtain x where x_type: "x ∈⇩c X"
by auto
then have "eval_func X 𝟭 ∘⇩c id⇩c 𝟭 ×⇩f (x ∘⇩c β⇘𝟭 ×⇩c 𝟭⇙)⇧♯ = x ∘⇩c β⇘𝟭 ×⇩c 𝟭⇙"
using comp_type terminal_func_type transpose_func_def by blast
show "injective (eval_func X 𝟭)"
unfolding injective_def
proof clarify
fix a b
assume a_type: "a ∈⇩c domain (eval_func X 𝟭)"
assume b_type: "b ∈⇩c domain (eval_func X 𝟭)"
assume evals_equal: "eval_func X 𝟭 ∘⇩c a = eval_func X 𝟭 ∘⇩c b"
have eval_dom: "domain(eval_func X 𝟭) = 𝟭 ×⇩c (X⇗𝟭⇖)"
using cfunc_type_def eval_func_type by auto
obtain A where a_def: "A ∈⇩c X⇗𝟭⇖ ∧ a = ⟨id 𝟭, A⟩"
by (typecheck_cfuncs, metis a_type cart_prod_decomp eval_dom terminal_func_unique)
obtain B where b_def: "B ∈⇩c X⇗𝟭⇖ ∧ b = ⟨id 𝟭, B⟩"
by (typecheck_cfuncs, metis b_type cart_prod_decomp eval_dom terminal_func_unique)
have "A⇧♭ ∘⇩c ⟨id 𝟭, id 𝟭⟩ = B⇧♭ ∘⇩c ⟨id 𝟭, id 𝟭⟩"
proof -
have "A⇧♭ ∘⇩c ⟨id 𝟭 , id 𝟭⟩ = (eval_func X 𝟭) ∘⇩c (id 𝟭 ×⇩f (A⇧♭)⇧♯) ∘⇩c ⟨id 𝟭, id 𝟭⟩"
by (typecheck_cfuncs, smt (verit, best) a_def comp_associative2 inv_transpose_func_def3 sharp_cancels_flat)
also have "... = eval_func X 𝟭 ∘⇩c a"
using a_def cfunc_cross_prod_comp_cfunc_prod id_right_unit2 sharp_cancels_flat by (typecheck_cfuncs, force)
also have "... = eval_func X 𝟭 ∘⇩c b"
by (simp add: evals_equal)
also have "... = (eval_func X 𝟭) ∘⇩c (id 𝟭 ×⇩f (B⇧♭)⇧♯) ∘⇩c ⟨id 𝟭, id 𝟭⟩"
using b_def cfunc_cross_prod_comp_cfunc_prod id_right_unit2 sharp_cancels_flat by (typecheck_cfuncs, auto)
also have "... = B⇧♭ ∘⇩c ⟨id 𝟭, id 𝟭⟩"
by (typecheck_cfuncs, smt (verit) b_def comp_associative2 inv_transpose_func_def3 sharp_cancels_flat)
finally show "A⇧♭ ∘⇩c ⟨id 𝟭, id 𝟭⟩ = B⇧♭ ∘⇩c ⟨id 𝟭, id 𝟭⟩".
qed
then have "A⇧♭ = B⇧♭"
by (typecheck_cfuncs, smt swap_def a_def b_def cfunc_prod_comp comp_associative2 diagonal_def diagonal_type id_right_unit2 id_type left_cart_proj_type right_cart_proj_type swap_idempotent swap_type terminal_func_comp terminal_func_unique)
then have "A = B"
by (metis a_def b_def sharp_cancels_flat)
then show "a = b"
by (simp add: a_def b_def)
qed
next
assume "∄x. x ∈⇩c X"
then show "injective (eval_func X 𝟭)"
by (typecheck_cfuncs, metis cfunc_type_def comp_type injective_def)
qed
text ‹In the lemma below, the nonempty assumption is required.
Consider, for example, @{term "X = Ω"} and @{term "A = ∅"}›
lemma sharp_pres_mono:
assumes "f : A ×⇩c Z → X"
assumes "monomorphism(f)"
assumes "nonempty A"
shows "monomorphism(f⇧♯)"
unfolding monomorphism_def2
proof(clarify)
fix g h U Y x
assume g_type[type_rule]: "g : U → Y"
assume h_type[type_rule]: "h : U → Y"
assume f_sharp_type[type_rule]: "f⇧♯ : Y → x"
assume equals: "f⇧♯ ∘⇩c g = f⇧♯ ∘⇩c h"
have f_sharp_type2: "f⇧♯ : Z → X⇗A⇖"
by (simp add: assms(1) transpose_func_type)
have Y_is_Z: "Y = Z"
using cfunc_type_def f_sharp_type f_sharp_type2 by auto
have x_is_XA: "x = X⇗A⇖"
using cfunc_type_def f_sharp_type f_sharp_type2 by auto
have g_type2: "g : U → Z"
using Y_is_Z g_type by blast
have h_type2: "h : U → Z"
using Y_is_Z h_type by blast
have idg_type: "(id(A) ×⇩f g) : A ×⇩c U → A ×⇩c Z"
by (simp add: cfunc_cross_prod_type g_type2 id_type)
have idh_type: "(id(A) ×⇩f h) : A ×⇩c U → A ×⇩c Z"
by (simp add: cfunc_cross_prod_type h_type2 id_type)
then have epic: "epimorphism(right_cart_proj A U)"
using assms(3) nonempty_left_imp_right_proj_epimorphism by blast
have fIdg_is_fIdh: "f ∘⇩c (id(A) ×⇩f g) = f ∘⇩c (id(A) ×⇩f h)"
proof -
have "f ∘⇩c (id(A) ×⇩f g) = (eval_func X A ∘⇩c (id(A) ×⇩f f⇧♯)) ∘⇩c (id(A) ×⇩f g)"
using assms(1) transpose_func_def by auto
also have "... = (eval_func X A ∘⇩c (id(A) ×⇩f f⇧♯)) ∘⇩c (id(A) ×⇩f h)"
by (metis Y_is_Z equals f_sharp_type2 g_type h_type inv_transpose_func_def3 inv_transpose_of_composition)
also have "... = f ∘⇩c (id(A) ×⇩f h)"
using assms(1) transpose_func_def by auto
finally show ?thesis.
qed
then have idg_is_idh: "(id(A) ×⇩f g) = (id(A) ×⇩f h)"
using assms fIdg_is_fIdh idg_type idh_type monomorphism_def3 by blast
then have "g ∘⇩c (right_cart_proj A U) = h ∘⇩c (right_cart_proj A U)"
by (smt g_type2 h_type2 id_type right_cart_proj_cfunc_cross_prod)
then show "g = h"
using epic epimorphism_def2 g_type2 h_type2 right_cart_proj_type by blast
qed
subsection ‹Metafunctions and their Inverses (Cnufatems)›
subsubsection ‹Metafunctions›
definition metafunc :: "cfunc ⇒ cfunc" where
"metafunc f ≡ (f ∘⇩c (left_cart_proj (domain f) 𝟭))⇧♯"
lemma metafunc_def2:
assumes "f : X → Y"
shows "metafunc f = (f ∘⇩c (left_cart_proj X 𝟭))⇧♯"
using assms unfolding metafunc_def cfunc_type_def by auto
lemma metafunc_type[type_rule]:
assumes "f : X → Y"
shows "metafunc f ∈⇩c Y⇗X⇖"
using assms by (unfold metafunc_def2, typecheck_cfuncs)
lemma eval_lemma:
assumes f_type[type_rule]: "f : X → Y"
assumes x_type[type_rule]: "x ∈⇩c X"
shows "eval_func Y X ∘⇩c ⟨x, metafunc f⟩ = f ∘⇩c x"
proof -
have "eval_func Y X ∘⇩c ⟨x, metafunc f⟩ = eval_func Y X ∘⇩c (id X ×⇩f (f ∘⇩c (left_cart_proj X 𝟭))⇧♯) ∘⇩c ⟨x, id 𝟭⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 metafunc_def2)
also have "... = (eval_func Y X ∘⇩c (id X ×⇩f (f ∘⇩c (left_cart_proj X 𝟭))⇧♯)) ∘⇩c ⟨x, id 𝟭⟩"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = (f ∘⇩c (left_cart_proj X 𝟭)) ∘⇩c ⟨x, id 𝟭⟩"
by (typecheck_cfuncs, metis transpose_func_def)
also have "... = f ∘⇩c x"
by (typecheck_cfuncs, metis assms cfunc_type_def comp_associative left_cart_proj_cfunc_prod)
finally show "eval_func Y X ∘⇩c ⟨x, metafunc f⟩ = f ∘⇩c x".
qed
subsubsection ‹Inverse Metafunctions (Cnufatems)›
definition cnufatem :: "cfunc ⇒ cfunc" where
"cnufatem f = (THE g. ∀ Y X. f : 𝟭 → Y⇗X⇖ ⟶ g = eval_func Y X ∘⇩c ⟨id X, f ∘⇩c β⇘X⇙⟩)"
lemma cnufatem_def2:
assumes "f ∈⇩c Y⇗X⇖"
shows "cnufatem f = eval_func Y X ∘⇩c ⟨id X, f ∘⇩c β⇘X⇙⟩"
using assms unfolding cnufatem_def cfunc_type_def
by (smt (verit, ccfv_threshold) exp_set_inj theI')
lemma cnufatem_type[type_rule]:
assumes "f ∈⇩c Y⇗X⇖"
shows "cnufatem f : X → Y"
using assms cnufatem_def2
by (auto, typecheck_cfuncs)
lemma cnufatem_metafunc:
assumes f_type[type_rule]: "f : X → Y"
shows "cnufatem (metafunc f) = f"
proof(etcs_rule one_separator)
fix x
assume x_type[type_rule]: "x ∈⇩c X"
have "cnufatem (metafunc f) ∘⇩c x = eval_func Y X ∘⇩c ⟨id X, (metafunc f) ∘⇩c β⇘X⇙⟩ ∘⇩c x"
using cnufatem_def2 comp_associative2 by (typecheck_cfuncs, fastforce)
also have "... = eval_func Y X ∘⇩c ⟨x, (metafunc f)⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left)
also have "... = f ∘⇩c x"
using eval_lemma by (typecheck_cfuncs, presburger)
finally show "cnufatem (metafunc f) ∘⇩c x = f ∘⇩c x".
qed
lemma metafunc_cnufatem:
assumes f_type[type_rule]: "f ∈⇩c Y⇗X⇖"
shows "metafunc (cnufatem f) = f"
proof (etcs_rule same_evals_equal[where X = Y, where A = X], etcs_rule one_separator)
fix x1
assume x1_type[type_rule]: "x1 ∈⇩c X ×⇩c 𝟭"
then obtain x where x_type[type_rule]: "x ∈⇩c X" and x_def: " x1 = ⟨x, id 𝟭⟩"
by (typecheck_cfuncs, metis cart_prod_decomp one_unique_element)
have "(eval_func Y X ∘⇩c id⇩c X ×⇩f metafunc (cnufatem f)) ∘⇩c ⟨x, id 𝟭⟩ =
eval_func Y X ∘⇩c ⟨x , metafunc (cnufatem f)⟩"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 id_right_unit2)
also have "... = (cnufatem f) ∘⇩c x"
using eval_lemma by (typecheck_cfuncs, presburger)
also have "... = (eval_func Y X ∘⇩c ⟨id X, f ∘⇩c β⇘X⇙⟩) ∘⇩c x"
using assms cnufatem_def2 by presburger
also have "... = eval_func Y X ∘⇩c ⟨id X, f ∘⇩c β⇘X⇙⟩ ∘⇩c x"
by (typecheck_cfuncs, metis comp_associative2)
also have "... = eval_func Y X ∘⇩c ⟨id X ∘⇩c x , f ∘⇩c (β⇘X⇙ ∘⇩c x)⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left id_left_unit2 id_right_unit2 terminal_func_comp_elem)
also have "... = eval_func Y X ∘⇩c ⟨id X ∘⇩c x , f ∘⇩c id 𝟭⟩"
by (simp add: terminal_func_comp_elem x_type)
also have "... = eval_func Y X ∘⇩c (id⇩c X ×⇩f f) ∘⇩c ⟨x, id 𝟭⟩"
using cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, force)
also have "... = (eval_func Y X ∘⇩c id⇩c X ×⇩f f) ∘⇩c x1"
by (typecheck_cfuncs, metis comp_associative2 x_def)
ultimately show "(eval_func Y X ∘⇩c id⇩c X ×⇩f metafunc (cnufatem f)) ∘⇩c x1 = (eval_func Y X ∘⇩c id⇩c X ×⇩f f) ∘⇩c x1"
using x_def by simp
qed
subsubsection ‹Metafunction Composition›
definition meta_comp :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
"meta_comp X Y Z = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id(Z⇗Y⇖) ×⇩f (eval_func Y X ∘⇩c swap (Y⇗X⇖) X)) ∘⇩c (associate_right (Z⇗Y⇖) (Y⇗X⇖) X) ∘⇩c swap X ((Z⇗Y⇖) ×⇩c (Y⇗X⇖)))⇧♯"
lemma meta_comp_type[type_rule]:
"meta_comp X Y Z : Z⇗Y⇖ ×⇩c Y⇗X⇖ → Z⇗X⇖"
unfolding meta_comp_def by typecheck_cfuncs
definition meta_comp2 :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "□" 55)
where "meta_comp2 f g = (THE h. ∃ W X Y. g : W → Y⇗X⇖ ∧ h = (f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯)"
lemma meta_comp2_def2:
assumes "f: W → Z⇗Y⇖"
assumes "g: W → Y⇗X⇖"
shows "f □ g = (f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯"
using assms unfolding meta_comp2_def
by (smt (z3) cfunc_type_def exp_set_inj the_equality)
lemma meta_comp2_type[type_rule]:
assumes "f: W → Z⇗Y⇖"
assumes "g: W → Y⇗X⇖"
shows "f □ g : W → Z⇗X⇖"
proof -
have "(f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯ : W → Z⇗X⇖"
using assms by typecheck_cfuncs
then show ?thesis
using assms by (simp add: meta_comp2_def2)
qed
lemma meta_comp2_elements_aux:
assumes "f ∈⇩c Z⇗Y⇖"
assumes "g ∈⇩c Y⇗X⇖"
assumes "x ∈⇩c X"
shows "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩) ∘⇩c ⟨x, id⇩c 𝟭⟩ = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c ⟨x,g⟩,f⟩"
proof-
have "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩) ∘⇩c ⟨x, id⇩c 𝟭⟩= f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩ ∘⇩c ⟨x, id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = f⇧♭ ∘⇩c ⟨g⇧♭ ∘⇩c ⟨x, id⇩c 𝟭⟩,right_cart_proj X 𝟭 ∘⇩c ⟨x, id⇩c 𝟭⟩ ⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp)
also have "... = f⇧♭ ∘⇩c ⟨g⇧♭ ∘⇩c ⟨x, id⇩c 𝟭⟩,id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs, metis one_unique_element)
also have "... = f⇧♭ ∘⇩c ⟨(eval_func Y X) ∘⇩c (id X ×⇩f g) ∘⇩c ⟨x, id⇩c 𝟭⟩,id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3)
also have "... = f⇧♭ ∘⇩c ⟨(eval_func Y X) ∘⇩c ⟨x, g⟩,id⇩c 𝟭⟩"
using assms cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 by (typecheck_cfuncs,force)
also have "... = (eval_func Z Y) ∘⇩c (id Y ×⇩f f) ∘⇩c ⟨(eval_func Y X) ∘⇩c ⟨x, g⟩,id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3)
also have "... = (eval_func Z Y) ∘⇩c ⟨(eval_func Y X) ∘⇩c ⟨x, g⟩,f⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
finally show "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩) ∘⇩c ⟨x,id⇩c 𝟭⟩ = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c ⟨x,g⟩,f⟩".
qed
lemma meta_comp2_def3:
assumes "f ∈⇩c Z⇗Y⇖"
assumes "g ∈⇩c Y⇗X⇖"
shows "f □ g = metafunc ((cnufatem f) ∘⇩c (cnufatem g))"
using assms
proof(unfold meta_comp2_def2 cnufatem_def2 metafunc_def meta_comp_def)
have "f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩ = ((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭"
proof(rule one_separator[where X = "X ×⇩c 𝟭", where Y = Z])
show "f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩ : X ×⇩c 𝟭 → Z"
using assms by typecheck_cfuncs
show "((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭 : X ×⇩c 𝟭 → Z"
using assms by typecheck_cfuncs
next
fix x1
assume x1_type[type_rule]: "x1 ∈⇩c (X ×⇩c 𝟭)"
then obtain x where x_type[type_rule]: "x ∈⇩c X" and x_def: "x1 = ⟨x, id⇩c 𝟭⟩"
by (metis cart_prod_decomp id_type terminal_func_unique)
then have "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩) ∘⇩c x1 = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c ⟨x,g⟩,f⟩"
using assms meta_comp2_elements_aux x_def by blast
also have "... = eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩ ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩ ∘⇩c x"
using assms by (typecheck_cfuncs, metis cart_prod_extract_left)
also have "... = (eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩ ∘⇩c x"
using assms by (typecheck_cfuncs, meson comp_associative2)
also have "... = ((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c x"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭 ∘⇩c x1"
using assms id_type left_cart_proj_cfunc_prod x_def by (typecheck_cfuncs, auto)
also have "... = (((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭) ∘⇩c x1"
using assms by (typecheck_cfuncs, meson comp_associative2)
finally show "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩) ∘⇩c x1 = (((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭) ∘⇩c x1".
qed
then show "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩)⇧♯ = (((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj (domain ((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩)) 𝟭)⇧♯"
using assms cfunc_type_def cnufatem_def2 cnufatem_type domain_comp by force
qed
lemma meta_comp2_def4:
assumes f_type[type_rule]: "f ∈⇩c Z⇗Y⇖" and g_type[type_rule]: "g ∈⇩c Y⇗X⇖"
shows "f □ g = meta_comp X Y Z ∘⇩c ⟨f,g⟩"
using assms
proof(unfold meta_comp2_def2 cnufatem_def2 metafunc_def meta_comp_def)
have "(((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭) =
(eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f (eval_func Y X ∘⇩c swap (Y⇗X⇖) X)) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖)) ∘⇩c (id (X) ×⇩f ⟨f,g⟩)"
proof(etcs_rule one_separator)
fix x1
assume x1_type[type_rule]: "x1 ∈⇩c X ×⇩c 𝟭"
then obtain x where x_type[type_rule]: "x ∈⇩c X" and x_def: "x1 = ⟨x, id⇩c 𝟭⟩"
by (metis cart_prod_decomp id_type terminal_func_unique)
have "(((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭) ∘⇩c x1 =
((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭 ∘⇩c x1"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
also have "... = ((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c x"
using id_type left_cart_proj_cfunc_prod x_def by (typecheck_cfuncs, presburger)
also have "... = (eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩ ∘⇩c x"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
also have "... = eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩ ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩ ∘⇩c x"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
also have "... = eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩ ∘⇩c eval_func Y X ∘⇩c ⟨x ,g⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left)
also have "... = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c ⟨x ,g⟩ ,f⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y) ∘⇩c ⟨f , eval_func Y X ∘⇩c ⟨x, g⟩⟩"
by (typecheck_cfuncs, metis comp_associative2 swap_ap)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y) ∘⇩c ⟨id⇩c (Z⇗Y⇖) ∘⇩c f , (eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c ⟨g, x⟩⟩"
by (typecheck_cfuncs, smt (z3) comp_associative2 id_left_unit2 swap_ap)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y) ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f (eval_func Y X ∘⇩c swap (Y⇗X⇖) X)) ∘⇩c ⟨f,⟨g, x⟩⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X)) ∘⇩c ⟨f,⟨g, x⟩⟩"
using assms comp_associative2 by (typecheck_cfuncs, force)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X)) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c ⟨⟨f,g⟩, x ⟩"
using assms by (typecheck_cfuncs, simp add: associate_right_ap)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X) ∘⇩c ⟨⟨f,g⟩, x ⟩"
using assms comp_associative2 by (typecheck_cfuncs, force)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X) ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖) ∘⇩c ⟨x, ⟨f,g⟩⟩"
using assms by (typecheck_cfuncs, simp add: swap_ap)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖)) ∘⇩c ⟨x, ⟨f,g⟩⟩"
using assms comp_associative2 by (typecheck_cfuncs, force)
also have "... = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖)) ∘⇩c ((id⇩c X ×⇩f ⟨f,g⟩) ∘⇩c x1)"
using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 id_type x_def)
also have "... = ((eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖)) ∘⇩c id⇩c X ×⇩f ⟨f,g⟩) ∘⇩c x1"
by (typecheck_cfuncs, meson comp_associative2)
finally show "(((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c left_cart_proj X 𝟭) ∘⇩c x1 =
((eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖)) ∘⇩c id⇩c X ×⇩f ⟨f,g⟩) ∘⇩c x1".
qed
then have "(((eval_func Z Y ∘⇩c ⟨id⇩c Y,f ∘⇩c β⇘Y⇙⟩) ∘⇩c eval_func Y X ∘⇩c ⟨id⇩c X,g ∘⇩c β⇘X⇙⟩) ∘⇩c
left_cart_proj X 𝟭)⇧♯ = (eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f (eval_func Y X ∘⇩c swap (Y⇗X⇖) X))
∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖))⇧♯ ∘⇩c ⟨f,g⟩"
using assms by (typecheck_cfuncs, simp add: sharp_comp)
then show "(f⇧♭ ∘⇩c ⟨g⇧♭,right_cart_proj X 𝟭⟩)⇧♯ =
(eval_func Z Y ∘⇩c swap (Z⇗Y⇖) Y ∘⇩c (id⇩c (Z⇗Y⇖) ×⇩f eval_func Y X ∘⇩c swap (Y⇗X⇖) X) ∘⇩c associate_right (Z⇗Y⇖) (Y⇗X⇖) X ∘⇩c swap X (Z⇗Y⇖ ×⇩c Y⇗X⇖))⇧♯ ∘⇩c ⟨f,g⟩"
using assms cfunc_type_def cnufatem_def2 cnufatem_type domain_comp meta_comp2_def2 meta_comp2_def3 metafunc_def by force
qed
lemma meta_comp_on_els:
assumes "f : W → Z⇗Y⇖"
assumes "g : W → Y⇗X⇖"
assumes "w ∈⇩c W"
shows "(f □ g) ∘⇩c w = (f ∘⇩c w) □ (g ∘⇩c w)"
proof -
have "(f □ g) ∘⇩c w = (f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯ ∘⇩c w"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
also have "... = (eval_func Z Y ∘⇩c (id Y ×⇩f f) ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f g), right_cart_proj X W⟩)⇧♯ ∘⇩c w"
using assms comp_associative2 inv_transpose_func_def3 by (typecheck_cfuncs, force)
also have "... = (eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f g), f ∘⇩c right_cart_proj X W⟩)⇧♯ ∘⇩c w"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = (eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), (f ∘⇩c w) ∘⇩c right_cart_proj X 𝟭⟩)⇧♯"
proof -
have "(eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f g), f ∘⇩c right_cart_proj X W⟩)⇧♯⇧♭ ∘⇩c (id X ×⇩f w) =
eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), f ∘⇩c right_cart_proj X W ∘⇩c (id X ×⇩f w)⟩"
proof -
have "eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f g), f ∘⇩c right_cart_proj X W⟩ ∘⇩c (id X ×⇩f w)
= eval_func Z Y ∘⇩c ⟨(eval_func Y X ∘⇩c (id X ×⇩f g)) ∘⇩c (id X ×⇩f w), (f ∘⇩c right_cart_proj X W) ∘⇩c (id X ×⇩f w)⟩"
using assms cfunc_prod_comp by (typecheck_cfuncs, force)
also have "... = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f g) ∘⇩c (id X ×⇩f w), f ∘⇩c right_cart_proj X W ∘⇩c (id X ×⇩f w)⟩"
using assms comp_associative2 by (typecheck_cfuncs, auto)
also have "... = eval_func Z Y ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), f ∘⇩c right_cart_proj X W ∘⇩c (id X ×⇩f w)⟩"
using assms by (typecheck_cfuncs, metis identity_distributes_across_composition)
ultimately show ?thesis
using assms comp_associative2 flat_cancels_sharp by (typecheck_cfuncs, auto)
qed
then show ?thesis
using assms by (typecheck_cfuncs, smt (z3) comp_associative2 inv_transpose_func_def3
inv_transpose_of_composition right_cart_proj_cfunc_cross_prod transpose_func_unique)
qed
also have "... = (eval_func Z Y ∘⇩c (id⇩c Y ×⇩f ((f ∘⇩c w) ∘⇩c right_cart_proj X 𝟭)) ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), id (X×⇩c 𝟭)⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (eval_func Z Y ∘⇩c (id⇩c Y ×⇩f (f ∘⇩c w)) ∘⇩c (id (Y) ×⇩f right_cart_proj X 𝟭) ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), id (X×⇩c 𝟭)⟩)⇧♯"
using assms comp_associative2 identity_distributes_across_composition by (typecheck_cfuncs, force)
also have "... = ((f∘⇩cw)⇧♭ ∘⇩c (id (Y) ×⇩f right_cart_proj X 𝟭) ∘⇩c ⟨eval_func Y X ∘⇩c (id X ×⇩f (g∘⇩c w)), id (X×⇩c 𝟭)⟩)⇧♯"
using assms by (typecheck_cfuncs, smt (z3) comp_associative2 inv_transpose_func_def3)
also have "... = ((f∘⇩cw)⇧♭ ∘⇩c (id (Y) ×⇩f right_cart_proj X 𝟭) ∘⇩c ⟨(g∘⇩c w)⇧♭, id (X×⇩c 𝟭)⟩)⇧♯"
using assms inv_transpose_func_def3 by (typecheck_cfuncs, force)
also have "... = ((f∘⇩c w)⇧♭ ∘⇩c ⟨(g∘⇩c w)⇧♭, right_cart_proj X 𝟭⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (f∘⇩c w) □ (g ∘⇩c w)"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
finally show ?thesis.
qed
lemma meta_comp2_def5:
assumes "f : W → Z⇗Y⇖"
assumes "g : W → Y⇗X⇖"
shows "f □ g = meta_comp X Y Z ∘⇩c ⟨f,g⟩"
proof(rule one_separator[where X = W, where Y = "Z⇗X⇖"])
show "f □ g : W → Z⇗X⇖"
using assms by typecheck_cfuncs
show "meta_comp X Y Z ∘⇩c ⟨f,g⟩ : W → Z⇗X⇖"
using assms by typecheck_cfuncs
next
fix w
assume w_type[type_rule]: "w ∈⇩c W"
have "(meta_comp X Y Z ∘⇩c ⟨f,g⟩) ∘⇩c w = meta_comp X Y Z ∘⇩c ⟨f,g⟩ ∘⇩c w"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = meta_comp X Y Z ∘⇩c ⟨f ∘⇩c w, g ∘⇩c w⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp)
also have "... = (f∘⇩c w) □ (g ∘⇩c w)"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def4)
also have "... = (f □ g) ∘⇩c w"
using assms by (typecheck_cfuncs, simp add: meta_comp_on_els)
ultimately show "(f □ g) ∘⇩c w = (meta_comp X Y Z ∘⇩c ⟨f,g⟩) ∘⇩c w"
by simp
qed
lemma meta_left_identity:
assumes "g ∈⇩c X⇗X⇖"
shows "g □ metafunc (id X) = g"
using assms by (typecheck_cfuncs, metis cfunc_type_def cnufatem_metafunc cnufatem_type id_right_unit meta_comp2_def3 metafunc_cnufatem)
lemma meta_right_identity:
assumes "g ∈⇩c X⇗X⇖"
shows "metafunc(id X) □ g = g"
using assms by (typecheck_cfuncs, smt (z3) cnufatem_metafunc cnufatem_type id_left_unit2 meta_comp2_def3 metafunc_cnufatem)
lemma comp_as_metacomp:
assumes "g : X → Y"
assumes "f : Y → Z"
shows "f ∘⇩c g = cnufatem(metafunc f □ metafunc g)"
using assms by (typecheck_cfuncs, simp add: cnufatem_metafunc meta_comp2_def3)
lemma metacomp_as_comp:
assumes "g ∈⇩c Y⇗X⇖"
assumes "f ∈⇩c Z⇗Y⇖"
shows "cnufatem f ∘⇩c cnufatem g = cnufatem(f □ g)"
using assms by (typecheck_cfuncs, simp add: comp_as_metacomp metafunc_cnufatem)
lemma meta_comp_assoc:
assumes "e : W → A⇗Z⇖"
assumes "f : W → Z⇗Y⇖"
assumes "g : W → Y⇗X⇖"
shows "(e □ f) □ g = e □ (f □ g)"
proof -
have "(e □ f) □ g = (e⇧♭ ∘⇩c ⟨f⇧♭, right_cart_proj Y W⟩)⇧♯ □ g"
using assms by (simp add: meta_comp2_def2)
also have "... = ((e⇧♭ ∘⇩c ⟨f⇧♭, right_cart_proj Y W⟩)⇧♯⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
also have "... = ((e⇧♭ ∘⇩c ⟨f⇧♭, right_cart_proj Y W⟩) ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: flat_cancels_sharp)
also have "... = (e⇧♭ ∘⇩c ⟨f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩ ,right_cart_proj X W⟩)⇧♯"
using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 right_cart_proj_cfunc_prod)
also have "... = (e⇧♭ ∘⇩c ⟨(f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯⇧♭ ,right_cart_proj X W⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: flat_cancels_sharp)
also have "... = e □ (f⇧♭ ∘⇩c ⟨g⇧♭, right_cart_proj X W⟩)⇧♯"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
also have "... = e □ (f □ g)"
using assms by (simp add: meta_comp2_def2)
finally show ?thesis.
qed
subsection ‹Partially Parameterized Functions on Pairs›
definition left_param :: "cfunc ⇒ cfunc ⇒ cfunc" ("_⇘[_,-]⇙" [100,0]100) where
"left_param k p ≡ (THE f. ∃ P Q R. k : P ×⇩c Q → R ∧ f = k ∘⇩c ⟨p ∘⇩c β⇘Q⇙, id Q⟩)"
lemma left_param_def2:
assumes "k : P ×⇩c Q → R"
shows "k⇘[p,-]⇙ ≡ k ∘⇩c ⟨p ∘⇩c β⇘Q⇙, id Q⟩"
proof -
have "∃ P Q R. k : P ×⇩c Q → R ∧ left_param k p = k ∘⇩c ⟨p ∘⇩c β⇘Q⇙, id Q⟩"
unfolding left_param_def by (smt (z3) cfunc_type_def the1I2 transpose_func_type assms)
then show "k⇘[p,-]⇙ ≡ k ∘⇩c ⟨p ∘⇩c β⇘Q⇙, id Q⟩"
by (smt (z3) assms cfunc_type_def transpose_func_type)
qed
lemma left_param_type[type_rule]:
assumes "k : P ×⇩c Q → R"
assumes "p ∈⇩c P"
shows "k⇘[p,-]⇙ : Q → R"
using assms by (unfold left_param_def2, typecheck_cfuncs)
lemma left_param_on_el:
assumes "k : P ×⇩c Q → R"
assumes "p ∈⇩c P"
assumes "q ∈⇩c Q"
shows "k⇘[p,-]⇙ ∘⇩c q = k ∘⇩c ⟨p, q⟩"
proof -
have "k⇘[p,-]⇙ ∘⇩c q = k ∘⇩c ⟨p ∘⇩c β⇘Q⇙, id Q⟩ ∘⇩c q"
using assms cfunc_type_def comp_associative left_param_def2 by (typecheck_cfuncs, force)
also have "... = k ∘⇩c ⟨p, q⟩"
using assms(2,3) cart_prod_extract_right by force
finally show ?thesis.
qed
definition right_param :: "cfunc ⇒ cfunc ⇒ cfunc" ("_⇘[-,_]⇙" [100,0]100) where
"right_param k q ≡ (THE f. ∃ P Q R. k : P ×⇩c Q → R ∧ f = k ∘⇩c ⟨id P, q ∘⇩c β⇘P⇙⟩)"
lemma right_param_def2:
assumes "k : P ×⇩c Q → R"
shows "k⇘[-,q]⇙ ≡ k ∘⇩c ⟨id P, q ∘⇩c β⇘P⇙⟩"
proof -
have "∃ P Q R. k : P ×⇩c Q → R ∧ right_param k q = k ∘⇩c ⟨id P, q ∘⇩c β⇘P⇙⟩"
unfolding right_param_def by (rule theI', insert assms, auto, metis cfunc_type_def exp_set_inj transpose_func_type)
then show "k⇘[-,q]⇙ ≡ k ∘⇩c ⟨id⇩c P,q ∘⇩c β⇘P⇙⟩"
by (smt (z3) assms cfunc_type_def exp_set_inj transpose_func_type)
qed
lemma right_param_type[type_rule]:
assumes "k : P ×⇩c Q → R"
assumes "q ∈⇩c Q"
shows "k⇘[-,q]⇙ : P → R"
using assms by (unfold right_param_def2, typecheck_cfuncs)
lemma right_param_on_el:
assumes "k : P ×⇩c Q → R"
assumes "p ∈⇩c P"
assumes "q ∈⇩c Q"
shows "k⇘[-,q]⇙ ∘⇩c p = k ∘⇩c ⟨p, q⟩"
proof -
have "k⇘[-,q]⇙ ∘⇩c p = k ∘⇩c ⟨id P, q ∘⇩c β⇘P⇙⟩ ∘⇩c p"
using assms cfunc_type_def comp_associative right_param_def2 by (typecheck_cfuncs, force)
also have "... = k ∘⇩c ⟨p, q⟩"
using assms(2,3) cart_prod_extract_left by force
finally show ?thesis.
qed
subsection ‹Exponential Set Facts›
text ‹The lemma below corresponds to Proposition 2.5.7 in Halvorson.›
lemma exp_one:
"X⇗𝟭⇖ ≅ X"
proof -
obtain e where e_defn: "e = eval_func X 𝟭" and e_type: "e : 𝟭 ×⇩c X⇗𝟭⇖ → X"
using eval_func_type by auto
obtain i where i_type: "i: 𝟭 ×⇩c 𝟭 → 𝟭"
using terminal_func_type by blast
obtain i_inv where i_iso: "i_inv: 𝟭→ 𝟭 ×⇩c 𝟭 ∧
i ∘⇩c i_inv = id(𝟭) ∧
i_inv ∘⇩c i = id(𝟭 ×⇩c 𝟭)"
by (smt cfunc_cross_prod_comp_cfunc_prod cfunc_cross_prod_comp_diagonal cfunc_cross_prod_def cfunc_prod_type cfunc_type_def diagonal_def i_type id_cross_prod id_left_unit id_type left_cart_proj_type right_cart_proj_cfunc_prod right_cart_proj_type terminal_func_unique)
then have i_inv_type: "i_inv: 𝟭→ 𝟭 ×⇩c 𝟭"
by auto
have inj: "injective(e)"
by (simp add: e_defn eval_func_X_one_injective)
have surj: "surjective(e)"
unfolding surjective_def
proof clarify
fix y
assume "y ∈⇩c codomain e"
then have y_type: "y ∈⇩c X"
using cfunc_type_def e_type by auto
have witness_type: "(id⇩c 𝟭 ×⇩f (y ∘⇩c i)⇧♯) ∘⇩c i_inv ∈⇩c 𝟭 ×⇩c X⇗𝟭⇖"
using y_type i_type i_inv_type by typecheck_cfuncs
have square: "e ∘⇩c (id(𝟭) ×⇩f (y ∘⇩c i)⇧♯) = y ∘⇩c i"
using comp_type e_defn i_type transpose_func_def y_type by blast
then show "∃x. x ∈⇩c domain e ∧ e ∘⇩c x = y"
unfolding cfunc_type_def using y_type i_type i_inv_type e_type
by (intro exI[where x="(id(𝟭) ×⇩f (y ∘⇩c i)⇧♯) ∘⇩c i_inv"], typecheck_cfuncs, metis cfunc_type_def comp_associative i_iso id_right_unit2)
qed
have "isomorphism e"
using epi_mon_is_iso inj injective_imp_monomorphism surj surjective_is_epimorphism by fastforce
then show "X⇗𝟭⇖ ≅ X"
using e_type is_isomorphic_def isomorphic_is_symmetric isomorphic_is_transitive one_x_A_iso_A by blast
qed
text ‹The lemma below corresponds to Proposition 2.5.8 in Halvorson.›
lemma exp_empty:
"X⇗∅⇖ ≅ 𝟭"
proof -
obtain f where f_type: "f = α⇘X⇙∘⇩c (left_cart_proj ∅ 𝟭)" and fsharp_type[type_rule]: "f⇧♯ ∈⇩c X⇗∅⇖"
using transpose_func_type by (typecheck_cfuncs, force)
have uniqueness: "∀z. z ∈⇩c X⇗∅⇖ ⟶ z=f⇧♯"
proof clarify
fix z
assume z_type[type_rule]: "z ∈⇩c X⇗∅⇖"
obtain j where j_iso:"j:∅ → ∅ ×⇩c 𝟭 ∧ isomorphism(j)"
using is_isomorphic_def isomorphic_is_symmetric empty_prod_X by presburger
obtain ψ where psi_type: "ψ : ∅ ×⇩c 𝟭 → ∅ ∧
j ∘⇩c ψ = id(∅ ×⇩c 𝟭) ∧ ψ ∘⇩c j = id(∅)"
using cfunc_type_def isomorphism_def j_iso by fastforce
then have f_sharp : "id(∅)×⇩f z = id(∅)×⇩f f⇧♯"
by (typecheck_cfuncs, meson comp_type emptyset_is_empty one_separator)
then show "z = f⇧♯"
using fsharp_type same_evals_equal z_type by force
qed
then have "∃! x. x ∈⇩c X⇗∅⇖"
by (intro ex1I[where a="f⇧♯"], simp_all add: fsharp_type)
then show "X⇗∅⇖ ≅ 𝟭"
using single_elem_iso_one by auto
qed
lemma one_exp:
"𝟭⇗X⇖ ≅ 𝟭"
proof -
have nonempty: "nonempty(𝟭⇗X⇖)"
using nonempty_def right_cart_proj_type transpose_func_type by blast
obtain e where e_defn: "e = eval_func 𝟭 X" and e_type: "e : X ×⇩c 𝟭⇗X⇖ → 𝟭"
by (simp add: eval_func_type)
have uniqueness: "∀y. (y∈⇩c 𝟭⇗X⇖ ⟶ e ∘⇩c (id(X) ×⇩f y) : X ×⇩c 𝟭 → 𝟭)"
by (meson cfunc_cross_prod_type comp_type e_type id_type)
have uniquess_form: "∀y. (y∈⇩c 𝟭⇗X⇖ ⟶ e ∘⇩c (id(X) ×⇩f y) = β⇘X ×⇩c 𝟭⇙)"
using terminal_func_unique uniqueness by blast
then have ex1: "(∃! x. x ∈⇩c 𝟭⇗X⇖)"
by (metis e_defn nonempty nonempty_def transpose_func_unique uniqueness)
show "𝟭⇗X⇖ ≅ 𝟭"
using ex1 single_elem_iso_one by auto
qed
text ‹The lemma below corresponds to Proposition 2.5.9 in Halvorson.›
lemma power_rule:
"(X ×⇩c Y)⇗A⇖ ≅ X⇗A⇖ ×⇩c Y⇗A⇖"
proof -
have "is_cart_prod ((X ×⇩c Y)⇗A⇖) ((left_cart_proj X Y)⇗A⇖⇩f) (right_cart_proj X Y⇗A⇖⇩f) (X⇗A⇖) (Y⇗A⇖)"
proof (etcs_subst is_cart_prod_def2, clarify)
fix f g Z
assume f_type[type_rule]: "f : Z → X⇗A⇖"
assume g_type[type_rule]: "g : Z → Y⇗A⇖"
show "∃h. h : Z → (X ×⇩c Y)⇗A⇖ ∧
left_cart_proj X Y⇗A⇖⇩f ∘⇩c h = f ∧
right_cart_proj X Y⇗A⇖⇩f ∘⇩c h = g ∧
(∀h2. h2 : Z → (X ×⇩c Y)⇗A⇖ ∧ left_cart_proj X Y⇗A⇖⇩f ∘⇩c h2 = f ∧ right_cart_proj X Y⇗A⇖⇩f ∘⇩c h2 = g ⟶
h2 = h)"
proof (intro exI[where x="⟨f⇧♭ ,g⇧♭⟩⇧♯"], safe, typecheck_cfuncs)
have "((left_cart_proj X Y)⇗A⇖⇩f) ∘⇩c ⟨f⇧♭ ,g⇧♭⟩⇧♯ = ((left_cart_proj X Y) ∘⇩c ⟨f⇧♭ ,g⇧♭⟩)⇧♯"
by (typecheck_cfuncs, metis transpose_of_comp)
also have "... = f⇧♭⇧♯"
by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod)
also have "... = f"
by (typecheck_cfuncs, simp add: sharp_cancels_flat)
finally show projection_property1: "((left_cart_proj X Y)⇗A⇖⇩f) ∘⇩c ⟨f⇧♭ ,g⇧♭⟩⇧♯ = f".
show projection_property2: "((right_cart_proj X Y)⇗A⇖⇩f) ∘⇩c ⟨f⇧♭ ,g⇧♭⟩⇧♯ = g"
by (typecheck_cfuncs, metis right_cart_proj_cfunc_prod sharp_cancels_flat transpose_of_comp)
show "⋀h2. h2 : Z → (X ×⇩c Y)⇗A⇖ ⟹
f = left_cart_proj X Y⇗A⇖⇩f ∘⇩c h2 ⟹
g = right_cart_proj X Y⇗A⇖⇩f ∘⇩c h2 ⟹
h2 = ⟨(left_cart_proj X Y⇗A⇖⇩f ∘⇩c h2)⇧♭,(right_cart_proj X Y⇗A⇖⇩f ∘⇩c h2)⇧♭⟩⇧♯"
proof -
fix h
assume h_type[type_rule]: "h : Z → (X ×⇩c Y)⇗A⇖"
assume h_property1: "f = ((left_cart_proj X Y)⇗A⇖⇩f) ∘⇩c h"
assume h_property2: "g = ((right_cart_proj X Y)⇗A⇖⇩f) ∘⇩c h"
have "f = (left_cart_proj X Y)⇗A⇖⇩f ∘⇩c h⇧♭⇧♯"
by (metis h_property1 h_type sharp_cancels_flat)
also have "... = ((left_cart_proj X Y) ∘⇩c h⇧♭)⇧♯"
by (typecheck_cfuncs, simp add: transpose_of_comp)
ultimately have computation1: "f = ((left_cart_proj X Y) ∘⇩c h⇧♭)⇧♯"
by simp
then have unqiueness1: "(left_cart_proj X Y) ∘⇩c h⇧♭ = f⇧♭"
by (typecheck_cfuncs, simp add: flat_cancels_sharp)
have "g = ((right_cart_proj X Y)⇗A⇖⇩f) ∘⇩c (h⇧♭)⇧♯"
by (metis h_property2 h_type sharp_cancels_flat)
have "... = ((right_cart_proj X Y) ∘⇩c h⇧♭)⇧♯"
by (typecheck_cfuncs, metis transpose_of_comp)
have computation2: "g = ((right_cart_proj X Y) ∘⇩c h⇧♭)⇧♯"
by (simp add: ‹g = right_cart_proj X Y⇗A⇖⇩f ∘⇩c h⇧♭⇧♯› ‹right_cart_proj X Y⇗A⇖⇩f ∘⇩c h⇧♭⇧♯ = (right_cart_proj X Y ∘⇩c h⇧♭)⇧♯›)
then have unqiueness2: "(right_cart_proj X Y) ∘⇩c h⇧♭ = g⇧♭"
using h_type g_type by (typecheck_cfuncs, simp add: computation2 flat_cancels_sharp)
then have h_flat: "h⇧♭ = ⟨f⇧♭, g⇧♭⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_unique unqiueness1 unqiueness2)
then have h_is_sharp_prod_fflat_gflat: "h = ⟨f⇧♭, g⇧♭⟩⇧♯"
by (metis h_type sharp_cancels_flat)
then show "h = ⟨(left_cart_proj X Y⇗A⇖⇩f ∘⇩c h)⇧♭,(right_cart_proj X Y⇗A⇖⇩f ∘⇩c h)⇧♭⟩⇧♯"
using h_property1 h_property2 by force
qed
qed
qed
then show "(X ×⇩c Y)⇗A⇖ ≅ X⇗A⇖ ×⇩c Y⇗A⇖"
using canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def by fastforce
qed
lemma exponential_coprod_distribution:
"Z⇗(X ∐ Y)⇖ ≅ (Z⇗X⇖) ×⇩c (Z⇗Y⇖)"
proof -
have "is_cart_prod (Z⇗(X ∐ Y)⇖) ((eval_func Z (X ∐ Y) ∘⇩c (left_coproj X Y) ×⇩f (id(Z⇗(X ∐ Y)⇖)) )⇧♯) ((eval_func Z (X ∐ Y) ∘⇩c (right_coproj X Y) ×⇩f (id(Z⇗(X ∐ Y)⇖)) )⇧♯) (Z⇗X⇖) (Z⇗Y⇖)"
proof (etcs_subst is_cart_prod_def2, clarify)
fix f g H
assume f_type[type_rule]: "f : H → Z⇗X⇖"
assume g_type[type_rule]: "g : H → Z⇗Y⇖"
show "∃h. h : H → Z⇗(X ∐ Y)⇖ ∧
(eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h = f ∧
(eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h = g ∧
(∀h2. h2 : H → Z⇗(X ∐ Y)⇖ ∧
(eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h2 = f ∧
(eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h2 = g ⟶
h2 = h)"
proof (intro exI[where x="(f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯"], safe, typecheck_cfuncs)
have "(eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯ =
((eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖)) ∘⇩c (id X ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯))⇧♯"
using sharp_comp by (typecheck_cfuncs, blast)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c (left_coproj X Y ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯))⇧♯"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c (id (X ∐ Y) ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯) ∘⇩c (left_coproj X Y ×⇩f id H))⇧♯"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
also have "... = (f⇧♭ ⨿ g⇧♭ ∘⇩c (dist_prod_coprod_right X Y H ∘⇩c left_coproj X Y ×⇩f id H))⇧♯"
using comp_associative2 transpose_func_def by (typecheck_cfuncs, force)
also have "... = (f⇧♭ ⨿ g⇧♭ ∘⇩c left_coproj (X ×⇩c H) (Y ×⇩c H))⇧♯"
by (simp add: dist_prod_coprod_right_left_coproj)
also have "... = f"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod sharp_cancels_flat)
finally show "(eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯ = f".
next
have "(eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯ =
((eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖)) ∘⇩c (id Y ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯))⇧♯"
using sharp_comp by (typecheck_cfuncs, blast)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c (right_coproj X Y ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯))⇧♯"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c (id (X ∐ Y) ×⇩f (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯) ∘⇩c (right_coproj X Y ×⇩f id H))⇧♯"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
also have "... = (f⇧♭ ⨿ g⇧♭ ∘⇩c (dist_prod_coprod_right X Y H ∘⇩c right_coproj X Y ×⇩f id H))⇧♯"
using comp_associative2 transpose_func_def by (typecheck_cfuncs, force)
also have "... = (f⇧♭ ⨿ g⇧♭ ∘⇩c right_coproj (X ×⇩c H) (Y ×⇩c H))⇧♯"
by (simp add: dist_prod_coprod_right_right_coproj)
also have "... = g"
by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod sharp_cancels_flat)
finally show "(eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H)⇧♯ = g".
next
fix h
assume h_type[type_rule]: "h : H → Z⇗(X ∐ Y)⇖"
assume f_eqs: "f = (eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h"
assume g_eqs: "g = (eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h"
have "(f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H) = h⇧♭"
proof(etcs_rule one_separator[where X = "(X ∐ Y) ×⇩c H", where Y = Z])
show "⋀xyh. xyh ∈⇩c (X ∐ Y) ×⇩c H ⟹ (f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H) ∘⇩c xyh = h⇧♭ ∘⇩c xyh"
proof-
fix xyh
assume l_type[type_rule]: "xyh ∈⇩c (X ∐ Y) ×⇩c H"
then obtain xy and z where xy_type[type_rule]: "xy ∈⇩c X ∐ Y" and z_type[type_rule]: "z ∈⇩c H"
and xyh_def: "xyh = ⟨xy,z⟩"
using cart_prod_decomp by blast
show "(f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H) ∘⇩c xyh = h⇧♭ ∘⇩c xyh"
proof(cases "∃x. x ∈⇩c X ∧ xy = left_coproj X Y ∘⇩c x")
assume "∃x. x ∈⇩c X ∧ xy = left_coproj X Y ∘⇩c x"
then obtain x where x_type[type_rule]: "x ∈⇩c X" and xy_def: "xy = left_coproj X Y ∘⇩c x"
by blast
have "(f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H) ∘⇩c xyh = (f⇧♭ ⨿ g⇧♭) ∘⇩c (dist_prod_coprod_right X Y H ∘⇩c ⟨left_coproj X Y ∘⇩c x,z⟩)"
by (typecheck_cfuncs, simp add: comp_associative2 xy_def xyh_def)
also have "... = (f⇧♭ ⨿ g⇧♭) ∘⇩c ((dist_prod_coprod_right X Y H ∘⇩c (left_coproj X Y ×⇩f id H)) ∘⇩c ⟨x,z⟩)"
using dist_prod_coprod_right_ap_left dist_prod_coprod_right_left_coproj by (typecheck_cfuncs, presburger)
also have "... = (f⇧♭ ⨿ g⇧♭) ∘⇩c (left_coproj (X ×⇩c H) (Y ×⇩c H) ∘⇩c ⟨x,z⟩)"
using dist_prod_coprod_right_left_coproj by presburger
also have "... = f⇧♭ ∘⇩c ⟨x,z⟩"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
also have "... = ((eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h)⇧♭ ∘⇩c ⟨x,z⟩"
using f_eqs by fastforce
also have "... = (((eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯⇧♭) ∘⇩c (id X ×⇩f h)) ∘⇩c ⟨x,z⟩"
using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
also have "... = ((eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖)) ∘⇩c (id X ×⇩f h)) ∘⇩c ⟨x,z⟩"
by (typecheck_cfuncs, simp add: flat_cancels_sharp)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f h) ∘⇩c ⟨x,z⟩"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
also have "... = eval_func Z (X ∐ Y) ∘⇩c ⟨left_coproj X Y ∘⇩c x, h ∘⇩c z⟩"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2)
also have "... = eval_func Z (X ∐ Y) ∘⇩c ((id(X ∐ Y) ×⇩f h) ∘⇩c ⟨xy,z⟩)"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 xy_def)
also have "... = h⇧♭ ∘⇩c xyh"
by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3 xyh_def)
finally show ?thesis.
next
assume "∄x. x ∈⇩c X ∧ xy = left_coproj X Y ∘⇩c x"
then obtain y where y_type[type_rule]: "y ∈⇩c Y" and xy_def: "xy = right_coproj X Y ∘⇩c y"
using coprojs_jointly_surj by (typecheck_cfuncs, blast)
have "(f⇧♭ ⨿ g⇧♭ ∘⇩c dist_prod_coprod_right X Y H) ∘⇩c xyh = (f⇧♭ ⨿ g⇧♭) ∘⇩c (dist_prod_coprod_right X Y H ∘⇩c ⟨right_coproj X Y ∘⇩c y,z⟩)"
by (typecheck_cfuncs, simp add: comp_associative2 xy_def xyh_def)
also have "... = (f⇧♭ ⨿ g⇧♭) ∘⇩c ((dist_prod_coprod_right X Y H ∘⇩c (right_coproj X Y ×⇩f id H)) ∘⇩c ⟨y,z⟩)"
using dist_prod_coprod_right_ap_right dist_prod_coprod_right_right_coproj by (typecheck_cfuncs, presburger)
also have "... = (f⇧♭ ⨿ g⇧♭) ∘⇩c (right_coproj (X ×⇩c H) (Y ×⇩c H) ∘⇩c ⟨y,z⟩)"
using dist_prod_coprod_right_right_coproj by presburger
also have "... = g⇧♭ ∘⇩c ⟨y,z⟩"
by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
also have "... = ((eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h)⇧♭ ∘⇩c ⟨y,z⟩"
using g_eqs by fastforce
also have "... = (((eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯⇧♭) ∘⇩c (id Y ×⇩f h)) ∘⇩c ⟨y,z⟩"
using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
also have "... = ((eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖)) ∘⇩c (id Y ×⇩f h)) ∘⇩c ⟨y,z⟩"
by (typecheck_cfuncs, simp add: flat_cancels_sharp)
also have "... = (eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f h) ∘⇩c ⟨y,z⟩"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
also have "... = eval_func Z (X ∐ Y) ∘⇩c ⟨right_coproj X Y ∘⇩c y, h ∘⇩c z⟩"
by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2)
also have "... = eval_func Z (X ∐ Y) ∘⇩c ((id(X ∐ Y) ×⇩f h) ∘⇩c ⟨xy,z⟩)"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 xy_def)
also have "... = h⇧♭ ∘⇩c xyh"
by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3 xyh_def)
finally show ?thesis.
qed
qed
qed
then show "h = (((eval_func Z (X ∐ Y) ∘⇩c left_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h)⇧♭ ⨿
((eval_func Z (X ∐ Y) ∘⇩c right_coproj X Y ×⇩f id⇩c (Z⇗(X ∐ Y)⇖))⇧♯ ∘⇩c h)⇧♭ ∘⇩c
dist_prod_coprod_right X Y H)⇧♯"
using f_eqs g_eqs h_type sharp_cancels_flat by force
qed
qed
then show ?thesis
by (metis canonical_cart_prod_is_cart_prod cart_prods_isomorphic is_isomorphic_def prod.sel(1,2))
qed
lemma empty_exp_nonempty:
assumes "nonempty X"
shows "∅⇗X⇖ ≅ ∅"
proof-
obtain j where j_type[type_rule]: "j: ∅⇗X⇖ → 𝟭×⇩c ∅⇗X⇖" and j_def: "isomorphism(j)"
using is_isomorphic_def isomorphic_is_symmetric one_x_A_iso_A by blast
obtain y where y_type[type_rule]: "y ∈⇩c X"
using assms nonempty_def by blast
obtain e where e_type[type_rule]: "e: X×⇩c ∅⇗X⇖ → ∅"
using eval_func_type by blast
have iso_type[type_rule]: "(e ∘⇩c y ×⇩f id(∅⇗X⇖)) ∘⇩c j : ∅⇗X⇖ → ∅"
by typecheck_cfuncs
show "∅⇗X⇖ ≅ ∅"
using function_to_empty_is_iso is_isomorphic_def iso_type by blast
qed
lemma exp_pres_iso_left:
assumes "A ≅ X"
shows "A⇗Y⇖ ≅ X⇗Y⇖"
proof -
obtain φ where φ_def: "φ: X → A ∧ isomorphism(φ)"
using assms is_isomorphic_def isomorphic_is_symmetric by blast
obtain ψ where ψ_def: "ψ: A → X ∧ isomorphism(ψ) ∧ (ψ ∘⇩c φ = id(X))"
using φ_def cfunc_type_def isomorphism_def by fastforce
have idA: "φ ∘⇩c ψ = id(A)"
by (metis φ_def ψ_def cfunc_type_def comp_associative id_left_unit2 isomorphism_def)
have phi_eval_type: "(φ ∘⇩c eval_func X Y)⇧♯: X⇗Y⇖ → A⇗Y⇖"
using φ_def by (typecheck_cfuncs, blast)
have psi_eval_type: "(ψ ∘⇩c eval_func A Y)⇧♯: A⇗Y⇖ → X⇗Y⇖"
using ψ_def by (typecheck_cfuncs, blast)
have idXY: "(ψ ∘⇩c eval_func A Y)⇧♯ ∘⇩c (φ ∘⇩c eval_func X Y)⇧♯ = id(X⇗Y⇖)"
proof -
have "(ψ ∘⇩c eval_func A Y)⇧♯ ∘⇩c (φ ∘⇩c eval_func X Y)⇧♯ = ψ⇗Y⇖⇩f ∘⇩c φ⇗Y⇖⇩f"
using φ_def ψ_def exp_func_def2 by auto
also have "... = (ψ ∘⇩c φ)⇗Y⇖⇩f"
by (metis φ_def ψ_def transpose_factors)
also have "... = (id X)⇗Y⇖⇩f"
by (simp add: ψ_def)
also have "... = id(X⇗Y⇖)"
by (simp add: exponential_object_identity2)
finally show "(ψ ∘⇩c eval_func A Y)⇧♯ ∘⇩c (φ ∘⇩c eval_func X Y)⇧♯ = id(X⇗Y⇖)".
qed
have idAY: "(φ ∘⇩c eval_func X Y)⇧♯ ∘⇩c (ψ ∘⇩c eval_func A Y)⇧♯ = id(A⇗Y⇖)"
proof -
have "(φ ∘⇩c eval_func X Y)⇧♯ ∘⇩c (ψ ∘⇩c eval_func A Y)⇧♯ = φ⇗Y⇖⇩f ∘⇩c ψ⇗Y⇖⇩f"
using φ_def ψ_def exp_func_def2 by auto
also have "... = (φ ∘⇩c ψ)⇗Y⇖⇩f"
by (metis φ_def ψ_def transpose_factors)
also have "... = (id A)⇗Y⇖⇩f"
by (simp add: idA)
also have "... = id(A⇗Y⇖)"
by (simp add: exponential_object_identity2)
finally show "(φ ∘⇩c eval_func X Y)⇧♯ ∘⇩c (ψ ∘⇩c eval_func A Y)⇧♯ = id(A⇗Y⇖)".
qed
show "A⇗Y⇖ ≅ X⇗Y⇖"
by (metis cfunc_type_def comp_epi_imp_epi comp_monic_imp_monic epi_mon_is_iso idAY idXY id_isomorphism is_isomorphic_def iso_imp_epi_and_monic phi_eval_type psi_eval_type)
qed
lemma expset_power_tower:
"(A⇗B⇖)⇗C⇖ ≅ A⇗(B×⇩c C)⇖"
proof -
obtain φ where φ_def: "φ = ((eval_func A (B×⇩c C)) ∘⇩c (associate_left B C (A⇗(B×⇩c C)⇖)))" and
φ_type[type_rule]: "φ: B ×⇩c (C×⇩c (A⇗(B×⇩c C)⇖)) → A" and
φdbsharp_type[type_rule]: "(φ⇧♯)⇧♯ : (A⇗(B×⇩c C)⇖) → ((A⇗B⇖)⇗C⇖)"
using transpose_func_type by (typecheck_cfuncs, fastforce)
obtain ψ where ψ_def: "ψ = (eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C) ∘⇩c (associate_right B C ((A⇗B⇖)⇗C⇖))" and
ψ_type[type_rule]: "ψ : (B ×⇩c C) ×⇩c ((A⇗B⇖)⇗C⇖) → A" and
ψsharp_type[type_rule]: "ψ⇧♯: (A⇗B⇖)⇗C⇖ → (A⇗(B×⇩c C)⇖)"
using transpose_func_type by (typecheck_cfuncs, blast)
have "φ⇧♯⇧♯ ∘⇩c ψ⇧♯ = id((A⇗B⇖)⇗C⇖)"
proof(etcs_rule same_evals_equal[where X = "(A⇗B⇖)", where A = "C"])
show "eval_func (A⇗B⇖) C ∘⇩c id⇩c C ×⇩f φ⇧♯⇧♯ ∘⇩c ψ⇧♯ =
eval_func (A⇗B⇖) C ∘⇩c id⇩c C ×⇩f id⇩c (A⇗B⇖⇗C⇖)"
proof(etcs_rule same_evals_equal[where X = "A", where A = "B"])
show "eval_func A B ∘⇩c id⇩c B ×⇩f (eval_func (A⇗B⇖) C ∘⇩c (id⇩c C ×⇩f φ⇧♯⇧♯ ∘⇩c ψ⇧♯)) =
eval_func A B ∘⇩c id⇩c B ×⇩f eval_func (A⇗B⇖) C ∘⇩c id⇩c C ×⇩f id⇩c (A⇗B⇖⇗C⇖)"
proof -
have "eval_func A B ∘⇩c id⇩c B ×⇩f (eval_func (A⇗B⇖) C ∘⇩c (id⇩c C ×⇩f φ⇧♯⇧♯ ∘⇩c ψ⇧♯)) =
eval_func A B ∘⇩c id⇩c B ×⇩f (eval_func (A⇗B⇖) C ∘⇩c (id⇩c C ×⇩f φ⇧♯⇧♯) ∘⇩c (id⇩c C ×⇩f ψ⇧♯))"
by (typecheck_cfuncs, metis identity_distributes_across_composition)
also have "... = eval_func A B ∘⇩c id⇩c B ×⇩f ((eval_func (A⇗B⇖) C ∘⇩c (id⇩c C ×⇩f φ⇧♯⇧♯)) ∘⇩c (id⇩c C ×⇩f ψ⇧♯))"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = eval_func A B ∘⇩c id⇩c B ×⇩f (φ⇧♯ ∘⇩c (id⇩c C ×⇩f ψ⇧♯))"
by (typecheck_cfuncs, simp add: transpose_func_def)
also have "... = eval_func A B ∘⇩c ((id⇩c B ×⇩f φ⇧♯) ∘⇩c (id⇩c B ×⇩f (id⇩c C ×⇩f ψ⇧♯)))"
using identity_distributes_across_composition by (typecheck_cfuncs, auto)
also have "... = (eval_func A B ∘⇩c ((id⇩c B ×⇩f φ⇧♯))) ∘⇩c (id⇩c B ×⇩f (id⇩c C ×⇩f ψ⇧♯))"
using comp_associative2 by (typecheck_cfuncs,blast)
also have "... = φ ∘⇩c (id⇩c B ×⇩f (id⇩c C ×⇩f ψ⇧♯))"
by (typecheck_cfuncs, simp add: transpose_func_def)
also have "... = ((eval_func A (B×⇩c C)) ∘⇩c (associate_left B C (A⇗(B×⇩c C)⇖))) ∘⇩c (id⇩c B ×⇩f (id⇩c C ×⇩f ψ⇧♯))"
by (simp add: φ_def)
also have "... = (eval_func A (B×⇩c C)) ∘⇩c (associate_left B C (A⇗(B×⇩c C)⇖)) ∘⇩c (id⇩c B ×⇩f (id⇩c C ×⇩f ψ⇧♯))"
using comp_associative2 by (typecheck_cfuncs, auto)
also have "... = (eval_func A (B×⇩c C)) ∘⇩c ((id⇩c B ×⇩f id⇩c C) ×⇩f ψ⇧♯) ∘⇩c associate_left B C ((A⇗B⇖)⇗C⇖)"
by (typecheck_cfuncs, simp add: associate_left_crossprod_ap)
also have "... = (eval_func A (B×⇩c C)) ∘⇩c ((id⇩c (B ×⇩c C)) ×⇩f ψ⇧♯) ∘⇩c associate_left B C ((A⇗B⇖)⇗C⇖)"
by (simp add: id_cross_prod)
also have "... = ψ ∘⇩c associate_left B C ((A⇗B⇖)⇗C⇖)"
by (typecheck_cfuncs, simp add: comp_associative2 transpose_func_def)
also have "... = ((eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C)) ∘⇩c ((associate_right B C ((A⇗B⇖)⇗C⇖))∘⇩c associate_left B C ((A⇗B⇖)⇗C⇖))"
by (typecheck_cfuncs, simp add: ψ_def cfunc_type_def comp_associative)
also have "... = ((eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C)) ∘⇩c id(B ×⇩c (C ×⇩c ((A⇗B⇖)⇗C⇖)))"
by (simp add: right_left)
also have "... = (eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C)"
by (typecheck_cfuncs, meson id_right_unit2)
also have "... = eval_func A B ∘⇩c id⇩c B ×⇩f eval_func (A⇗B⇖) C ∘⇩c id⇩c C ×⇩f id⇩c (A⇗B⇖⇗C⇖)"
by (typecheck_cfuncs, simp add: id_cross_prod id_right_unit2)
finally show ?thesis.
qed
qed
qed
have "ψ⇧♯ ∘⇩c φ⇧♯⇧♯ = id(A⇗(B ×⇩c C)⇖)"
proof(etcs_rule same_evals_equal[where X = "A", where A = "(B ×⇩c C)"])
show "eval_func A (B ×⇩c C) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f (ψ⇧♯ ∘⇩c φ⇧♯⇧♯)) =
eval_func A (B ×⇩c C) ∘⇩c id⇩c (B ×⇩c C) ×⇩f id⇩c (A⇗(B ×⇩c C)⇖)"
proof -
have "eval_func A (B ×⇩c C) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f (ψ⇧♯ ∘⇩c φ⇧♯⇧♯)) =
eval_func A (B ×⇩c C) ∘⇩c ((id⇩c (B ×⇩c C) ×⇩f (ψ⇧♯)) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f φ⇧♯⇧♯))"
by (typecheck_cfuncs, simp add: identity_distributes_across_composition)
also have "... = ( eval_func A (B ×⇩c C) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f (ψ⇧♯))) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f φ⇧♯⇧♯)"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = ψ ∘⇩c (id⇩c (B ×⇩c C) ×⇩f φ⇧♯⇧♯)"
by (typecheck_cfuncs, simp add: transpose_func_def)
also have "... =(eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C) ∘⇩c (associate_right B C ((A⇗B⇖)⇗C⇖)) ∘⇩c (id⇩c (B ×⇩c C) ×⇩f φ⇧♯⇧♯)"
by (typecheck_cfuncs, smt ψ_def cfunc_type_def comp_associative domain_comp)
also have "... =(eval_func A B) ∘⇩c (id(B)×⇩f eval_func (A⇗B⇖) C) ∘⇩c (associate_right B C ((A⇗B⇖)⇗C⇖)) ∘⇩c ((id⇩c (B) ×⇩f id( C)) ×⇩f φ⇧♯⇧♯)"
by (typecheck_cfuncs, simp add: id_cross_prod)
also have "... =(eval_func A B) ∘⇩c ((id(B)×⇩f eval_func (A⇗B⇖) C) ∘⇩c ((id⇩c (B) ×⇩f (id(C) ×⇩f φ⇧♯⇧♯)) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))))"
using associate_right_crossprod_ap by (typecheck_cfuncs, auto)
also have "... =(eval_func A B) ∘⇩c ((id(B)×⇩f eval_func (A⇗B⇖) C) ∘⇩c (id⇩c (B) ×⇩f (id(C) ×⇩f φ⇧♯⇧♯))) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... =(eval_func A B) ∘⇩c (id(B)×⇩f ((eval_func (A⇗B⇖) C)∘⇩c (id(C) ×⇩f φ⇧♯⇧♯))) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))"
using identity_distributes_across_composition by (typecheck_cfuncs, auto)
also have "... =(eval_func A B) ∘⇩c (id(B)×⇩f φ⇧♯) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))"
by (typecheck_cfuncs, simp add: transpose_func_def)
also have "... =((eval_func A B) ∘⇩c (id(B)×⇩f φ⇧♯)) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = φ ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖))"
by (typecheck_cfuncs, simp add: transpose_func_def)
also have "... = (eval_func A (B×⇩c C)) ∘⇩c ((associate_left B C (A⇗(B×⇩c C)⇖)) ∘⇩c (associate_right B C (A⇗(B ×⇩c C)⇖)))"
by (typecheck_cfuncs, simp add: φ_def comp_associative2)
also have "... = eval_func A (B×⇩c C) ∘⇩c id ((B ×⇩c C) ×⇩c (A⇗(B×⇩c C)⇖))"
by (typecheck_cfuncs, simp add: left_right)
also have "... = eval_func A (B ×⇩c C) ∘⇩c id⇩c (B ×⇩c C) ×⇩f id⇩c (A⇗(B ×⇩c C)⇖)"
by (typecheck_cfuncs, simp add: id_cross_prod)
finally show ?thesis.
qed
qed
show ?thesis
by (metis ‹φ⇧♯⇧♯ ∘⇩c ψ⇧♯ = id⇩c (A⇗B⇖⇗C⇖)› ‹ψ⇧♯ ∘⇩c φ⇧♯⇧♯ = id⇩c (A⇗(B ×⇩c C)⇖)› φdbsharp_type ψsharp_type cfunc_type_def is_isomorphic_def isomorphism_def)
qed
lemma exp_pres_iso_right:
assumes "A ≅ X"
shows "Y⇗A⇖ ≅ Y⇗X⇖"
proof -
obtain φ where φ_def: "φ: X → A ∧ isomorphism(φ)"
using assms is_isomorphic_def isomorphic_is_symmetric by blast
obtain ψ where ψ_def: "ψ: A → X ∧ isomorphism(ψ) ∧ (ψ ∘⇩c φ = id(X))"
using φ_def cfunc_type_def isomorphism_def by fastforce
have idA: "φ ∘⇩c ψ = id(A)"
by (metis φ_def ψ_def cfunc_type_def comp_associative id_left_unit2 isomorphism_def)
obtain f where f_def: "f = (eval_func Y X) ∘⇩c (ψ ×⇩f id(Y⇗X⇖))" and f_type[type_rule]: "f: A×⇩c (Y⇗X⇖) → Y" and fsharp_type[type_rule]: "f⇧♯ : Y⇗X⇖ → Y⇗A⇖"
using ψ_def transpose_func_type by (typecheck_cfuncs, presburger)
obtain g where g_def: "g = (eval_func Y A) ∘⇩c (φ ×⇩f id(Y⇗A⇖))" and g_type[type_rule]: "g: X×⇩c (Y⇗A⇖) → Y" and gsharp_type[type_rule]: "g⇧♯ : Y⇗A⇖ → Y⇗X⇖"
using φ_def transpose_func_type by (typecheck_cfuncs, presburger)
have fsharp_gsharp_id: "f⇧♯ ∘⇩c g⇧♯ = id(Y⇗A⇖)"
proof(etcs_rule same_evals_equal[where X = Y, where A = A])
have "eval_func Y A ∘⇩c id⇩c A ×⇩f f⇧♯ ∘⇩c g⇧♯ = eval_func Y A ∘⇩c (id⇩c A ×⇩f f⇧♯) ∘⇩c (id⇩c A ×⇩f g⇧♯)"
using fsharp_type gsharp_type identity_distributes_across_composition by auto
also have "... = eval_func Y X ∘⇩c (ψ ×⇩f id(Y⇗X⇖)) ∘⇩c (id⇩c A ×⇩f g⇧♯)"
using ψ_def cfunc_type_def comp_associative f_def f_type gsharp_type transpose_func_def by (typecheck_cfuncs, smt)
also have "... = eval_func Y X ∘⇩c (ψ ×⇩f g⇧♯)"
by (smt ψ_def cfunc_cross_prod_comp_cfunc_cross_prod gsharp_type id_left_unit2 id_right_unit2 id_type)
also have "... = eval_func Y X ∘⇩c (id X ×⇩f g⇧♯) ∘⇩c (ψ ×⇩f id(Y⇗A⇖))"
by (smt ψ_def cfunc_cross_prod_comp_cfunc_cross_prod gsharp_type id_left_unit2 id_right_unit2 id_type)
also have "... = eval_func Y A ∘⇩c (φ ×⇩f id(Y⇗A⇖)) ∘⇩c (ψ ×⇩f id(Y⇗A⇖))"
by (typecheck_cfuncs, smt φ_def ψ_def comp_associative2 flat_cancels_sharp g_def g_type inv_transpose_func_def3)
also have "... = eval_func Y A ∘⇩c ((φ ∘⇩c ψ) ×⇩f (id(Y⇗A⇖) ∘⇩c id(Y⇗A⇖)))"
using φ_def ψ_def cfunc_cross_prod_comp_cfunc_cross_prod by (typecheck_cfuncs, auto)
also have "... = eval_func Y A ∘⇩c id(A) ×⇩f id(Y⇗A⇖)"
using idA id_right_unit2 by (typecheck_cfuncs, auto)
finally show "eval_func Y A ∘⇩c id⇩c A ×⇩f f⇧♯ ∘⇩c g⇧♯ = eval_func Y A ∘⇩c id⇩c A ×⇩f id⇩c (Y⇗A⇖)".
qed
have gsharp_fsharp_id: "g⇧♯ ∘⇩c f⇧♯ = id(Y⇗X⇖)"
proof(etcs_rule same_evals_equal[where X = Y, where A = X])
have "eval_func Y X ∘⇩c id⇩c X ×⇩f g⇧♯ ∘⇩c f⇧♯ = eval_func Y X ∘⇩c (id⇩c X ×⇩f g⇧♯) ∘⇩c (id⇩c X ×⇩f f⇧♯)"
using fsharp_type gsharp_type identity_distributes_across_composition by auto
also have "... = eval_func Y A ∘⇩c (φ ×⇩f id⇩c (Y⇗A⇖)) ∘⇩c (id⇩c X ×⇩f f⇧♯)"
using φ_def cfunc_type_def comp_associative fsharp_type g_def g_type transpose_func_def by (typecheck_cfuncs, smt)
also have "... = eval_func Y A ∘⇩c (φ ×⇩f f⇧♯)"
by (smt φ_def cfunc_cross_prod_comp_cfunc_cross_prod fsharp_type id_left_unit2 id_right_unit2 id_type)
also have "... = eval_func Y A ∘⇩c (id(A) ×⇩f f⇧♯) ∘⇩c (φ ×⇩f id⇩c (Y⇗X⇖))"
by (smt φ_def cfunc_cross_prod_comp_cfunc_cross_prod fsharp_type id_left_unit2 id_right_unit2 id_type)
also have "... = eval_func Y X ∘⇩c (ψ ×⇩f id⇩c (Y⇗X⇖)) ∘⇩c (φ ×⇩f id⇩c (Y⇗X⇖))"
by (typecheck_cfuncs, smt φ_def ψ_def comp_associative2 f_def f_type flat_cancels_sharp inv_transpose_func_def3)
also have "... = eval_func Y X ∘⇩c ((ψ ∘⇩c φ) ×⇩f (id(Y⇗X⇖) ∘⇩c id(Y⇗X⇖)))"
using φ_def ψ_def cfunc_cross_prod_comp_cfunc_cross_prod by (typecheck_cfuncs, auto)
also have "... = eval_func Y X ∘⇩c id(X) ×⇩f id(Y⇗X⇖)"
using ψ_def id_left_unit2 by (typecheck_cfuncs, auto)
finally show "eval_func Y X ∘⇩c id⇩c X ×⇩f g⇧♯ ∘⇩c f⇧♯ = eval_func Y X ∘⇩c id⇩c X ×⇩f id⇩c (Y⇗X⇖)".
qed
show ?thesis
by (metis cfunc_type_def comp_epi_imp_epi comp_monic_imp_monic epi_mon_is_iso fsharp_gsharp_id fsharp_type gsharp_fsharp_id gsharp_type id_isomorphism is_isomorphic_def iso_imp_epi_and_monic)
qed
lemma exp_pres_iso:
assumes "A ≅ X" "B ≅ Y"
shows "A⇗B⇖ ≅ X⇗Y⇖"
by (meson assms exp_pres_iso_left exp_pres_iso_right isomorphic_is_transitive)
lemma empty_to_nonempty:
assumes "nonempty X" "is_empty Y"
shows "Y⇗X⇖ ≅ ∅"
by (meson assms exp_pres_iso_left isomorphic_is_transitive no_el_iff_iso_empty empty_exp_nonempty)
lemma exp_is_empty:
assumes "is_empty X"
shows "Y⇗X⇖ ≅ 𝟭"
using assms exp_pres_iso_right isomorphic_is_transitive no_el_iff_iso_empty exp_empty by blast
lemma nonempty_to_nonempty:
assumes "nonempty X" "nonempty Y"
shows "nonempty(Y⇗X⇖)"
by (meson assms(2) comp_type nonempty_def terminal_func_type transpose_func_type)
lemma empty_to_nonempty_converse:
assumes "Y⇗X⇖ ≅ ∅"
shows "is_empty Y ∧ nonempty X"
by (metis is_empty_def exp_is_empty assms no_el_iff_iso_empty nonempty_def nonempty_to_nonempty single_elem_iso_one)
text ‹The definition below corresponds to Definition 2.5.11 in Halvorson.›
definition powerset :: "cset ⇒ cset" ("𝒫_" [101]100) where
"𝒫 X = Ω⇗X⇖"
lemma sets_squared:
"A⇗Ω⇖ ≅ A ×⇩c A"
proof -
obtain φ where φ_def: "φ = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩⟩" and
φ_type[type_rule]: "φ : A⇗Ω⇖ → A ×⇩c A"
by (typecheck_cfuncs, simp)
have "injective φ"
unfolding injective_def
proof(clarify)
fix f g
assume "f ∈⇩c domain φ" then have f_type[type_rule]: "f ∈⇩c A⇗Ω⇖"
using φ_type cfunc_type_def by (typecheck_cfuncs, auto)
assume "g ∈⇩c domain φ" then have g_type[type_rule]: "g ∈⇩c A⇗Ω⇖"
using φ_type cfunc_type_def by (typecheck_cfuncs, auto)
assume eqs: "φ ∘⇩c f = φ ∘⇩c g"
show "f = g"
proof(etcs_rule one_separator)
show "⋀id_1. id_1 ∈⇩c 𝟭 ⟹ f ∘⇩c id_1 = g ∘⇩c id_1"
proof(etcs_rule same_evals_equal[where X = A, where A = Ω])
fix id_1
assume id1_is: "id_1 ∈⇩c 𝟭"
then have id1_eq: "id_1 = id(𝟭)"
using id_type one_unique_element by auto
obtain a1 a2 where phi_f_def: "φ ∘⇩c f = ⟨a1,a2⟩ ∧ a1 ∈⇩c A ∧ a2 ∈⇩c A"
using φ_type cart_prod_decomp comp_type f_type by blast
have equation1: "⟨a1,a2⟩ = ⟨eval_func A Ω ∘⇩c ⟨𝗍, f⟩,
eval_func A Ω ∘⇩c ⟨𝖿, f⟩⟩"
proof -
have "⟨a1,a2⟩ = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩⟩ ∘⇩c f"
using φ_def phi_f_def by auto
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c f,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c f⟩"
by (typecheck_cfuncs,smt cfunc_prod_comp comp_associative2)
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c f, id(A⇗Ω⇖) ∘⇩c f⟩,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c f, id(A⇗Ω⇖)∘⇩c f⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍, f⟩,
eval_func A Ω ∘⇩c ⟨𝖿, f⟩⟩"
by (typecheck_cfuncs, metis id1_eq id1_is id_left_unit2 id_right_unit2 terminal_func_unique)
finally show ?thesis.
qed
have equation2: "⟨a1,a2⟩ = ⟨eval_func A Ω ∘⇩c ⟨𝗍, g⟩,
eval_func A Ω ∘⇩c ⟨𝖿, g⟩⟩"
proof -
have "⟨a1,a2⟩ = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩⟩ ∘⇩c g"
using φ_def eqs phi_f_def by auto
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c g ,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c g⟩"
by (typecheck_cfuncs,smt cfunc_prod_comp comp_associative2)
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c g, id(A⇗Ω⇖) ∘⇩c g⟩,
eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c g, id(A⇗Ω⇖)∘⇩c g ⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
also have "... = ⟨eval_func A Ω ∘⇩c ⟨𝗍, g⟩,
eval_func A Ω ∘⇩c ⟨𝖿, g⟩⟩"
by (typecheck_cfuncs, metis id1_eq id1_is id_left_unit2 id_right_unit2 terminal_func_unique)
finally show ?thesis.
qed
have "⟨eval_func A Ω ∘⇩c ⟨𝗍, f⟩, eval_func A Ω ∘⇩c ⟨𝖿, f⟩⟩ =
⟨eval_func A Ω ∘⇩c ⟨𝗍, g⟩, eval_func A Ω ∘⇩c ⟨𝖿, g⟩⟩"
using equation1 equation2 by auto
then have equation3: "(eval_func A Ω ∘⇩c ⟨𝗍, f⟩ = eval_func A Ω ∘⇩c ⟨𝗍, g⟩) ∧
(eval_func A Ω ∘⇩c ⟨𝖿, f⟩ = eval_func A Ω ∘⇩c ⟨𝖿, g⟩)"
using cart_prod_eq2 by (typecheck_cfuncs, auto)
have "eval_func A Ω ∘⇩c id⇩c Ω ×⇩f f = eval_func A Ω ∘⇩c id⇩c Ω ×⇩f g"
proof(etcs_rule one_separator)
fix x
assume x_type[type_rule]: "x ∈⇩c Ω ×⇩c 𝟭"
then obtain w i where x_def: "(w ∈⇩c Ω) ∧ (i ∈⇩c 𝟭) ∧ (x = ⟨w,i⟩)"
using cart_prod_decomp by blast
then have i_def: "i = id(𝟭)"
using id1_eq id1_is one_unique_element by auto
have w_def: "(w = 𝖿) ∨ (w = 𝗍)"
by (simp add: true_false_only_truth_values x_def)
then have x_def2: "(x = ⟨𝖿,i⟩) ∨ (x = ⟨𝗍,i⟩)"
using x_def by auto
show "(eval_func A Ω ∘⇩c id⇩c Ω ×⇩f f) ∘⇩c x = (eval_func A Ω ∘⇩c id⇩c Ω ×⇩f g) ∘⇩c x"
proof(cases "(x = ⟨𝖿,i⟩)", clarify)
assume case1: "x = ⟨𝖿,i⟩"
have "(eval_func A Ω ∘⇩c (id⇩c Ω ×⇩f f)) ∘⇩c ⟨𝖿,i⟩ = eval_func A Ω ∘⇩c ((id⇩c Ω ×⇩f f) ∘⇩c ⟨𝖿,i⟩)"
using case1 comp_associative2 x_type by (typecheck_cfuncs, auto)
also have "... = eval_func A Ω ∘⇩c ⟨id⇩c Ω ∘⇩c 𝖿,f ∘⇩c i⟩"
using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
also have "... = eval_func A Ω ∘⇩c ⟨𝖿, f ⟩"
using f_type false_func_type i_def id_left_unit2 id_right_unit2 by auto
also have "... = eval_func A Ω ∘⇩c ⟨𝖿, g⟩"
using equation3 by blast
also have "... = eval_func A Ω ∘⇩c ⟨id⇩c Ω ∘⇩c 𝖿,g ∘⇩c i⟩"
by (typecheck_cfuncs, simp add: i_def id_left_unit2 id_right_unit2)
also have "... = eval_func A Ω ∘⇩c ((id⇩c Ω ×⇩f g) ∘⇩c ⟨𝖿,i⟩)"
using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
also have "... = (eval_func A Ω ∘⇩c (id⇩c Ω ×⇩f g)) ∘⇩c ⟨𝖿,i⟩"
using case1 comp_associative2 x_type by (typecheck_cfuncs, auto)
finally show "(eval_func A Ω ∘⇩c id⇩c Ω ×⇩f f) ∘⇩c ⟨𝖿,i⟩ = (eval_func A Ω ∘⇩c id⇩c Ω ×⇩f g) ∘⇩c ⟨𝖿,i⟩".
next
assume case2: "x ≠ ⟨𝖿,i⟩"
then have x_eq: "x = ⟨𝗍,i⟩"
using x_def2 by blast
have "(eval_func A Ω ∘⇩c (id⇩c Ω ×⇩f f)) ∘⇩c ⟨𝗍,i⟩ = eval_func A Ω ∘⇩c ((id⇩c Ω ×⇩f f) ∘⇩c ⟨𝗍,i⟩)"
using case2 x_eq comp_associative2 x_type by (typecheck_cfuncs, auto)
also have "... = eval_func A Ω ∘⇩c ⟨id⇩c Ω ∘⇩c 𝗍,f ∘⇩c i⟩"
using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
also have "... = eval_func A Ω ∘⇩c ⟨𝗍, f ⟩"
using f_type i_def id_left_unit2 id_right_unit2 true_func_type by auto
also have "... = eval_func A Ω ∘⇩c ⟨𝗍, g⟩"
using equation3 by blast
also have "... = eval_func A Ω ∘⇩c ⟨id⇩c Ω ∘⇩c 𝗍,g ∘⇩c i⟩"
by (typecheck_cfuncs, simp add: i_def id_left_unit2 id_right_unit2)
also have "... = eval_func A Ω ∘⇩c ((id⇩c Ω ×⇩f g) ∘⇩c ⟨𝗍,i⟩)"
using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
also have "... = (eval_func A Ω ∘⇩c (id⇩c Ω ×⇩f g)) ∘⇩c ⟨𝗍,i⟩"
using comp_associative2 x_eq x_type by (typecheck_cfuncs, blast)
ultimately show "(eval_func A Ω ∘⇩c id⇩c Ω ×⇩f f) ∘⇩c x = (eval_func A Ω ∘⇩c id⇩c Ω ×⇩f g) ∘⇩c x"
by (simp add: x_eq)
qed
qed
then show "eval_func A Ω ∘⇩c id⇩c Ω ×⇩f f ∘⇩c id_1 = eval_func A Ω ∘⇩c id⇩c Ω ×⇩f g ∘⇩c id_1"
using f_type g_type same_evals_equal by blast
qed
qed
qed
then have "monomorphism(φ)"
using injective_imp_monomorphism by auto
have "surjective(φ)"
unfolding surjective_def
proof(clarify)
fix y
assume "y ∈⇩c codomain φ" then have y_type[type_rule]: "y ∈⇩c A ×⇩c A"
using φ_type cfunc_type_def by auto
then obtain a1 a2 where y_def[type_rule]: "y = ⟨a1,a2⟩ ∧ a1 ∈⇩c A ∧ a2 ∈⇩c A"
using cart_prod_decomp by blast
then have aua: "(a1 ⨿ a2): 𝟭 ∐ 𝟭 → A"
by (typecheck_cfuncs, simp add: y_def)
obtain f where f_def: "f = ((a1 ⨿ a2) ∘⇩c case_bool ∘⇩c left_cart_proj Ω 𝟭)⇧♯" and
f_type[type_rule]: "f ∈⇩c A⇗Ω⇖"
by (meson aua case_bool_type comp_type left_cart_proj_type transpose_func_type)
have a1_is: "(eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩) ∘⇩c f = a1"
proof-
have "(eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩) ∘⇩c f = eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c f"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = eval_func A Ω ∘⇩c ⟨𝗍 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c f, id(A⇗Ω⇖) ∘⇩c f⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
also have "... = eval_func A Ω ∘⇩c ⟨𝗍, f⟩"
by (metis cfunc_type_def f_type id_left_unit id_right_unit id_type one_unique_element terminal_func_comp terminal_func_type true_func_type)
also have "... = eval_func A Ω ∘⇩c ⟨id(Ω) ∘⇩c 𝗍, f ∘⇩c id(𝟭)⟩"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
also have "... = eval_func A Ω ∘⇩c (id(Ω) ×⇩f f) ∘⇩c ⟨𝗍, id(𝟭)⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (eval_func A Ω ∘⇩c (id(Ω) ×⇩f f)) ∘⇩c ⟨𝗍, id(𝟭)⟩"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = ((a1 ⨿ a2) ∘⇩c case_bool ∘⇩c left_cart_proj Ω 𝟭) ∘⇩c ⟨𝗍, id(𝟭)⟩"
by (typecheck_cfuncs, metis aua f_def flat_cancels_sharp inv_transpose_func_def3)
also have "... = (a1 ⨿ a2) ∘⇩c case_bool ∘⇩c 𝗍"
by (typecheck_cfuncs, smt case_bool_type aua comp_associative2 left_cart_proj_cfunc_prod)
also have "... = (a1 ⨿ a2) ∘⇩c left_coproj 𝟭 𝟭"
by (simp add: case_bool_true)
also have "... = a1"
using left_coproj_cfunc_coprod y_def by blast
finally show ?thesis.
qed
have a2_is: "(eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩) ∘⇩c f = a2"
proof-
have "(eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩) ∘⇩c f = eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙, id(A⇗Ω⇖)⟩ ∘⇩c f"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = eval_func A Ω ∘⇩c ⟨𝖿 ∘⇩c β⇘A⇗Ω⇖⇙ ∘⇩c f, id(A⇗Ω⇖) ∘⇩c f⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
also have "... = eval_func A Ω ∘⇩c ⟨𝖿, f⟩"
by (metis cfunc_type_def f_type id_left_unit id_right_unit id_type one_unique_element terminal_func_comp terminal_func_type false_func_type)
also have "... = eval_func A Ω ∘⇩c ⟨id(Ω) ∘⇩c 𝖿, f ∘⇩c id(𝟭)⟩"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
also have "... = eval_func A Ω ∘⇩c (id(Ω) ×⇩f f) ∘⇩c ⟨𝖿, id(𝟭)⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (eval_func A Ω ∘⇩c (id(Ω) ×⇩f f)) ∘⇩c ⟨𝖿, id(𝟭)⟩"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = ((a1 ⨿ a2) ∘⇩c case_bool ∘⇩c left_cart_proj Ω 𝟭) ∘⇩c ⟨𝖿, id(𝟭)⟩"
by (typecheck_cfuncs, metis aua f_def flat_cancels_sharp inv_transpose_func_def3)
also have "... = (a1 ⨿ a2) ∘⇩c case_bool ∘⇩c 𝖿"
by (typecheck_cfuncs, smt aua comp_associative2 left_cart_proj_cfunc_prod)
also have "... = (a1 ⨿ a2) ∘⇩c right_coproj 𝟭 𝟭"
by (simp add: case_bool_false)
also have "... = a2"
using right_coproj_cfunc_coprod y_def by blast
finally show ?thesis.
qed
have "φ ∘⇩c f = ⟨a1,a2⟩"
unfolding φ_def by (typecheck_cfuncs, simp add: a1_is a2_is cfunc_prod_comp)
then show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
using φ_type cfunc_type_def f_type y_def by auto
qed
then have "epimorphism(φ)"
by (simp add: surjective_is_epimorphism)
then have "isomorphism(φ)"
by (simp add: ‹monomorphism φ› epi_mon_is_iso)
then show ?thesis
using φ_type is_isomorphic_def by blast
qed
end