Theory Coproduct
section ‹Coproducts›
theory Coproduct
imports Equivalence
begin
hide_const case_bool
text ‹The axiomatization below corresponds to Axiom 7 (Coproducts) in Halvorson.›
axiomatization
coprod :: "cset ⇒ cset ⇒ cset" (infixr "∐" 65) and
left_coproj :: "cset ⇒ cset ⇒ cfunc" and
right_coproj :: "cset ⇒ cset ⇒ cfunc" and
cfunc_coprod :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "⨿" 65)
where
left_proj_type[type_rule]: "left_coproj X Y : X → X∐Y" and
right_proj_type[type_rule]: "right_coproj X Y : Y → X∐Y" and
cfunc_coprod_type[type_rule]: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g : X∐Y → Z" and
left_coproj_cfunc_coprod: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g ∘⇩c (left_coproj X Y) = f" and
right_coproj_cfunc_coprod: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g ∘⇩c (right_coproj X Y) = g" and
cfunc_coprod_unique: "f : X → Z ⟹ g : Y → Z ⟹ h : X ∐ Y → Z ⟹
h ∘⇩c left_coproj X Y = f ⟹ h ∘⇩c right_coproj X Y = g ⟹ h = f ⨿ g"
definition is_coprod :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cset ⇒ bool" where
"is_coprod W i⇩0 i⇩1 X Y ⟷
(i⇩0 : X → W ∧ i⇩1 : Y → W ∧
(∀ f g Z. (f : X → Z ∧ g : Y → Z) ⟶
(∃ h. h : W → Z ∧ h ∘⇩c i⇩0 = f ∧ h ∘⇩c i⇩1 = g ∧
(∀ h2. (h2 : W → Z ∧ h2 ∘⇩c i⇩0 = f ∧ h2 ∘⇩c i⇩1 = g) ⟶ h2 = h))))"
lemma is_coprod_def2:
assumes "i⇩0 : X → W" "i⇩1 : Y → W"
shows "is_coprod W i⇩0 i⇩1 X Y ⟷
(∀ f g Z. (f : X → Z ∧ g : Y → Z) ⟶
(∃ h. h : W → Z ∧ h ∘⇩c i⇩0 = f ∧ h ∘⇩c i⇩1 = g ∧
(∀ h2. (h2 : W → Z ∧ h2 ∘⇩c i⇩0 = f ∧ h2 ∘⇩c i⇩1 = g) ⟶ h2 = h)))"
unfolding is_coprod_def using assms by auto
abbreviation is_coprod_triple :: "cset × cfunc × cfunc ⇒ cset ⇒ cset ⇒ bool" where
"is_coprod_triple Wi X Y ≡ is_coprod (fst Wi) (fst (snd Wi)) (snd (snd Wi)) X Y"
lemma canonical_coprod_is_coprod:
"is_coprod (X ∐ Y) (left_coproj X Y) (right_coproj X Y) X Y"
unfolding is_coprod_def
proof (typecheck_cfuncs)
fix f g Z
assume f_type: "f : X → Z"
assume g_type: "g : Y → Z"
show "∃h. h : X ∐ Y → Z ∧
h ∘⇩c left_coproj X Y = f ∧
h ∘⇩c right_coproj X Y = g ∧ (∀h2. h2 : X ∐ Y → Z ∧ h2 ∘⇩c left_coproj X Y = f ∧ h2 ∘⇩c right_coproj X Y = g ⟶ h2 = h)"
using cfunc_coprod_type cfunc_coprod_unique f_type g_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod
by(intro exI[where x="f⨿g"], auto)
qed
text ‹The lemma below is dual to Proposition 2.1.8 in Halvorson.›
lemma coprods_isomorphic:
assumes W_coprod: "is_coprod_triple (W, i⇩0, i⇩1) X Y"
assumes W'_coprod: "is_coprod_triple (W', i'⇩0, i'⇩1) X Y"
shows "∃ g. g : W → W' ∧ isomorphism g ∧ g ∘⇩c i⇩0 = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
proof -
obtain f where f_def: "f : W' → W ∧ f ∘⇩c i'⇩0 = i⇩0 ∧ f ∘⇩c i'⇩1 = i⇩1"
using W_coprod W'_coprod unfolding is_coprod_def
by (metis split_pairs)
obtain g where g_def: "g : W → W' ∧ g ∘⇩c i⇩0 = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
using W_coprod W'_coprod unfolding is_coprod_def
by (metis split_pairs)
have fg0: "(f ∘⇩c g) ∘⇩c i⇩0 = i⇩0"
by (metis W_coprod comp_associative2 f_def g_def is_coprod_def split_pairs)
have fg1: "(f ∘⇩c g) ∘⇩c i⇩1 = i⇩1"
by (metis W_coprod comp_associative2 f_def g_def is_coprod_def split_pairs)
obtain idW where "idW : W → W ∧ (∀ h2. (h2 : W → W ∧ h2 ∘⇩c i⇩0 = i⇩0 ∧ h2 ∘⇩c i⇩1 = i⇩1) ⟶ h2 = idW)"
by (smt (verit, best) W_coprod is_coprod_def prod.sel)
then have fg: "f ∘⇩c g = id W"
proof clarify
assume idW_unique: "∀h2. h2 : W → W ∧ h2 ∘⇩c i⇩0 = i⇩0 ∧ h2 ∘⇩c i⇩1 = i⇩1 ⟶ h2 = idW"
have 1: "f ∘⇩c g = idW"
using comp_type f_def fg0 fg1 g_def idW_unique by blast
have 2: "id W = idW"
using W_coprod idW_unique id_left_unit2 id_type is_coprod_def by auto
from 1 2 show "f ∘⇩c g = id W"
by auto
qed
have gf0: "(g ∘⇩c f) ∘⇩c i'⇩0= i'⇩0"
using W'_coprod comp_associative2 f_def g_def is_coprod_def by auto
have gf1: "(g ∘⇩c f) ∘⇩c i'⇩1 = i'⇩1"
using W'_coprod comp_associative2 f_def g_def is_coprod_def by auto
obtain idW' where "idW': W'→ W'∧ (∀ h2. (h2 : W'→ W'∧ h2 ∘⇩c i'⇩0= i'⇩0 ∧ h2 ∘⇩c i'⇩1= i'⇩1) ⟶ h2 = idW')"
by (smt (verit, best) W'_coprod is_coprod_def prod.sel)
then have gf: "g ∘⇩c f = id W'"
proof clarify
assume idW'_unique: "∀h2. h2 : W' → W' ∧ h2 ∘⇩c i'⇩0 = i'⇩0 ∧ h2 ∘⇩c i'⇩1 = i'⇩1 ⟶ h2 = idW'"
have 1: "g ∘⇩c f = idW'"
using comp_type f_def g_def gf0 gf1 idW'_unique by blast
have 2: "id W' = idW'"
using W'_coprod idW'_unique id_left_unit2 id_type is_coprod_def by auto
from 1 2 show "g ∘⇩c f = id W'"
by auto
qed
have g_iso: "isomorphism g"
using f_def fg g_def gf isomorphism_def3 by blast
from g_iso g_def show "∃ g. g : W → W' ∧ isomorphism g ∧ g ∘⇩c i⇩0 = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
by blast
qed
subsection ‹Coproduct Function Properities›
lemma cfunc_coprod_comp:
assumes "a : Y → Z" "b : X → Y" "c : W → Y"
shows "(a ∘⇩c b) ⨿ (a ∘⇩c c) = a ∘⇩c (b ⨿ c)"
proof -
have "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (left_coproj X W) = a ∘⇩c (b ⨿ c) ∘⇩c (left_coproj X W)"
using assms by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
then have left_coproj_eq: "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (left_coproj X W) = (a ∘⇩c (b ⨿ c)) ∘⇩c (left_coproj X W)"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
have "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (right_coproj X W) = a ∘⇩c (b ⨿ c) ∘⇩c (right_coproj X W)"
using assms by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
then have right_coproj_eq: "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (right_coproj X W) = (a ∘⇩c (b ⨿ c)) ∘⇩c (right_coproj X W)"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
show "(a ∘⇩c b) ⨿ (a ∘⇩c c) = a ∘⇩c (b ⨿ c)"
using assms left_coproj_eq right_coproj_eq
by (typecheck_cfuncs, smt cfunc_coprod_unique left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
qed
lemma id_coprod:
"id(A ∐ B) = (left_coproj A B) ⨿ (right_coproj A B)"
by (typecheck_cfuncs, simp add: cfunc_coprod_unique id_left_unit2)
text ‹The lemma below corresponds to Proposition 2.4.1 in Halvorson.›
lemma coproducts_disjoint:
" x∈⇩c X ⟹ y ∈⇩c Y ⟹ (left_coproj X Y) ∘⇩c x ≠ (right_coproj X Y) ∘⇩c y"
proof (rule ccontr, clarify)
assume x_type[type_rule]: "x∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c Y"
assume BWOC: "((left_coproj X Y) ∘⇩c x = (right_coproj X Y) ∘⇩c y)"
obtain g where g_def: "g factorsthru 𝗍" and g_type[type_rule]: "g: X → Ω"
by (typecheck_cfuncs, meson comp_type factors_through_def2 terminal_func_type)
then have fact1: "𝗍 = g ∘⇩c x"
by (metis cfunc_type_def comp_associative factors_through_def id_right_unit2 id_type
terminal_func_comp terminal_func_unique true_func_type x_type)
obtain h where h_def: "h factorsthru 𝖿" and h_type[type_rule]: "h: Y → Ω"
by (typecheck_cfuncs, meson comp_type factors_through_def2 one_terminal_object terminal_object_def)
then have gUh_type[type_rule]: "g ⨿ h: X ∐ Y → Ω" and
gUh_def: "(g ⨿ h) ∘⇩c (left_coproj X Y) = g ∧ (g ⨿ h) ∘⇩c (right_coproj X Y) = h"
using left_coproj_cfunc_coprod right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
then have fact2: "𝖿 = ((g ⨿ h) ∘⇩c (right_coproj X Y)) ∘⇩c y"
by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 factors_through_def2 gUh_def h_def id_right_unit2 terminal_func_comp_elem terminal_func_unique)
also have "... = ((g ⨿ h) ∘⇩c (left_coproj X Y)) ∘⇩c x"
by (smt BWOC comp_associative2 gUh_type left_proj_type right_proj_type x_type y_type)
also have "... = 𝗍"
by (simp add: fact1 gUh_def)
ultimately show False
using true_false_distinct by auto
qed
text ‹The lemma below corresponds to Proposition 2.4.2 in Halvorson.›
lemma left_coproj_are_monomorphisms:
"monomorphism(left_coproj X Y)"
proof (cases "∃x. x ∈⇩c X")
assume X_nonempty: "∃x. x ∈⇩c X"
then obtain x where x_type[type_rule]: "x ∈⇩c X"
by auto
then have "(id X ⨿ (x ∘⇩c β⇘Y⇙)) ∘⇩c left_coproj X Y = id X"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
then show "monomorphism (left_coproj X Y)"
by (typecheck_cfuncs, metis (mono_tags) cfunc_coprod_type comp_monic_imp_monic'
comp_type id_isomorphism id_type iso_imp_epi_and_monic terminal_func_type x_type)
next
show "∄x. x ∈⇩c X ⟹ monomorphism (left_coproj X Y)"
by (typecheck_cfuncs, metis cfunc_type_def injective_def injective_imp_monomorphism)
qed
lemma right_coproj_are_monomorphisms:
"monomorphism(right_coproj X Y)"
proof (cases "∃y. y ∈⇩c Y")
assume Y_nonempty: "∃y. y ∈⇩c Y"
then obtain y where y_type[type_rule]: "y ∈⇩c Y"
by auto
have "((y ∘⇩c β⇘X⇙) ⨿ id Y) ∘⇩c right_coproj X Y = id Y"
by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
then show "monomorphism (right_coproj X Y)"
by (typecheck_cfuncs, metis (mono_tags) cfunc_coprod_type comp_monic_imp_monic'
comp_type id_isomorphism id_type iso_imp_epi_and_monic terminal_func_type y_type)
next
show "∄y. y ∈⇩c Y ⟹ monomorphism (right_coproj X Y)"
by (typecheck_cfuncs, metis cfunc_type_def injective_def injective_imp_monomorphism)
qed
text ‹The lemma below corresponds to Exercise 2.4.3 in Halvorson.›
lemma coprojs_jointly_surj:
assumes z_type[type_rule]: "z ∈⇩c X ∐ Y"
shows "(∃ x. (x ∈⇩c X ∧ z = (left_coproj X Y) ∘⇩c x))
∨ (∃ y. (y ∈⇩c Y ∧ z = (right_coproj X Y) ∘⇩c y))"
proof (clarify, rule ccontr)
assume not_in_right_image: "∄y. y ∈⇩c Y ∧ z = right_coproj X Y ∘⇩c y"
assume not_in_left_image: "∄x. x ∈⇩c X ∧ z = left_coproj X Y ∘⇩c x"
obtain h where h_def: "h = 𝖿 ∘⇩c β⇘X ∐ Y⇙" and h_type[type_rule]: "h : X ∐ Y → Ω"
by (typecheck_cfuncs, simp)
have fact1: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c left_coproj X Y = h ∘⇩c left_coproj X Y"
proof(etcs_rule one_separator[where X=X, where Y = Ω])
show "⋀x. x ∈⇩c X ⟹ ((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x =
(h ∘⇩c left_coproj X Y) ∘⇩c x"
proof -
fix x
assume x_type: "x ∈⇩c X"
have "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x =
eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩ ∘⇩c (left_coproj X Y ∘⇩c x)"
using x_type by (typecheck_cfuncs, metis assms cfunc_type_def comp_associative)
also have "... = 𝖿"
using assms eq_pred_false_extract_right not_in_left_image x_type by (typecheck_cfuncs, presburger)
also have "... = h ∘⇩c (left_coproj X Y ∘⇩c x)"
using x_type by (typecheck_cfuncs, smt comp_associative2 h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
also have "... = (h ∘⇩c left_coproj X Y) ∘⇩c x"
using x_type cfunc_type_def comp_associative comp_type false_func_type h_def terminal_func_type by (typecheck_cfuncs, force)
finally show "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x = (h ∘⇩c left_coproj X Y) ∘⇩c x".
qed
qed
have fact2: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c right_coproj X Y = h ∘⇩c right_coproj X Y"
proof(etcs_rule one_separator[where X = Y, where Y = Ω])
show "⋀x. x ∈⇩c Y ⟹
((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c x =
(h ∘⇩c right_coproj X Y) ∘⇩c x"
proof -
fix x
assume x_type[type_rule]: "x ∈⇩c Y"
have "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c x = 𝖿"
by (typecheck_cfuncs, smt (verit) assms cfunc_type_def eq_pred_false_extract_right comp_associative comp_type not_in_right_image)
also have "... = (h ∘⇩c right_coproj X Y) ∘⇩c x"
by (etcs_assocr,typecheck_cfuncs, metis cfunc_type_def comp_associative h_def id_right_unit2 terminal_func_comp_elem terminal_func_type)
finally show "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c x = (h ∘⇩c right_coproj X Y) ∘⇩c x".
qed
qed
have indicator_is_false:"eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩ = h"
proof(etcs_rule one_separator[where X = "X ∐ Y", where Y = Ω])
show "⋀x. x ∈⇩c X ∐ Y ⟹ (eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c x = h ∘⇩c x"
by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp fact1 fact2 id_coprod id_right_unit2 left_proj_type right_proj_type)
qed
have hz_gives_false: "h ∘⇩c z = 𝖿"
using assms by (typecheck_cfuncs, smt comp_associative2 h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
then have indicator_z_gives_false: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c z = 𝖿"
using assms indicator_is_false by (typecheck_cfuncs, blast)
then have indicator_z_gives_true: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c z = 𝗍"
using assms by (typecheck_cfuncs, smt (verit, del_insts) comp_associative2 eq_pred_true_extract_right)
then show False
using indicator_z_gives_false true_false_distinct by auto
qed
lemma maps_into_1u1:
assumes x_type: "x∈⇩c (𝟭 ∐ 𝟭)"
shows "(x = left_coproj 𝟭 𝟭) ∨ (x = right_coproj 𝟭 𝟭)"
using assms by (typecheck_cfuncs, metis coprojs_jointly_surj terminal_func_unique)
lemma coprod_preserves_left_epi:
assumes "f: X → Z" "g: Y → Z"
assumes "surjective(f)"
shows "surjective(f ⨿ g)"
unfolding surjective_def
proof(clarify)
fix z
assume y_type[type_rule]: "z ∈⇩c codomain (f ⨿ g)"
then obtain x where x_def: "x ∈⇩c X ∧ f ∘⇩c x = z"
using assms cfunc_coprod_type cfunc_type_def cfunc_type_def surjective_def by auto
have "(f ⨿ g) ∘⇩c (left_coproj X Y ∘⇩c x) = z"
by (typecheck_cfuncs, smt assms comp_associative2 left_coproj_cfunc_coprod x_def)
then show "∃x. x ∈⇩c domain(f ⨿ g) ∧ f ⨿ g ∘⇩c x = z"
by (typecheck_cfuncs, metis assms(1,2) cfunc_type_def codomain_comp domain_comp left_proj_type x_def)
qed
lemma coprod_preserves_right_epi:
assumes "f: X → Z" "g: Y → Z"
assumes "surjective(g)"
shows "surjective(f ⨿ g)"
unfolding surjective_def
proof(clarify)
fix z
assume y_type: "z ∈⇩c codomain (f ⨿ g)"
have fug_type: "(f ⨿ g) : (X ∐ Y) → Z"
by (typecheck_cfuncs, simp add: assms)
then have y_type2: "z ∈⇩c Z"
using cfunc_type_def y_type by auto
then have "∃ y. y ∈⇩c Y ∧ g ∘⇩c y = z"
using assms(2,3) cfunc_type_def surjective_def by auto
then obtain y where y_def: "y ∈⇩c Y ∧ g ∘⇩c y = z"
by blast
have coproj_x_type: "right_coproj X Y ∘⇩c y ∈⇩c X ∐ Y"
using comp_type right_proj_type y_def by blast
have "(f ⨿ g) ∘⇩c (right_coproj X Y ∘⇩c y) = z"
using assms(1) assms(2) cfunc_type_def comp_associative fug_type right_coproj_cfunc_coprod right_proj_type y_def by auto
then show "∃y. y ∈⇩c domain(f ⨿ g) ∧ f ⨿ g ∘⇩c y = z"
using cfunc_type_def coproj_x_type fug_type by auto
qed
lemma coprod_eq:
assumes "a : X ∐ Y → Z" "b : X ∐ Y → Z"
shows "a = b ⟷
(a ∘⇩c left_coproj X Y = b ∘⇩c left_coproj X Y
∧ a ∘⇩c right_coproj X Y = b ∘⇩c right_coproj X Y)"
by (smt assms cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type)
lemma coprod_eqI:
assumes "a : X ∐ Y → Z" "b : X ∐ Y → Z"
assumes "(a ∘⇩c left_coproj X Y = b ∘⇩c left_coproj X Y
∧ a ∘⇩c right_coproj X Y = b ∘⇩c right_coproj X Y)"
shows "a = b"
using assms coprod_eq by blast
lemma coprod_eq2:
assumes "a : X → Z" "b : Y → Z" "c : X → Z" "d : Y → Z"
shows "(a ⨿ b) = (c ⨿ d) ⟷ (a = c ∧ b = d)"
by (metis assms left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
lemma coprod_decomp:
assumes "a : X ∐ Y → A"
shows "∃ x y. a = (x ⨿ y) ∧ x : X → A ∧ y : Y → A"
proof (rule exI[where x="a ∘⇩c left_coproj X Y"], intro exI[where x="a ∘⇩c right_coproj X Y"], safe)
show "a = (a ∘⇩c left_coproj X Y) ⨿ (a ∘⇩c right_coproj X Y)"
using assms cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type by auto
show "a ∘⇩c left_coproj X Y : X → A"
by (meson assms comp_type left_proj_type)
show "a ∘⇩c right_coproj X Y : Y → A"
by (meson assms comp_type right_proj_type)
qed
text ‹The lemma below corresponds to Proposition 2.4.4 in Halvorson.›
lemma truth_value_set_iso_1u1:
"isomorphism(𝗍⨿𝖿)"
by (typecheck_cfuncs, smt (verit, best) CollectI epi_mon_is_iso injective_def2
injective_imp_monomorphism left_coproj_cfunc_coprod left_proj_type maps_into_1u1
right_coproj_cfunc_coprod right_proj_type surjective_def2 surjective_is_epimorphism
true_false_distinct true_false_only_truth_values)
subsubsection ‹Equality Predicate with Coproduct Properities›
lemma eq_pred_left_coproj:
assumes u_type[type_rule]: "u ∈⇩c X ∐ Y" and x_type[type_rule]: "x ∈⇩c X"
shows "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩ = ((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c u"
proof (cases "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩= 𝗍")
assume case1: "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩ = 𝗍"
then have u_is_left_coproj: "u = left_coproj X Y ∘⇩c x"
using eq_pred_iff_eq by (typecheck_cfuncs_prems, presburger)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
proof -
have "((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c u
= ((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c left_coproj X Y ∘⇩c x"
using u_is_left_coproj by auto
also have "... = (eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ∘⇩c x "
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
also have "... = eq_pred X ∘⇩c ⟨x, x⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left cfunc_type_def comp_associative)
also have "... = 𝗍"
using eq_pred_iff_eq by (typecheck_cfuncs, blast)
ultimately show ?thesis
by (simp add: case1)
qed
next
assume "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ ≠ 𝗍"
then have case2: "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = 𝖿"
using true_false_only_truth_values by (typecheck_cfuncs, blast)
then have u_not_left_coproj_x: "u ≠ left_coproj X Y ∘⇩c x"
using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
proof (cases "∃ g. g : 𝟭 → X ∧ u = left_coproj X Y ∘⇩c g")
assume "∃g. g ∈⇩c X ∧ u = left_coproj X Y ∘⇩c g"
then obtain g where g_type[type_rule]: "g ∈⇩c X" and g_def: "u = left_coproj X Y ∘⇩c g"
by auto
then have x_not_g: "x ≠ g"
using u_not_left_coproj_x by auto
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
proof -
have "(eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c left_coproj X Y ∘⇩c g
= (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ∘⇩c g"
using comp_associative2 left_coproj_cfunc_coprod by (typecheck_cfuncs, force)
also have "... = eq_pred X ∘⇩c ⟨g,x⟩"
by (typecheck_cfuncs, simp add: cart_prod_extract_left comp_associative2)
also have "... = 𝖿"
using eq_pred_iff_eq_conv x_not_g by (typecheck_cfuncs, blast)
ultimately show ?thesis
using case2 g_def by argo
qed
next
assume "∄g. g ∈⇩c X ∧ u = left_coproj X Y ∘⇩c g"
then obtain g where g_type[type_rule]: "g ∈⇩c Y" and g_def: "u = right_coproj X Y ∘⇩c g"
by (meson coprojs_jointly_surj u_type)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
proof -
have "(eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u
= (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c right_coproj X Y ∘⇩c g"
using g_def by auto
also have "... = (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c g"
by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
also have "... = 𝖿"
by (typecheck_cfuncs, smt (z3) comp_associative2 id_right_unit2 id_type terminal_func_comp terminal_func_unique)
ultimately show ?thesis
using case2 by argo
qed
qed
qed
lemma eq_pred_right_coproj:
assumes u_type[type_rule]: "u ∈⇩c X ∐ Y" and y_type[type_rule]: "y ∈⇩c Y"
shows "eq_pred (X ∐ Y) ∘⇩c ⟨u, right_coproj X Y ∘⇩c y⟩ = ((𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id Y, y ∘⇩c β⇘Y⇙⟩)) ∘⇩c u"
proof (cases "eq_pred (X ∐ Y) ∘⇩c ⟨u, right_coproj X Y ∘⇩c y⟩ = 𝗍")
assume case1: "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = 𝗍"
then have u_is_right_coproj: "u = right_coproj X Y ∘⇩c y"
using eq_pred_iff_eq by (typecheck_cfuncs_prems, presburger)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
proof -
have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u
= (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c right_coproj X Y ∘⇩c y"
using u_is_right_coproj by auto
also have "... = (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c y"
by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
also have "... = eq_pred Y ∘⇩c ⟨y,y⟩"
by (typecheck_cfuncs, smt cart_prod_extract_left comp_associative2)
also have "... = 𝗍"
using eq_pred_iff_eq y_type by auto
ultimately show ?thesis
using case1 by argo
qed
next
assume "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ ≠ 𝗍"
then have eq_pred_false: "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = 𝖿"
using true_false_only_truth_values by (typecheck_cfuncs, blast)
then have u_not_right_coproj_y: "u ≠ right_coproj X Y ∘⇩c y"
using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
proof (cases "∃ g. g : 𝟭 → Y ∧ u = right_coproj X Y ∘⇩c g")
assume "∃g. g ∈⇩c Y ∧ u = right_coproj X Y ∘⇩c g"
then obtain g where g_type[type_rule]: "g ∈⇩c Y" and g_def: "u = right_coproj X Y ∘⇩c g"
by auto
then have y_not_g: "y ≠ g"
using u_not_right_coproj_y by auto
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
proof -
have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c right_coproj X Y ∘⇩c g
= (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c g"
by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
also have "... = eq_pred Y ∘⇩c ⟨g,y⟩"
using cart_prod_extract_left comp_associative2 by (typecheck_cfuncs, auto)
also have "... = 𝖿"
using eq_pred_iff_eq_conv y_not_g y_type g_type by blast
ultimately show ?thesis
using eq_pred_false g_def by argo
qed
next
assume "∄g. g ∈⇩c Y ∧ u = right_coproj X Y ∘⇩c g"
then obtain g where g_type[type_rule]: "g ∈⇩c X" and g_def: "u = left_coproj X Y ∘⇩c g"
by (meson coprojs_jointly_surj u_type)
show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
proof -
have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u
= (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c left_coproj X Y ∘⇩c g"
using g_def by auto
also have "... = (𝖿 ∘⇩c β⇘X⇙) ∘⇩c g"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
also have "... = 𝖿"
by (typecheck_cfuncs, smt (z3) comp_associative2 id_right_unit2 id_type terminal_func_comp terminal_func_unique)
ultimately show ?thesis
using eq_pred_false by auto
qed
qed
qed
subsection ‹Bowtie Product›
definition cfunc_bowtie_prod :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "⨝⇩f" 55) where
"f ⨝⇩f g = ((left_coproj (codomain f) (codomain g)) ∘⇩c f) ⨿ ((right_coproj (codomain f) (codomain g)) ∘⇩c g)"
lemma cfunc_bowtie_prod_def2:
assumes "f : X → Y" "g : V→ W"
shows "f ⨝⇩f g = (left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)"
using assms cfunc_bowtie_prod_def cfunc_type_def by auto
lemma cfunc_bowtie_prod_type[type_rule]:
"f : X → Y ⟹ g : V → W ⟹ f ⨝⇩f g : X ∐ V → Y ∐ W"
unfolding cfunc_bowtie_prod_def
using cfunc_coprod_type cfunc_type_def comp_type left_proj_type right_proj_type by auto
lemma left_coproj_cfunc_bowtie_prod:
"f : X → Y ⟹ g : V → W ⟹ (f ⨝⇩f g) ∘⇩c left_coproj X V = left_coproj Y W ∘⇩c f"
unfolding cfunc_bowtie_prod_def2
by (meson comp_type left_coproj_cfunc_coprod left_proj_type right_proj_type)
lemma right_coproj_cfunc_bowtie_prod:
"f : X → Y ⟹ g : V → W ⟹ (f ⨝⇩f g) ∘⇩c right_coproj X V = right_coproj Y W ∘⇩c g"
unfolding cfunc_bowtie_prod_def2
by (meson comp_type right_coproj_cfunc_coprod right_proj_type left_proj_type)
lemma cfunc_bowtie_prod_unique: "f : X → Y ⟹ g : V → W ⟹ h : X ∐ V → Y ∐ W ⟹
h ∘⇩c left_coproj X V = left_coproj Y W ∘⇩c f ⟹
h ∘⇩c right_coproj X V = right_coproj Y W ∘⇩c g ⟹ h = f ⨝⇩f g"
unfolding cfunc_bowtie_prod_def
using cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type by auto
text ‹The lemma below is dual to Proposition 2.1.11 in Halvorson.›
lemma identity_distributes_across_composition_dual:
assumes f_type: "f : A → B" and g_type: "g : B → C"
shows "(g ∘⇩c f) ⨝⇩f id X = (g ⨝⇩f id X) ∘⇩c (f ⨝⇩f id X)"
proof -
from cfunc_bowtie_prod_unique
have uniqueness: "∀h. h : A ∐ X → C ∐ X ∧
h ∘⇩c left_coproj A X = left_coproj C X ∘⇩c (g ∘⇩c f) ∧
h ∘⇩c right_coproj A X = right_coproj C X ∘⇩c id(X) ⟶
h = (g ∘⇩c f) ⨝⇩f id⇩c X"
using assms by (typecheck_cfuncs, simp add: cfunc_bowtie_prod_unique)
have left_eq: " ((g ⨝⇩f id⇩c X) ∘⇩c (f ⨝⇩f id⇩c X)) ∘⇩c left_coproj A X = left_coproj C X ∘⇩c (g ∘⇩c f)"
by (typecheck_cfuncs, smt comp_associative2 left_coproj_cfunc_bowtie_prod left_proj_type assms)
have right_eq: " ((g ⨝⇩f id⇩c X) ∘⇩c (f ⨝⇩f id⇩c X)) ∘⇩c right_coproj A X = right_coproj C X ∘⇩c id X"
by(typecheck_cfuncs, smt comp_associative2 id_right_unit2 right_coproj_cfunc_bowtie_prod right_proj_type assms)
show ?thesis
using assms left_eq right_eq uniqueness by (typecheck_cfuncs, auto)
qed
lemma coproduct_of_beta:
"β⇘X⇙ ⨿ β⇘Y⇙ = β⇘X∐Y⇙"
by (metis (full_types) cfunc_coprod_unique left_proj_type right_proj_type terminal_func_comp terminal_func_type)
lemma cfunc_bowtieprod_comp_cfunc_coprod:
assumes a_type: "a : Y → Z" and b_type: "b : W → Z"
assumes f_type: "f : X → Y" and g_type: "g : V → W"
shows "(a ⨿ b) ∘⇩c (f ⨝⇩f g) = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
proof -
from cfunc_bowtie_prod_unique have uniqueness:
"∀h. h : X ∐ V → Z ∧ h ∘⇩c left_coproj X V = a ∘⇩c f ∧ h ∘⇩c right_coproj X V = b ∘⇩c g ⟶
h = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
using assms comp_type by (metis (full_types) cfunc_coprod_unique)
have left_eq: "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ∘⇩c f)"
proof -
have "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ⨿ b) ∘⇩c (f ⨝⇩f g) ∘⇩c left_coproj X V"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (a ⨿ b) ∘⇩c left_coproj Y W ∘⇩c f"
using f_type g_type left_coproj_cfunc_bowtie_prod by auto
also have "... = ((a ⨿ b) ∘⇩c left_coproj Y W) ∘⇩c f"
using a_type assms(2) cfunc_type_def comp_associative f_type by (typecheck_cfuncs, auto)
also have "... = (a ∘⇩c f)"
using a_type b_type left_coproj_cfunc_coprod by presburger
finally show "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ∘⇩c f)".
qed
have right_eq: "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (b ∘⇩c g)"
proof -
have "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (a ⨿ b) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (a ⨿ b) ∘⇩c right_coproj Y W ∘⇩c g"
using f_type g_type right_coproj_cfunc_bowtie_prod by auto
also have "... = ((a ⨿ b) ∘⇩c right_coproj Y W) ∘⇩c g"
using a_type assms(2) cfunc_type_def comp_associative g_type by (typecheck_cfuncs, auto)
also have "... = (b ∘⇩c g)"
using a_type b_type right_coproj_cfunc_coprod by auto
finally show "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (b ∘⇩c g)".
qed
show "(a ⨿ b) ∘⇩c (f ⨝⇩f g) = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
using uniqueness left_eq right_eq assms
by (typecheck_cfuncs, auto)
qed
lemma id_bowtie_prod: "id(X) ⨝⇩f id(Y) = id(X ∐ Y)"
by (metis cfunc_bowtie_prod_def id_codomain id_coprod id_right_unit2 left_proj_type right_proj_type)
lemma cfunc_bowtie_prod_comp_cfunc_bowtie_prod:
assumes "f : X → Y" "g : V → W" "x : Y → S" "y : W → T"
shows "(x ⨝⇩f y) ∘⇩c (f ⨝⇩f g) = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
proof-
have "(x ⨝⇩f y) ∘⇩c ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g))
= ((x ⨝⇩f y) ∘⇩c left_coproj Y W ∘⇩c f) ⨿ ((x ⨝⇩f y) ∘⇩c right_coproj Y W ∘⇩c g)"
using assms by (typecheck_cfuncs, simp add: cfunc_coprod_comp)
also have "... = (((x ⨝⇩f y) ∘⇩c left_coproj Y W) ∘⇩c f) ⨿ (((x ⨝⇩f y) ∘⇩c right_coproj Y W) ∘⇩c g)"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ((left_coproj S T ∘⇩c x) ∘⇩c f) ⨿ ((right_coproj S T ∘⇩c y) ∘⇩c g)"
using assms(3,4) left_coproj_cfunc_bowtie_prod right_coproj_cfunc_bowtie_prod by auto
also have "... = (left_coproj S T ∘⇩c x ∘⇩c f) ⨿ (right_coproj S T ∘⇩c y ∘⇩c g)"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
using assms cfunc_bowtie_prod_def cfunc_type_def codomain_comp by auto
ultimately show "(x ⨝⇩f y) ∘⇩c (f ⨝⇩f g) = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
using assms(1,2) cfunc_bowtie_prod_def2 by auto
qed
lemma cfunc_bowtieprod_epi:
assumes f_type[type_rule]: "f : X → Y" and g_type[type_rule]: "g : V → W"
assumes f_epi: "epimorphism f" and g_epi: "epimorphism g"
shows "epimorphism (f ⨝⇩f g)"
proof (typecheck_cfuncs, unfold epimorphism_def3, clarify)
fix x y A
assume x_type: "x: Y ∐ W → A"
assume y_type: "y: Y ∐ W → A"
assume eqs: "x ∘⇩c f ⨝⇩f g = y ∘⇩c f ⨝⇩f g"
obtain x1 x2 where x_expand: "x = x1 ⨿ x2" and x1_x2_type: "x1 : Y → A" "x2 : W → A"
using coprod_decomp x_type by blast
obtain y1 y2 where y_expand: "y = y1 ⨿ y2" and y1_y2_type: "y1 : Y → A" "y2 : W → A"
using coprod_decomp y_type by blast
have "(x1 = y1) ∧ (x2 = y2)"
proof
have "x1 ∘⇩c f = ((x1 ⨿ x2) ∘⇩c left_coproj Y W) ∘⇩c f"
using x1_x2_type left_coproj_cfunc_coprod by auto
also have "... = (x1 ⨿ x2) ∘⇩c left_coproj Y W ∘⇩c f"
using assms comp_associative2 x_expand x_type by (typecheck_cfuncs, auto)
also have "... = (x1 ⨿ x2) ∘⇩c (f ⨝⇩f g) ∘⇩c left_coproj X V"
using left_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
also have "... = (y1 ⨿ y2) ∘⇩c (f ⨝⇩f g) ∘⇩c left_coproj X V"
using assms cfunc_type_def comp_associative eqs x_expand x_type y_expand y_type by (typecheck_cfuncs, auto)
also have "... = (y1 ⨿ y2) ∘⇩c left_coproj Y W ∘⇩c f"
using assms by (typecheck_cfuncs, simp add: left_coproj_cfunc_bowtie_prod)
also have "... = ((y1 ⨿ y2) ∘⇩c left_coproj Y W) ∘⇩c f"
using assms comp_associative2 y_expand y_type by (typecheck_cfuncs, blast)
also have "... = y1 ∘⇩c f"
using y1_y2_type left_coproj_cfunc_coprod by auto
ultimately show "x1 = y1"
using epimorphism_def3 f_epi f_type x1_x2_type(1) y1_y2_type(1) by fastforce
next
have "x2 ∘⇩c g = ((x1 ⨿ x2) ∘⇩c right_coproj Y W) ∘⇩c g"
using x1_x2_type right_coproj_cfunc_coprod by auto
also have "... = (x1 ⨿ x2) ∘⇩c right_coproj Y W ∘⇩c g"
using assms comp_associative2 x_expand x_type by (typecheck_cfuncs, auto)
also have "... = (x1 ⨿ x2) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
using right_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
also have "... = (y1 ⨿ y2) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
using assms cfunc_type_def comp_associative eqs x_expand x_type y_expand y_type by (typecheck_cfuncs, auto)
also have "... = (y1 ⨿ y2) ∘⇩c right_coproj Y W ∘⇩c g"
using assms by (typecheck_cfuncs, simp add: right_coproj_cfunc_bowtie_prod)
also have "... = ((y1 ⨿ y2) ∘⇩c right_coproj Y W) ∘⇩c g"
using assms comp_associative2 y_expand y_type by (typecheck_cfuncs, blast)
also have "... = y2 ∘⇩c g"
using right_coproj_cfunc_coprod y1_y2_type(1) y1_y2_type(2) by auto
ultimately show "x2 = y2"
using epimorphism_def3 g_epi g_type x1_x2_type(2) y1_y2_type(2) by fastforce
qed
then show "x = y"
by (simp add: x_expand y_expand)
qed
lemma cfunc_bowtieprod_inj:
assumes type_assms: "f : X → Y" "g : V → W"
assumes f_epi: "injective f" and g_epi: "injective g"
shows "injective (f ⨝⇩f g)"
unfolding injective_def
proof(clarify)
fix z1 z2
assume x_type: "z1 ∈⇩c domain (f ⨝⇩f g)"
assume y_type: "z2 ∈⇩c domain (f ⨝⇩f g)"
assume eqs: "(f ⨝⇩f g) ∘⇩c z1 = (f ⨝⇩f g) ∘⇩c z2"
have f_bowtie_g_type: "(f ⨝⇩f g) : X ∐ V → Y ∐ W"
by (simp add: cfunc_bowtie_prod_type type_assms(1) type_assms(2))
have x_type2: "z1 ∈⇩c X ∐ V"
using cfunc_type_def f_bowtie_g_type x_type by auto
have y_type2: "z2 ∈⇩c X ∐ V"
using cfunc_type_def f_bowtie_g_type y_type by auto
have z1_decomp: "(∃ x1. (x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1))
∨ (∃ y1. (y1 ∈⇩c V ∧ z1 = right_coproj X V ∘⇩c y1))"
by (simp add: coprojs_jointly_surj x_type2)
have z2_decomp: "(∃ x2. (x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2))
∨ (∃ y2. (y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2))"
by (simp add: coprojs_jointly_surj y_type2)
show "z1 = z2"
proof(cases "∃ x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1")
assume case1: "∃x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
obtain x1 where x1_def: "x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
using case1 by blast
show "z1 = z2"
proof(cases "∃ x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2")
assume caseA: "∃x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
show "z1 = z2"
proof -
obtain x2 where x2_def: "x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
using caseA by blast
have "x1 = x2"
proof -
have "left_coproj Y W ∘⇩c f ∘⇩c x1 = (left_coproj Y W ∘⇩c f) ∘⇩c x1"
using cfunc_type_def comp_associative left_proj_type type_assms(1) x1_def by auto
also have "... =
(((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x1"
using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x1"
using comp_associative2 type_assms x1_def by (typecheck_cfuncs, fastforce)
also have "... = (f ⨝⇩f g) ∘⇩c z1"
using cfunc_bowtie_prod_def2 type_assms x1_def by auto
also have "... = (f ⨝⇩f g) ∘⇩c z2"
by (meson eqs)
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x2"
using cfunc_bowtie_prod_def2 type_assms(1) type_assms(2) x2_def by auto
also have "... = ((((left_coproj Y W) ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x2"
by (typecheck_cfuncs, meson comp_associative2 type_assms(1) type_assms(2) x2_def)
also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x2"
using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = left_coproj Y W ∘⇩c f ∘⇩c x2"
by (metis comp_associative2 left_proj_type type_assms(1) x2_def)
ultimately have "f ∘⇩c x1 = f ∘⇩c x2"
using cfunc_type_def left_coproj_are_monomorphisms
left_proj_type monomorphism_def type_assms(1) x1_def x2_def by (typecheck_cfuncs,auto)
then show "x1 = x2"
by (metis cfunc_type_def f_epi injective_def type_assms(1) x1_def x2_def)
qed
then show "z1 = z2"
by (simp add: x1_def x2_def)
qed
next
assume caseB: "∄x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
then obtain y2 where y2_def: "(y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2)"
using z2_decomp by blast
have "left_coproj Y W ∘⇩c f ∘⇩c x1 = (left_coproj Y W ∘⇩c f) ∘⇩c x1"
using cfunc_type_def comp_associative left_proj_type type_assms(1) x1_def by auto
also have "... =
(((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x1"
using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x1"
using comp_associative2 type_assms(1,2) x1_def by (typecheck_cfuncs, fastforce)
also have "... = (f ⨝⇩f g) ∘⇩c z1"
using cfunc_bowtie_prod_def2 type_assms x1_def by auto
also have "... = (f ⨝⇩f g) ∘⇩c z2"
by (meson eqs)
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y2"
using cfunc_bowtie_prod_def2 type_assms y2_def by auto
also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y2"
by (typecheck_cfuncs, meson comp_associative2 type_assms y2_def)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y2"
using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
also have "... = right_coproj Y W ∘⇩c g ∘⇩c y2"
using comp_associative2 type_assms(2) y2_def by (typecheck_cfuncs, auto)
ultimately have False
using comp_type coproducts_disjoint type_assms x1_def y2_def by auto
then show "z1 = z2"
by simp
qed
next
assume case2: "∄x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
then obtain y1 where y1_def: "y1 ∈⇩c V ∧ z1 = right_coproj X V ∘⇩c y1"
using z1_decomp by blast
show "z1 = z2"
proof(cases "∃ x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2")
assume caseA: "∃x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
show "z1 = z2"
proof -
obtain x2 where x2_def: "x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
using caseA by blast
have "left_coproj Y W ∘⇩c f ∘⇩c x2 = (left_coproj Y W ∘⇩c f) ∘⇩c x2"
using comp_associative2 type_assms(1) x2_def by (typecheck_cfuncs, auto)
also have "... =
(((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x2"
using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x2"
using comp_associative2 type_assms x2_def by (typecheck_cfuncs, fastforce)
also have "... = (f ⨝⇩f g) ∘⇩c z2"
using cfunc_bowtie_prod_def2 type_assms x2_def by auto
also have "... = (f ⨝⇩f g) ∘⇩c z1"
by (simp add: eqs)
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y1"
using cfunc_bowtie_prod_def2 type_assms y1_def by auto
also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y1"
by (typecheck_cfuncs, meson comp_associative2 type_assms y1_def)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y1"
using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
also have "... = right_coproj Y W ∘⇩c g ∘⇩c y1"
using comp_associative2 type_assms(2) y1_def by (typecheck_cfuncs, auto)
ultimately have False
using comp_type coproducts_disjoint type_assms x2_def y1_def by auto
then show "z1 = z2"
by simp
qed
next
assume caseB: "∄x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
then obtain y2 where y2_def: "(y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2)"
using z2_decomp by blast
have "y1 = y2"
proof -
have "right_coproj Y W ∘⇩c g ∘⇩c y1 = (right_coproj Y W ∘⇩c g) ∘⇩c y1"
using comp_associative2 type_assms(2) y1_def by (typecheck_cfuncs, auto)
also have "... =
(((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y1"
using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y1"
using comp_associative2 type_assms y1_def by (typecheck_cfuncs, fastforce)
also have "... = (f ⨝⇩f g) ∘⇩c z1"
using cfunc_bowtie_prod_def2 type_assms y1_def by auto
also have "... = (f ⨝⇩f g) ∘⇩c z2"
by (meson eqs)
also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y2"
using cfunc_bowtie_prod_def2 type_assms y2_def by auto
also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y2"
by (typecheck_cfuncs, meson comp_associative2 type_assms y2_def)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y2"
using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
also have "... = right_coproj Y W ∘⇩c g ∘⇩c y2"
using comp_associative2 type_assms(2) y2_def by (typecheck_cfuncs, auto)
ultimately have "g ∘⇩c y1 = g ∘⇩c y2"
using cfunc_type_def right_coproj_are_monomorphisms
right_proj_type monomorphism_def type_assms(2) y1_def y2_def by (typecheck_cfuncs,auto)
then show "y1 = y2"
by (metis cfunc_type_def g_epi injective_def type_assms(2) y1_def y2_def)
qed
then show "z1 = z2"
by (simp add: y1_def y2_def)
qed
qed
qed
lemma cfunc_bowtieprod_inj_converse:
assumes type_assms: "f : X → Y" "g : Z → W"
assumes inj_f_bowtie_g: "injective (f ⨝⇩f g)"
shows "injective f ∧ injective g"
unfolding injective_def
proof(safe)
fix x y
assume x_type: "x ∈⇩c domain f"
assume y_type: "y ∈⇩c domain f"
assume eqs: "f ∘⇩c x = f ∘⇩c y"
have x_type2: "x ∈⇩c X"
using cfunc_type_def type_assms(1) x_type by auto
have y_type2: "y ∈⇩c X"
using cfunc_type_def type_assms(1) y_type by auto
have fg_bowtie_tyepe: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
using assms by typecheck_cfuncs
have lift: "(f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c y"
proof -
have "(f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
using x_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x"
using left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
using x_type2 comp_associative2 type_assms(1) by (typecheck_cfuncs, auto)
also have "... = left_coproj Y W ∘⇩c f ∘⇩c y"
by (simp add: eqs)
also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c y"
using y_type2 comp_associative2 type_assms(1) by (typecheck_cfuncs, auto)
also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c y"
using left_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c y"
using y_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
then have "monomorphism (f ⨝⇩f g)"
using inj_f_bowtie_g injective_imp_monomorphism by auto
then have "left_coproj X Z ∘⇩c x = left_coproj X Z ∘⇩c y"
by (typecheck_cfuncs, metis cfunc_type_def fg_bowtie_tyepe inj_f_bowtie_g injective_def lift x_type2 y_type2)
then show "x = y"
using x_type2 y_type2 cfunc_type_def left_coproj_are_monomorphisms left_proj_type monomorphism_def by auto
next
fix x y
assume x_type: "x ∈⇩c domain g"
assume y_type: "y ∈⇩c domain g"
assume eqs: "g ∘⇩c x = g ∘⇩c y"
have x_type2: "x ∈⇩c Z"
using cfunc_type_def type_assms(2) x_type by auto
have y_type2: "y ∈⇩c Z"
using cfunc_type_def type_assms(2) y_type by auto
have fg_bowtie_tyepe: "f ⨝⇩f g : X ∐ Z → Y ∐ W"
using assms by typecheck_cfuncs
have lift: "(f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c x = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c y"
proof -
have "(f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c x = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c x"
using x_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c x"
using right_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = right_coproj Y W ∘⇩c g ∘⇩c x"
using x_type2 comp_associative2 type_assms(2) by (typecheck_cfuncs, auto)
also have "... = right_coproj Y W ∘⇩c g ∘⇩c y"
by (simp add: eqs)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y"
using y_type2 comp_associative2 type_assms(2) by (typecheck_cfuncs, auto)
also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c y"
using right_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c y"
using y_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
then have "monomorphism (f ⨝⇩f g)"
using inj_f_bowtie_g injective_imp_monomorphism by auto
then have "right_coproj X Z ∘⇩c x = right_coproj X Z ∘⇩c y"
by (typecheck_cfuncs, metis cfunc_type_def fg_bowtie_tyepe inj_f_bowtie_g injective_def lift x_type2 y_type2)
then show "x = y"
using x_type2 y_type2 cfunc_type_def right_coproj_are_monomorphisms right_proj_type monomorphism_def by auto
qed
lemma cfunc_bowtieprod_iso:
assumes type_assms: "f : X → Y" "g : V → W"
assumes f_iso: "isomorphism f" and g_iso: "isomorphism g"
shows "isomorphism (f ⨝⇩f g)"
by (typecheck_cfuncs, meson cfunc_bowtieprod_epi cfunc_bowtieprod_inj epi_mon_is_iso f_iso g_iso injective_imp_monomorphism iso_imp_epi_and_monic monomorphism_imp_injective singletonI assms)
lemma cfunc_bowtieprod_surj_converse:
assumes type_assms: "f : X → Y" "g : Z → W"
assumes inj_f_bowtie_g: "surjective (f ⨝⇩f g)"
shows "surjective f ∧ surjective g"
unfolding surjective_def
proof(safe)
fix y
assume y_type: "y ∈⇩c codomain f"
then have y_type2: "y ∈⇩c Y"
using cfunc_type_def type_assms(1) by auto
then have coproj_y_type: "left_coproj Y W ∘⇩c y ∈⇩c Y ∐ W"
by typecheck_cfuncs
have fg_type: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
using assms by typecheck_cfuncs
obtain xz where xz_def: "xz ∈⇩c X ∐ Z ∧ (f ⨝⇩f g) ∘⇩c xz = left_coproj Y W ∘⇩c y"
using fg_type y_type2 cfunc_type_def inj_f_bowtie_g surjective_def by (typecheck_cfuncs, auto)
then have xz_form: "(∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz) ∨
(∃ z. z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz)"
using coprojs_jointly_surj xz_def by (typecheck_cfuncs, blast)
show "∃ x. x ∈⇩c domain f ∧ f ∘⇩c x = y"
proof(cases "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz")
assume "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
then obtain x where x_def: "x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
by blast
have "f ∘⇩c x = y"
proof -
have "left_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
by (simp add: xz_def)
also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x"
by (simp add: x_def)
also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
using comp_associative2 fg_type x_def by (typecheck_cfuncs, auto)
also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x"
using left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
using comp_associative2 type_assms(1) x_def by (typecheck_cfuncs, auto)
ultimately show "f ∘⇩c x = y"
using type_assms(1) x_def y_type2
by (typecheck_cfuncs, metis cfunc_type_def left_coproj_are_monomorphisms left_proj_type monomorphism_def x_def)
qed
then show ?thesis
using cfunc_type_def type_assms(1) x_def by auto
next
assume "∄x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
then obtain z where z_def: "z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz"
using xz_form by blast
have False
proof -
have "left_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
by (simp add: xz_def)
also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c z"
by (simp add: z_def)
also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c z"
using comp_associative2 fg_type z_def by (typecheck_cfuncs, auto)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c z"
using right_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = right_coproj Y W ∘⇩c g ∘⇩c z"
using comp_associative2 type_assms(2) z_def by (typecheck_cfuncs, auto)
ultimately show False
using comp_type coproducts_disjoint type_assms(2) y_type2 z_def by auto
qed
then show ?thesis
by simp
qed
next
fix y
assume y_type: "y ∈⇩c codomain g"
then have y_type2: "y ∈⇩c W"
using cfunc_type_def type_assms(2) by auto
then have coproj_y_type: "(right_coproj Y W) ∘⇩c y ∈⇩c (Y ∐ W)"
using cfunc_type_def comp_type right_proj_type type_assms(2) by auto
have fg_type: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
by (simp add: cfunc_bowtie_prod_type type_assms)
obtain xz where xz_def: "xz ∈⇩c X ∐ Z ∧ (f ⨝⇩f g) ∘⇩c xz = right_coproj Y W ∘⇩c y"
using fg_type y_type2 cfunc_type_def inj_f_bowtie_g surjective_def by (typecheck_cfuncs, auto)
then have xz_form: "(∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz) ∨
(∃ z. z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz)"
using coprojs_jointly_surj xz_def by (typecheck_cfuncs, blast)
show "∃x. x ∈⇩c domain g ∧ g ∘⇩c x = y"
proof(cases "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz")
assume "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
then obtain x where x_def: "x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
by blast
have False
proof -
have "right_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
by (simp add: xz_def)
also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x"
by (simp add: x_def)
also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
using comp_associative2 fg_type x_def by (typecheck_cfuncs, auto)
also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x"
using left_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
using comp_associative2 type_assms(1) x_def by (typecheck_cfuncs, auto)
ultimately show False
by (metis comp_type coproducts_disjoint type_assms(1) x_def y_type2)
qed
then show ?thesis
by simp
next
assume "∄x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
then obtain z where z_def: "z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz"
using xz_form by blast
have "g ∘⇩c z = y"
proof -
have "right_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
by (simp add: xz_def)
also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c z"
by (simp add: z_def)
also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c z"
using comp_associative2 fg_type z_def by (typecheck_cfuncs, auto)
also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c z"
using right_coproj_cfunc_bowtie_prod type_assms by auto
also have "... = right_coproj Y W ∘⇩c g ∘⇩c z"
using comp_associative2 type_assms(2) z_def by (typecheck_cfuncs, auto)
ultimately show ?thesis
by (metis cfunc_type_def codomain_comp monomorphism_def
right_coproj_are_monomorphisms right_proj_type type_assms(2) y_type2 z_def)
qed
then show ?thesis
using cfunc_type_def type_assms(2) z_def by auto
qed
qed
subsection ‹Boolean Cases›
definition case_bool :: "cfunc" where
"case_bool = (THE f. f : Ω → (𝟭 ∐ 𝟭) ∧
(𝗍 ⨿ 𝖿) ∘⇩c f = id Ω ∧ f ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭))"
lemma case_bool_def2:
"case_bool : Ω → (𝟭 ∐ 𝟭) ∧
(𝗍 ⨿ 𝖿) ∘⇩c case_bool = id Ω ∧ case_bool ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭)"
unfolding case_bool_def
proof (rule theI', safe)
show "∃x. x : Ω → 𝟭 ∐ 𝟭 ∧ 𝗍 ⨿ 𝖿 ∘⇩c x = id⇩c Ω ∧ x ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)"
unfolding isomorphism_def
using isomorphism_def3 truth_value_set_iso_1u1 by (typecheck_cfuncs, blast)
next
fix x y
assume x_type[type_rule]: "x : Ω → 𝟭 ∐ 𝟭" and y_type[type_rule]: "y : Ω → 𝟭 ∐ 𝟭"
assume x_left_inv: "𝗍 ⨿ 𝖿 ∘⇩c x = id⇩c Ω"
assume "x ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)" "y ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)"
then have "x ∘⇩c 𝗍 ⨿ 𝖿 = y ∘⇩c 𝗍 ⨿ 𝖿"
by auto
then have "x ∘⇩c 𝗍 ⨿ 𝖿 ∘⇩c x = y ∘⇩c 𝗍 ⨿ 𝖿 ∘⇩c x"
by (typecheck_cfuncs, auto simp add: comp_associative2)
then show "x = y"
using id_right_unit2 x_left_inv by (typecheck_cfuncs_prems, auto)
qed
lemma case_bool_type[type_rule]:
"case_bool : Ω → 𝟭 ∐ 𝟭"
using case_bool_def2 by auto
lemma case_bool_true_coprod_false:
"case_bool ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭)"
using case_bool_def2 by auto
lemma true_coprod_false_case_bool:
"(𝗍 ⨿ 𝖿) ∘⇩c case_bool = id Ω"
using case_bool_def2 by auto
lemma case_bool_iso:
"isomorphism case_bool"
using case_bool_def2 unfolding isomorphism_def
by (intro exI[where x="𝗍 ⨿ 𝖿"], typecheck_cfuncs, auto simp add: cfunc_type_def)
lemma case_bool_true_and_false:
"(case_bool ∘⇩c 𝗍 = left_coproj 𝟭 𝟭) ∧ (case_bool ∘⇩c 𝖿 = right_coproj 𝟭 𝟭)"
proof -
have "(left_coproj 𝟭 𝟭) ⨿ (right_coproj 𝟭 𝟭) = id(𝟭 ∐ 𝟭)"
by (simp add: id_coprod)
also have "... = case_bool ∘⇩c (𝗍 ⨿ 𝖿)"
by (simp add: case_bool_def2)
also have "... = (case_bool ∘⇩c 𝗍) ⨿ (case_bool ∘⇩c 𝖿)"
using case_bool_def2 cfunc_coprod_comp false_func_type true_func_type by auto
ultimately show ?thesis
using coprod_eq2 by (typecheck_cfuncs, auto)
qed
lemma case_bool_true:
"case_bool ∘⇩c 𝗍 = left_coproj 𝟭 𝟭"
by (simp add: case_bool_true_and_false)
lemma case_bool_false:
"case_bool ∘⇩c 𝖿 = right_coproj 𝟭 𝟭"
by (simp add: case_bool_true_and_false)
lemma coprod_case_bool_true:
assumes "x1 ∈⇩c X"
assumes "x2 ∈⇩c X"
shows "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝗍 = x1"
proof -
have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝗍 = (x1 ⨿ x2) ∘⇩c case_bool ∘⇩c 𝗍"
using assms by (typecheck_cfuncs , simp add: comp_associative2)
also have "... = (x1 ⨿ x2) ∘⇩c left_coproj 𝟭 𝟭"
using assms case_bool_true by presburger
also have "... = x1"
using assms left_coproj_cfunc_coprod by force
finally show ?thesis.
qed
lemma coprod_case_bool_false:
assumes "x1 ∈⇩c X"
assumes "x2 ∈⇩c X"
shows "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝖿 = x2"
proof -
have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝖿 = (x1 ⨿ x2) ∘⇩c case_bool ∘⇩c 𝖿"
using assms by (typecheck_cfuncs , simp add: comp_associative2)
also have "... = (x1 ⨿ x2) ∘⇩c right_coproj 𝟭 𝟭"
using assms case_bool_false by presburger
also have "... = x2"
using assms right_coproj_cfunc_coprod by force
finally show ?thesis.
qed
subsection ‹Distribution of Products over Coproducts›
subsubsection ‹Factor Product over Coproduct on Left›
definition factor_prod_coprod_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
"factor_prod_coprod_left A B C = (id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)"
lemma factor_prod_coprod_left_type[type_rule]:
"factor_prod_coprod_left A B C : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
unfolding factor_prod_coprod_left_def by typecheck_cfuncs
lemma factor_prod_coprod_left_ap_left:
assumes "a ∈⇩c A" "b ∈⇩c B"
shows "factor_prod_coprod_left A B C ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, b⟩ = ⟨a, left_coproj B C ∘⇩c b⟩"
unfolding factor_prod_coprod_left_def using assms
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 left_coproj_cfunc_coprod)
lemma factor_prod_coprod_left_ap_right:
assumes "a ∈⇩c A" "c ∈⇩c C"
shows "factor_prod_coprod_left A B C ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, c⟩ = ⟨a, right_coproj B C ∘⇩c c⟩"
unfolding factor_prod_coprod_left_def using assms
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 right_coproj_cfunc_coprod)
lemma factor_prod_coprod_left_mono:
"monomorphism (factor_prod_coprod_left A B C)"
proof -
obtain φ where φ_def: "φ = (id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)" and
φ_type[type_rule]: "φ : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
by (typecheck_cfuncs, simp)
have injective: "injective(φ)"
unfolding injective_def
proof(clarify)
fix x y
assume x_type: "x ∈⇩c domain φ"
assume y_type: "y ∈⇩c domain φ"
assume equal: "φ ∘⇩c x = φ ∘⇩c y"
have x_type[type_rule]: "x ∈⇩c (A ×⇩c B) ∐ (A ×⇩c C)"
using cfunc_type_def φ_type x_type by auto
then have x_form: "(∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')
∨ (∃ x'. x' ∈⇩c A ×⇩c C ∧ x = (right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')"
by (simp add: coprojs_jointly_surj)
have y_type[type_rule]: "y ∈⇩c (A ×⇩c B) ∐ (A ×⇩c C)"
using cfunc_type_def φ_type y_type by auto
then have y_form: "(∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y')
∨ (∃ y'. y' ∈⇩c A ×⇩c C ∧ y = (right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y')"
by (simp add: coprojs_jointly_surj)
show "x = y"
proof(cases "(∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')")
assume "∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x'"
then obtain x' where x'_def[type_rule]: "x' ∈⇩c A ×⇩c B" "x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
by blast
then have ab_exists: "∃ a b. a ∈⇩c A ∧ b ∈⇩c B ∧ x' =⟨a,b⟩"
using cart_prod_decomp by blast
then obtain a b where ab_def[type_rule]: "a ∈⇩c A" "b ∈⇩c B" "x' =⟨a,b⟩"
by blast
show "x = y"
proof(cases "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y'")
assume "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y'"
then obtain y' where y'_def: "y' ∈⇩c A ×⇩c B" "y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
by blast
then have ab_exists: "∃ a' b'. a' ∈⇩c A ∧ b' ∈⇩c B ∧ y' =⟨a',b'⟩"
using cart_prod_decomp by blast
then obtain a' b' where a'b'_def[type_rule]: "a' ∈⇩c A" "b' ∈⇩c B" "y' =⟨a',b'⟩"
by blast
have equal_pair: "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩"
proof -
have "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨id A ∘⇩c a, left_coproj B C ∘⇩c b⟩"
using ab_def id_left_unit2 by force
also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨a, b⟩"
by (smt ab_def cfunc_cross_prod_comp_cfunc_prod id_type left_proj_type)
also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = φ ∘⇩c x"
using ab_def comp_associative2 x'_def by (typecheck_cfuncs, fastforce)
also have "... = φ ∘⇩c y"
by (simp add: local.equal)
also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', b'⟩"
using a'b'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨ a', b'⟩"
unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = ⟨id A ∘⇩c a', left_coproj B C ∘⇩c b'⟩"
using a'b'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, auto)
also have "... = ⟨a', left_coproj B C ∘⇩c b'⟩"
using a'b'_def id_left_unit2 by force
finally show "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩".
qed
then have a_equal: "a = a' ∧ left_coproj B C ∘⇩c b = left_coproj B C ∘⇩c b'"
using a'b'_def ab_def cart_prod_eq2 equal_pair by (typecheck_cfuncs, blast)
then have b_equal: "b = b'"
using a'b'_def a_equal ab_def left_coproj_are_monomorphisms left_proj_type monomorphism_def3 by blast
then show "x = y"
by (simp add: a'b'_def a_equal ab_def x'_def y'_def)
next
assume "∄y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
then obtain y' where y'_def: "y' ∈⇩c A ×⇩c C" "y = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
using y_form by blast
then obtain a' c' where a'c'_def: "a' ∈⇩c A" "c' ∈⇩c C" "y' =⟨a',c'⟩"
by (meson cart_prod_decomp)
have equal_pair: "⟨a, (left_coproj B C) ∘⇩c b⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩"
proof -
have "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨id A ∘⇩c a, left_coproj B C ∘⇩c b⟩"
using ab_def id_left_unit2 by force
also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨a, b⟩"
by (smt ab_def cfunc_cross_prod_comp_cfunc_prod id_type left_proj_type)
also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = φ ∘⇩c x"
using ab_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
also have "... = φ ∘⇩c y"
by (simp add: local.equal)
also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', c'⟩"
using a'c'_def comp_associative2 y'_def by (typecheck_cfuncs, blast)
also have "... = (id A ×⇩f right_coproj B C) ∘⇩c ⟨a', c'⟩"
unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = ⟨id A ∘⇩c a', right_coproj B C ∘⇩c c'⟩"
using a'c'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
also have "... = ⟨a', right_coproj B C ∘⇩c c'⟩"
using a'c'_def id_left_unit2 by force
finally show "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩".
qed
then have impossible: "left_coproj B C ∘⇩c b = right_coproj B C ∘⇩c c'"
using a'c'_def ab_def element_pair_eq equal_pair by (typecheck_cfuncs, blast)
then show "x = y"
using a'c'_def ab_def coproducts_disjoint by blast
qed
next
assume "∄x'. x' ∈⇩c A ×⇩c B ∧ x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
then obtain x' where x'_def: "x' ∈⇩c A ×⇩c C" "x = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
using x_form by blast
then have ac_exists: "∃ a c. a ∈⇩c A ∧ c ∈⇩c C ∧ x' =⟨a,c⟩"
using cart_prod_decomp by blast
then obtain a c where ac_def: "a ∈⇩c A" "c ∈⇩c C" "x' =⟨a,c⟩"
by blast
show "x = y"
proof(cases "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'")
assume "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
then obtain y' where y'_def: "y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
by blast
then obtain a' b' where a'b'_def: "a' ∈⇩c A ∧ b' ∈⇩c B ∧ y' =⟨a',b'⟩"
using cart_prod_decomp y'_def by blast
have equal_pair: "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩"
proof -
have "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨id(A) ∘⇩c a, right_coproj B C ∘⇩c c⟩"
using ac_def id_left_unit2 by force
also have "... = (id A ×⇩f right_coproj B C) ∘⇩c ⟨a, c⟩"
by (smt ac_def cfunc_cross_prod_comp_cfunc_prod id_type right_proj_type)
also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = φ ∘⇩c x"
using ac_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
also have "... = φ ∘⇩c y"
by (simp add: local.equal)
also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', b'⟩"
using a'b'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨a', b'⟩"
unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = ⟨id A ∘⇩c a', left_coproj B C ∘⇩c b'⟩"
using a'b'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
also have "... = ⟨a', left_coproj B C ∘⇩c b'⟩"
using a'b'_def id_left_unit2 by force
finally show "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩".
qed
then have impossible: "right_coproj B C ∘⇩c c = left_coproj B C ∘⇩c b'"
using a'b'_def ac_def cart_prod_eq2 equal_pair by (typecheck_cfuncs, blast)
then show "x = y"
using a'b'_def ac_def coproducts_disjoint by force
next
assume "∄y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
then obtain y' where y'_def: "y' ∈⇩c (A ×⇩c C) ∧ y = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
using y_form by blast
then obtain a' c' where a'c'_def: "a' ∈⇩c A" "c' ∈⇩c C" "y' =⟨a',c'⟩"
using cart_prod_decomp by blast
have equal_pair: "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩"
proof -
have "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨id A ∘⇩c a, right_coproj B C ∘⇩c c⟩"
using ac_def id_left_unit2 by force
also have "... = (id A ×⇩f right_coproj B C) ∘⇩c ⟨a, c⟩"
by (smt ac_def cfunc_cross_prod_comp_cfunc_prod id_type right_proj_type)
also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = φ ∘⇩c x"
using ac_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
also have "... = φ ∘⇩c y"
by (simp add: local.equal)
also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', c'⟩"
using a'c'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
also have "... = (id A ×⇩f right_coproj B C) ∘⇩c ⟨a', c'⟩"
unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = ⟨id A ∘⇩c a', right_coproj B C ∘⇩c c'⟩"
using a'c'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
also have "... = ⟨a', right_coproj B C ∘⇩c c'⟩"
using a'c'_def id_left_unit2 by force
finally show "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩".
qed
then have a_equal: "a = a' ∧ right_coproj B C ∘⇩c c = right_coproj B C ∘⇩c c'"
using a'c'_def ac_def element_pair_eq equal_pair by (typecheck_cfuncs, blast)
then have c_equal: "c = c'"
using a'c'_def a_equal ac_def right_coproj_are_monomorphisms right_proj_type monomorphism_def3 by blast
then show "x = y"
by (simp add: a'c'_def a_equal ac_def x'_def y'_def)
qed
qed
qed
then show "monomorphism (factor_prod_coprod_left A B C)"
using φ_def factor_prod_coprod_left_def injective_imp_monomorphism by fastforce
qed
lemma factor_prod_coprod_left_epi:
"epimorphism (factor_prod_coprod_left A B C)"
proof -
obtain φ where φ_def: "φ = (id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)" and
φ_type[type_rule]: "φ : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
by (typecheck_cfuncs, simp)
have surjective: "surjective((id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C))"
unfolding surjective_def
proof(clarify)
fix y
assume y_type: "y ∈⇩c codomain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
then have y_type2: "y ∈⇩c A ×⇩c (B ∐ C)"
using φ_def φ_type cfunc_type_def by auto
then obtain a where a_def: "∃ bc. a ∈⇩c A ∧ bc ∈⇩c B ∐ C ∧ y = ⟨a,bc⟩"
by (meson cart_prod_decomp)
then obtain bc where bc_def: "bc ∈⇩c (B ∐ C) ∧ y = ⟨a,bc⟩"
by blast
have bc_form: "(∃ b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b) ∨ (∃ c. c ∈⇩c C ∧ bc = right_coproj B C ∘⇩c c)"
by (simp add: bc_def coprojs_jointly_surj)
have domain_is: "(A ×⇩c B) ∐ (A ×⇩c C) = domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
by (typecheck_cfuncs, simp add: cfunc_type_def)
show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
(id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
proof(cases "∃ b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b")
assume case1: "∃b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
then obtain b where b_def: "b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
by blast
then have ab_type: "⟨a, b⟩ ∈⇩c (A ×⇩c B)"
using a_def b_def by (typecheck_cfuncs, blast)
obtain x where x_def: "x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, b⟩"
by simp
have x_type: "x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
using ab_type cfunc_type_def codomain_comp domain_comp domain_is left_proj_type x_def by auto
have y_def2: "y = ⟨a,left_coproj B C ∘⇩c b⟩"
by (simp add: b_def bc_def)
have "y = (id(A) ×⇩f left_coproj B C) ∘⇩c ⟨a,b⟩"
using a_def b_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 y_def2 by (typecheck_cfuncs, auto)
also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
unfolding φ_def by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
also have "... = φ ∘⇩c x"
using φ_type x_def ab_type comp_associative2 by (typecheck_cfuncs, auto)
ultimately show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
(id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
using φ_def x_type by auto
next
assume "∄b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
then have case2: "∃ c. c ∈⇩c C ∧ bc = (right_coproj B C ∘⇩c c)"
using bc_form by blast
then obtain c where c_def: "c ∈⇩c C ∧ bc = right_coproj B C ∘⇩c c"
by blast
then have ac_type: "⟨a, c⟩ ∈⇩c (A ×⇩c C)"
using a_def c_def by (typecheck_cfuncs, blast)
obtain x where x_def: "x = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, c⟩"
by simp
have x_type: "x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
using ac_type cfunc_type_def codomain_comp domain_comp domain_is right_proj_type x_def by auto
have y_def2: "y = ⟨a,right_coproj B C ∘⇩c c⟩"
by (simp add: c_def bc_def)
have "y = (id(A) ×⇩f right_coproj B C) ∘⇩c ⟨a,c⟩"
using a_def c_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 y_def2 by (typecheck_cfuncs, auto)
also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = φ ∘⇩c x"
using φ_type x_def ac_type comp_associative2 by (typecheck_cfuncs, auto)
ultimately show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
(id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
using φ_def x_type by auto
qed
qed
then show "epimorphism (factor_prod_coprod_left A B C)"
by (simp add: factor_prod_coprod_left_def surjective_is_epimorphism)
qed
lemma dist_prod_coprod_iso:
"isomorphism(factor_prod_coprod_left A B C)"
by (simp add: factor_prod_coprod_left_epi factor_prod_coprod_left_mono epi_mon_is_iso)
text ‹The lemma below corresponds to Proposition 2.5.10 in Halvorson.›
lemma prod_distribute_coprod:
"A ×⇩c (X ∐ Y) ≅ (A ×⇩c X) ∐ (A ×⇩c Y)"
using dist_prod_coprod_iso factor_prod_coprod_left_type is_isomorphic_def isomorphic_is_symmetric by blast
subsubsection ‹Distribute Product over Coproduct on Left›
definition dist_prod_coprod_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
"dist_prod_coprod_left A B C = (THE f. f : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)
∧ f ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))
∧ factor_prod_coprod_left A B C ∘⇩c f = id (A ×⇩c (B ∐ C)))"
lemma dist_prod_coprod_left_def2:
shows "dist_prod_coprod_left A B C : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)
∧ dist_prod_coprod_left A B C ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))
∧ factor_prod_coprod_left A B C ∘⇩c dist_prod_coprod_left A B C = id (A ×⇩c (B ∐ C))"
unfolding dist_prod_coprod_left_def
proof (rule theI', safe)
show "∃x. x : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C ∧
x ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C) ∧
factor_prod_coprod_left A B C ∘⇩c x = id⇩c (A ×⇩c B ∐ C)"
using dist_prod_coprod_iso[where A=A, where B=B, where C=C] unfolding isomorphism_def
by (typecheck_cfuncs, auto simp add: cfunc_type_def)
then obtain inv where inv_type: "inv : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C" and
inv_left: "inv ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)" and
inv_right: "factor_prod_coprod_left A B C ∘⇩c inv = id⇩c (A ×⇩c B ∐ C)"
by auto
fix x y
assume x_type: "x : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C"
assume y_type: "y : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C"
assume "x ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)"
and "y ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)"
then have "x ∘⇩c factor_prod_coprod_left A B C = y ∘⇩c factor_prod_coprod_left A B C"
by auto
then have "(x ∘⇩c factor_prod_coprod_left A B C) ∘⇩c inv = (y ∘⇩c factor_prod_coprod_left A B C) ∘⇩c inv"
by auto
then have "x ∘⇩c factor_prod_coprod_left A B C ∘⇩c inv = y ∘⇩c factor_prod_coprod_left A B C ∘⇩c inv"
using inv_type x_type y_type by (typecheck_cfuncs, auto simp add: comp_associative2)
then have "x ∘⇩c id⇩c (A ×⇩c B ∐ C) = y ∘⇩c id⇩c (A ×⇩c B ∐ C)"
by (simp add: inv_right)
then show "x = y"
using id_right_unit2 x_type y_type by auto
qed
lemma dist_prod_coprod_left_type[type_rule]:
"dist_prod_coprod_left A B C : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)"
by (simp add: dist_prod_coprod_left_def2)
lemma dist_factor_prod_coprod_left:
"dist_prod_coprod_left A B C ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))"
by (simp add: dist_prod_coprod_left_def2)
lemma factor_dist_prod_coprod_left:
"factor_prod_coprod_left A B C ∘⇩c dist_prod_coprod_left A B C = id (A ×⇩c (B ∐ C))"
by (simp add: dist_prod_coprod_left_def2)
lemma dist_prod_coprod_left_iso:
"isomorphism(dist_prod_coprod_left A B C)"
by (metis factor_dist_prod_coprod_left dist_prod_coprod_left_type dist_prod_coprod_iso factor_prod_coprod_left_type id_isomorphism id_right_unit2 id_type isomorphism_sandwich)
lemma dist_prod_coprod_left_ap_left:
assumes "a ∈⇩c A" "b ∈⇩c B"
shows "dist_prod_coprod_left A B C ∘⇩c ⟨a,left_coproj B C ∘⇩c b⟩ = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a,b⟩"
using assms by (typecheck_cfuncs, smt comp_associative2 dist_prod_coprod_left_def2 factor_prod_coprod_left_ap_left factor_prod_coprod_left_type id_left_unit2)
lemma dist_prod_coprod_left_ap_right:
assumes "a ∈⇩c A" "c ∈⇩c C"
shows "dist_prod_coprod_left A B C ∘⇩c ⟨a,right_coproj B C ∘⇩c c⟩ = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a,c⟩"
using assms by (typecheck_cfuncs, smt comp_associative2 dist_prod_coprod_left_def2 factor_prod_coprod_left_ap_right factor_prod_coprod_left_type id_left_unit2)
subsubsection ‹Factor Product over Coproduct on Right›
definition factor_prod_coprod_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
"factor_prod_coprod_right A B C = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)"
lemma factor_prod_coprod_right_type[type_rule]:
"factor_prod_coprod_right A B C : (A ×⇩c C) ∐ (B ×⇩c C) → (A ∐ B) ×⇩c C"
unfolding factor_prod_coprod_right_def by typecheck_cfuncs
lemma factor_prod_coprod_right_ap_left:
assumes "a ∈⇩c A" "c ∈⇩c C"
shows "factor_prod_coprod_right A B C ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩) = ⟨left_coproj A B ∘⇩c a, c⟩"
proof -
have "factor_prod_coprod_right A B C ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩)
= (swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)) ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩)"
unfolding factor_prod_coprod_right_def by auto
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c ((swap A C ⨝⇩f swap B C) ∘⇩c left_coproj (A ×⇩c C) (B ×⇩c C)) ∘⇩c ⟨a, c⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap A C) ∘⇩c ⟨a, c⟩"
using assms by (typecheck_cfuncs, auto simp add: left_coproj_cfunc_bowtie_prod)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap A C ∘⇩c ⟨a, c⟩"
using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, a⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
also have "... = swap C (A ∐ B) ∘⇩c ⟨c, left_coproj A B ∘⇩c a⟩"
using assms by (typecheck_cfuncs, simp add: factor_prod_coprod_left_ap_left)
also have "... = ⟨left_coproj A B ∘⇩c a, c⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
lemma factor_prod_coprod_right_ap_right:
assumes "b ∈⇩c B" "c ∈⇩c C"
shows "factor_prod_coprod_right A B C ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩ = ⟨right_coproj A B ∘⇩c b, c⟩"
proof -
have "factor_prod_coprod_right A B C ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩
= (swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)) ∘⇩c (right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩)"
unfolding factor_prod_coprod_right_def by auto
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c ((swap A C ⨝⇩f swap B C) ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C)) ∘⇩c ⟨b, c⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap B C) ∘⇩c ⟨b, c⟩"
using assms by (typecheck_cfuncs, auto simp add: right_coproj_cfunc_bowtie_prod)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap B C ∘⇩c ⟨b, c⟩"
using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, b⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
also have "... = swap C (A ∐ B) ∘⇩c ⟨c, right_coproj A B ∘⇩c b⟩"
using assms by (typecheck_cfuncs, simp add: factor_prod_coprod_left_ap_right)
also have "... = ⟨right_coproj A B ∘⇩c b, c⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
subsubsection ‹Distribute Product over Coproduct on Right›
definition dist_prod_coprod_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
"dist_prod_coprod_right A B C = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C"
lemma dist_prod_coprod_right_type[type_rule]:
"dist_prod_coprod_right A B C : (A ∐ B) ×⇩c C → (A ×⇩c C) ∐ (B ×⇩c C)"
unfolding dist_prod_coprod_right_def by typecheck_cfuncs
lemma dist_prod_coprod_right_ap_left:
assumes "a ∈⇩c A" "c ∈⇩c C"
shows "dist_prod_coprod_right A B C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩ = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩"
proof -
have "dist_prod_coprod_right A B C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩
= ((swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C) ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩"
unfolding dist_prod_coprod_right_def by auto
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c ⟨c, left_coproj A B ∘⇩c a⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, a⟩"
using assms by (typecheck_cfuncs, simp add: dist_prod_coprod_left_ap_left)
also have "... = ((swap C A ⨝⇩f swap C B) ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B)) ∘⇩c ⟨c, a⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C A) ∘⇩c ⟨c, a⟩"
using assms left_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, auto)
also have "... = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C A ∘⇩c ⟨c, a⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
lemma dist_prod_coprod_right_ap_right:
assumes "b ∈⇩c B" "c ∈⇩c C"
shows "dist_prod_coprod_right A B C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩ = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩"
proof -
have "dist_prod_coprod_right A B C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩
= ((swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C) ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩"
unfolding dist_prod_coprod_right_def by auto
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩"
using assms by (typecheck_cfuncs, smt comp_associative2)
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c ⟨c, right_coproj A B ∘⇩c b⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, b⟩"
using assms by (typecheck_cfuncs, simp add: dist_prod_coprod_left_ap_right)
also have "... = ((swap C A ⨝⇩f swap C B) ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B)) ∘⇩c ⟨c, b⟩"
using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = (right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C B) ∘⇩c ⟨c, b⟩"
using assms by (typecheck_cfuncs, auto simp add: right_coproj_cfunc_bowtie_prod)
also have "... = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C B ∘⇩c ⟨c, b⟩"
using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩"
using assms swap_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
lemma dist_prod_coprod_right_left_coproj:
"dist_prod_coprod_right X Y H ∘⇩c (left_coproj X Y ×⇩f id H) = left_coproj (X ×⇩c H) (Y ×⇩c H)"
by (typecheck_cfuncs, smt (z3) one_separator cart_prod_decomp cfunc_cross_prod_comp_cfunc_prod comp_associative2 dist_prod_coprod_right_ap_left id_left_unit2)
lemma dist_prod_coprod_right_right_coproj:
"dist_prod_coprod_right X Y H ∘⇩c (right_coproj X Y ×⇩f id H) = right_coproj (X ×⇩c H) (Y ×⇩c H)"
by (typecheck_cfuncs, smt (z3) one_separator cart_prod_decomp cfunc_cross_prod_comp_cfunc_prod comp_associative2 dist_prod_coprod_right_ap_right id_left_unit2)
lemma factor_dist_prod_coprod_right:
"factor_prod_coprod_right A B C ∘⇩c dist_prod_coprod_right A B C = id ((A ∐ B) ×⇩c C)"
unfolding factor_prod_coprod_right_def dist_prod_coprod_right_def
by (typecheck_cfuncs, smt (verit, best) cfunc_bowtie_prod_comp_cfunc_bowtie_prod comp_associative2 factor_dist_prod_coprod_left id_bowtie_prod id_left_unit2 swap_idempotent)
lemma dist_factor_prod_coprod_right:
"dist_prod_coprod_right A B C ∘⇩c factor_prod_coprod_right A B C = id ((A ×⇩c C) ∐ (B ×⇩c C))"
unfolding factor_prod_coprod_right_def dist_prod_coprod_right_def
by (typecheck_cfuncs, smt (verit, best) cfunc_bowtie_prod_comp_cfunc_bowtie_prod comp_associative2 dist_factor_prod_coprod_left id_bowtie_prod id_left_unit2 swap_idempotent)
lemma factor_prod_coprod_right_iso:
"isomorphism(factor_prod_coprod_right A B C)"
by (metis cfunc_type_def dist_factor_prod_coprod_right factor_prod_coprod_right_type factor_dist_prod_coprod_right dist_prod_coprod_right_type isomorphism_def)
subsection ‹Casting between Sets›
subsubsection ‹Going from a Set or its Complement to the Superset›
text ‹This subsection corresponds to Proposition 2.4.5 in Halvorson.›
definition into_super :: "cfunc ⇒ cfunc" where
"into_super m = m ⨿ m⇧c"
lemma into_super_type[type_rule]:
"monomorphism m ⟹ m : X → Y ⟹ into_super m : X ∐ (Y ∖ (X,m)) → Y"
unfolding into_super_def by typecheck_cfuncs
lemma into_super_mono:
assumes "monomorphism m" "m : X → Y"
shows "monomorphism (into_super m)"
proof (rule injective_imp_monomorphism, unfold injective_def, clarify)
fix x y
assume "x ∈⇩c domain (into_super m)" then have x_type: "x ∈⇩c X ∐ (Y ∖ (X,m))"
using assms cfunc_type_def into_super_type by auto
assume "y ∈⇩c domain (into_super m)" then have y_type: "y ∈⇩c X ∐ (Y ∖ (X,m))"
using assms cfunc_type_def into_super_type by auto
assume into_super_eq: "into_super m ∘⇩c x = into_super m ∘⇩c y"
have x_cases: "(∃ x'. x' ∈⇩c X ∧ x = left_coproj X (Y ∖ (X,m)) ∘⇩c x')
∨ (∃ x'. x' ∈⇩c Y ∖ (X,m) ∧ x = right_coproj X (Y ∖ (X,m)) ∘⇩c x')"
by (simp add: coprojs_jointly_surj x_type)
have y_cases: "(∃ y'. y' ∈⇩c X ∧ y = left_coproj X (Y ∖ (X,m)) ∘⇩c y')
∨ (∃ y'. y' ∈⇩c Y ∖ (X,m) ∧ y = right_coproj X (Y ∖ (X,m)) ∘⇩c y')"
by (simp add: coprojs_jointly_surj y_type)
show "x = y"
using x_cases y_cases
proof safe
fix x' y'
assume x'_type: "x' ∈⇩c X" and x_def: "x = left_coproj X (Y ∖ (X, m)) ∘⇩c x'"
assume y'_type: "y' ∈⇩c X" and y_def: "y = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
have "into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
using into_super_eq unfolding x_def y_def by auto
then have "(into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c y'"
using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
then have "m ∘⇩c x' = m ∘⇩c y'"
using assms unfolding into_super_def
by (simp add: complement_morphism_type left_coproj_cfunc_coprod)
then have "x' = y'"
using assms cfunc_type_def monomorphism_def x'_type y'_type by auto
then show "left_coproj X (Y ∖ (X, m)) ∘⇩c x' = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
by simp
next
fix x' y'
assume x'_type: "x' ∈⇩c X" and x_def: "x = left_coproj X (Y ∖ (X, m)) ∘⇩c x'"
assume y'_type: "y' ∈⇩c Y ∖ (X, m)" and y_def: "y = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
have "into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
using into_super_eq unfolding x_def y_def by auto
then have "(into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c y'"
using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
then have "m ∘⇩c x' = m⇧c ∘⇩c y'"
using assms unfolding into_super_def
by (simp add: complement_morphism_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
then have False
using assms complement_disjoint x'_type y'_type by blast
then show "left_coproj X (Y ∖ (X, m)) ∘⇩c x' = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
by auto
next
fix x' y'
assume x'_type: "x' ∈⇩c Y ∖ (X, m)" and x_def: "x = right_coproj X (Y ∖ (X, m)) ∘⇩c x'"
assume y'_type: "y' ∈⇩c X" and y_def: "y = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
have "into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
using into_super_eq unfolding x_def y_def by auto
then have "(into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c y'"
using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
then have "m⇧c ∘⇩c x' = m ∘⇩c y'"
using assms unfolding into_super_def
by (simp add: complement_morphism_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
then have False
using assms complement_disjoint x'_type y'_type by fastforce
then show "right_coproj X (Y ∖ (X, m)) ∘⇩c x' = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
by auto
next
fix x' y'
assume x'_type: "x' ∈⇩c Y ∖ (X, m)" and x_def: "x = right_coproj X (Y ∖ (X, m)) ∘⇩c x'"
assume y'_type: "y' ∈⇩c Y ∖ (X, m)" and y_def: "y = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
have "into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
using into_super_eq unfolding x_def y_def by auto
then have "(into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c y'"
using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
then have "m⇧c ∘⇩c x' = m⇧c ∘⇩c y'"
using assms unfolding into_super_def
by (simp add: complement_morphism_type right_coproj_cfunc_coprod)
then have "x' = y'"
using assms complement_morphism_mono complement_morphism_type monomorphism_def2 x'_type y'_type by blast
then show "right_coproj X (Y ∖ (X, m)) ∘⇩c x' = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
by simp
qed
qed
lemma into_super_epi:
assumes "monomorphism m" "m : X → Y"
shows "epimorphism (into_super m)"
proof (rule surjective_is_epimorphism, unfold surjective_def, clarify)
fix y
assume "y ∈⇩c codomain (into_super m)"
then have y_type: "y ∈⇩c Y"
using assms cfunc_type_def into_super_type by auto
have y_cases: "(characteristic_func m ∘⇩c y = 𝗍) ∨ (characteristic_func m ∘⇩c y = 𝖿)"
using y_type assms true_false_only_truth_values by (typecheck_cfuncs, blast)
then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
proof safe
assume "characteristic_func m ∘⇩c y = 𝗍"
then have "y ∈⇘Y⇙ (X, m)"
by (simp add: assms characteristic_func_true_relative_member y_type)
then obtain x where x_type: "x ∈⇩c X" and x_def: "y = m ∘⇩c x"
unfolding relative_member_def2 by (auto, unfold factors_through_def2, auto)
then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
unfolding into_super_def using assms cfunc_type_def comp_associative left_coproj_cfunc_coprod
by (intro exI[where x="left_coproj X (Y ∖ (X, m)) ∘⇩c x"], typecheck_cfuncs, metis)
next
assume "characteristic_func m ∘⇩c y = 𝖿"
then have "¬ y ∈⇘Y⇙ (X, m)"
by (simp add: assms characteristic_func_false_not_relative_member y_type)
then have "y ∈⇘Y⇙ (Y ∖ (X, m), m⇧c)"
by (simp add: assms not_in_subset_in_complement y_type)
then obtain x' where x'_type: "x' ∈⇩c Y ∖ (X, m)" and x'_def: "y = m⇧c ∘⇩c x'"
unfolding relative_member_def2 by (auto, unfold factors_through_def2, auto)
then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
unfolding into_super_def using assms cfunc_type_def comp_associative right_coproj_cfunc_coprod
by (intro exI[where x="right_coproj X (Y ∖ (X, m)) ∘⇩c x'"], typecheck_cfuncs, metis)
qed
qed
lemma into_super_iso:
assumes "monomorphism m" "m : X → Y"
shows "isomorphism (into_super m)"
using assms epi_mon_is_iso into_super_epi into_super_mono by auto
subsubsection ‹Going from a Set to a Subset or its Complement›
definition try_cast :: "cfunc ⇒ cfunc" where
"try_cast m = (THE m'. m' : codomain m → domain m ∐ ((codomain m) ∖ ((domain m),m))
∧ m' ∘⇩c into_super m = id (domain m ∐ (codomain m ∖ ((domain m),m)))
∧ into_super m ∘⇩c m' = id (codomain m))"
lemma try_cast_def2:
assumes "monomorphism m" "m : X → Y"
shows "try_cast m : codomain m → (domain m) ∐ ((codomain m) ∖ ((domain m),m))
∧ try_cast m ∘⇩c into_super m = id ((domain m) ∐ ((codomain m) ∖ ((domain m),m)))
∧ into_super m ∘⇩c try_cast m = id (codomain m)"
unfolding try_cast_def
proof (rule theI', safe)
show "∃x. x : codomain m → domain m ∐ (codomain m ∖ (domain m, m)) ∧
x ∘⇩c into_super m = id⇩c (domain m ∐ (codomain m ∖ (domain m, m))) ∧
into_super m ∘⇩c x = id⇩c (codomain m)"
using assms into_super_iso cfunc_type_def into_super_type unfolding isomorphism_def by fastforce
next
fix x y
assume x_type: "x : codomain m → domain m ∐ (codomain m ∖ (domain m, m))"
assume y_type: "y : codomain m → domain m ∐ (codomain m ∖ (domain m, m))"
assume "into_super m ∘⇩c x = id⇩c (codomain m)" and "into_super m ∘⇩c y = id⇩c (codomain m)"
then have "into_super m ∘⇩c x = into_super m ∘⇩c y"
by auto
then show "x = y"
using into_super_mono unfolding monomorphism_def
by (metis assms(1) cfunc_type_def into_super_type monomorphism_def x_type y_type)
qed
lemma try_cast_type[type_rule]:
assumes "monomorphism m" "m : X → Y"
shows "try_cast m : Y → X ∐ (Y ∖ (X,m))"
using assms cfunc_type_def try_cast_def2 by auto
lemma try_cast_into_super:
assumes "monomorphism m" "m : X → Y"
shows "try_cast m ∘⇩c into_super m = id (X ∐ (Y ∖ (X,m)))"
using assms cfunc_type_def try_cast_def2 by auto
lemma into_super_try_cast:
assumes "monomorphism m" "m : X → Y"
shows "into_super m ∘⇩c try_cast m = id Y"
using assms cfunc_type_def try_cast_def2 by auto
lemma try_cast_in_X:
assumes m_type: "monomorphism m" "m : X → Y"
assumes y_in_X: "y ∈⇘Y⇙ (X, m)"
shows "∃ x. x ∈⇩c X ∧ try_cast m ∘⇩c y = left_coproj X (Y ∖ (X,m)) ∘⇩c x"
proof -
have y_type: "y ∈⇩c Y"
using y_in_X unfolding relative_member_def2 by auto
obtain x where x_type: "x ∈⇩c X" and x_def: "y = m ∘⇩c x"
using y_in_X unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
then have "y = (into_super m ∘⇩c left_coproj X (Y ∖ (X,m))) ∘⇩c x"
unfolding into_super_def using complement_morphism_type left_coproj_cfunc_coprod m_type by auto
then have "y = into_super m ∘⇩c left_coproj X (Y ∖ (X,m)) ∘⇩c x"
using x_type m_type by (typecheck_cfuncs, simp add: comp_associative2)
then have "try_cast m ∘⇩c y = (try_cast m ∘⇩c into_super m) ∘⇩c left_coproj X (Y ∖ (X,m)) ∘⇩c x"
using x_type m_type by (typecheck_cfuncs, smt comp_associative2)
then have "try_cast m ∘⇩c y = left_coproj X (Y ∖ (X,m)) ∘⇩c x"
using m_type x_type by (typecheck_cfuncs, simp add: id_left_unit2 try_cast_into_super)
then show ?thesis
using x_type by blast
qed
lemma try_cast_not_in_X:
assumes m_type: "monomorphism m" "m : X → Y"
assumes y_in_X: "¬ y ∈⇘Y⇙ (X, m)" and y_type: "y ∈⇩c Y"
shows "∃ x. x ∈⇩c Y ∖ (X,m) ∧ try_cast m ∘⇩c y = right_coproj X (Y ∖ (X,m)) ∘⇩c x"
proof -
have y_in_complement: "y ∈⇘Y⇙ (Y ∖ (X,m), m⇧c)"
by (simp add: assms not_in_subset_in_complement)
then obtain x where x_type: "x ∈⇩c Y ∖ (X,m)" and x_def: "y = m⇧c ∘⇩c x"
unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
then have "y = (into_super m ∘⇩c right_coproj X (Y ∖ (X,m))) ∘⇩c x"
unfolding into_super_def using complement_morphism_type m_type right_coproj_cfunc_coprod by auto
then have "y = into_super m ∘⇩c right_coproj X (Y ∖ (X,m)) ∘⇩c x"
using x_type m_type by (typecheck_cfuncs, simp add: comp_associative2)
then have "try_cast m ∘⇩c y = (try_cast m ∘⇩c into_super m) ∘⇩c right_coproj X (Y ∖ (X,m)) ∘⇩c x"
using x_type m_type by (typecheck_cfuncs, smt comp_associative2)
then have "try_cast m ∘⇩c y = right_coproj X (Y ∖ (X,m)) ∘⇩c x"
using m_type x_type by (typecheck_cfuncs, simp add: id_left_unit2 try_cast_into_super)
then show ?thesis
using x_type by blast
qed
lemma try_cast_m_m:
assumes m_type: "monomorphism m" "m : X → Y"
shows "(try_cast m) ∘⇩c m = left_coproj X (Y ∖ (X,m))"
by (smt comp_associative2 complement_morphism_type id_left_unit2 into_super_def into_super_type left_coproj_cfunc_coprod left_proj_type m_type try_cast_into_super try_cast_type)
lemma try_cast_m_m':
assumes m_type: "monomorphism m" "m : X → Y"
shows "(try_cast m) ∘⇩c m⇧c = right_coproj X (Y ∖ (X,m))"
by (smt comp_associative2 complement_morphism_type id_left_unit2 into_super_def into_super_type m_type(1) m_type(2) right_coproj_cfunc_coprod right_proj_type try_cast_into_super try_cast_type)
lemma try_cast_mono:
assumes m_type: "monomorphism m" "m : X → Y"
shows "monomorphism(try_cast m)"
by (smt cfunc_type_def comp_monic_imp_monic' id_isomorphism into_super_type iso_imp_epi_and_monic try_cast_def2 assms)
subsection ‹Cases›
definition cases :: "cfunc ⇒ cfunc" where
"cases(f) = ((right_cart_proj 𝟭 (domain f)) ⨝⇩f (right_cart_proj 𝟭 (domain f))) ∘⇩c (dist_prod_coprod_right 𝟭 𝟭 (domain f)) ∘⇩c ⟨case_bool ∘⇩c f, id(domain(f))⟩"
lemma cases_def2:
assumes "f : X → Ω"
shows "cases(f) = ((right_cart_proj 𝟭 X) ⨝⇩f (right_cart_proj 𝟭 X)) ∘⇩c (dist_prod_coprod_right 𝟭 𝟭 X) ∘⇩c ⟨case_bool ∘⇩c f, id X⟩"
unfolding cases_def
using assms cfunc_type_def by auto
lemma cases_type[type_rule]:
assumes "f : X → Ω"
shows "cases(f) : X → X ∐ X"
using assms by(etcs_subst cases_def2,
meson case_bool_def2 cfunc_bowtie_prod_type cfunc_prod_type comp_type
dist_prod_coprod_right_type id_type right_cart_proj_type)
lemma true_case:
assumes x_type[type_rule]: "x ∈⇩c X"
assumes f_type[type_rule]: "f : X → Ω"
assumes true_case: "f ∘⇩c x = 𝗍"
shows "cases f ∘⇩c x = left_coproj X X ∘⇩c x"
proof (etcs_subst cases_def2)
have "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c
dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x
= (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f ∘⇩c x, x⟩"
using cfunc_prod_comp comp_associative2 id_left_unit2 by (etcs_assocr, typecheck_cfuncs, force)
also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨left_coproj 𝟭 𝟭, x⟩"
using true_case case_bool_true by argo
also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c left_coproj (𝟭 ×⇩c X) (𝟭 ×⇩c X) ∘⇩c ⟨id 𝟭 , x⟩"
by (typecheck_cfuncs, metis dist_prod_coprod_right_ap_left id_right_unit2)
also have "... = left_coproj X X ∘⇩c right_cart_proj 𝟭 X ∘⇩c ⟨id 𝟭, x⟩"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_bowtie_prod)
also have "... = left_coproj X X ∘⇩c x"
using right_cart_proj_cfunc_prod by (typecheck_cfuncs, presburger)
finally show "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x = left_coproj X X ∘⇩c x".
qed
lemma false_case:
assumes x_type[type_rule]: "x ∈⇩c X"
assumes f_type[type_rule]: "f : X → Ω"
assumes false_case: "f ∘⇩c x = 𝖿"
shows "cases f ∘⇩c x = right_coproj X X ∘⇩c x"
proof (etcs_subst cases_def2)
have "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c
dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x
= (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f ∘⇩c x, x⟩"
using cfunc_prod_comp comp_associative2 id_left_unit2 by (etcs_assocr, typecheck_cfuncs, force)
also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨right_coproj 𝟭 𝟭, x⟩"
using false_case case_bool_false by argo
also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c right_coproj (𝟭 ×⇩c X) (𝟭 ×⇩c X) ∘⇩c ⟨id 𝟭 , x⟩"
by (typecheck_cfuncs, metis dist_prod_coprod_right_ap_right id_right_unit2)
also have "... = right_coproj X X ∘⇩c right_cart_proj 𝟭 X ∘⇩c ⟨id 𝟭, x⟩"
using comp_associative2 right_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
also have "... = right_coproj X X ∘⇩c x"
using right_cart_proj_cfunc_prod by (typecheck_cfuncs, presburger)
finally show "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x = right_coproj X X ∘⇩c x".
qed
subsection ‹Coproduct Set Properities›
lemma coproduct_commutes:
"A ∐ B ≅ B ∐ A"
proof -
have id_AB: "((right_coproj A B) ⨿ (left_coproj A B)) ∘⇩c ((right_coproj B A) ⨿ (left_coproj B A)) = id(A ∐ B)"
by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp id_coprod left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
have id_BA: " ((right_coproj B A) ⨿ (left_coproj B A)) ∘⇩c ((right_coproj A B) ⨿ (left_coproj A B)) = id(B ∐ A)"
by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp id_coprod right_coproj_cfunc_coprod left_coproj_cfunc_coprod)
show "A ∐ B ≅ B ∐ A"
by (smt (verit, ccfv_threshold) cfunc_coprod_type cfunc_type_def id_AB id_BA is_isomorphic_def isomorphism_def left_proj_type right_proj_type)
qed
lemma coproduct_associates:
"A ∐ (B ∐ C) ≅ (A ∐ B) ∐ C"
proof -
obtain q where q_def: "q = (left_coproj (A ∐ B) C ) ∘⇩c (right_coproj A B)" and q_type[type_rule]: "q: B → (A ∐ B) ∐ C"
by (typecheck_cfuncs, simp)
obtain f where f_def: "f = q ⨿ (right_coproj (A ∐ B) C)" and f_type[type_rule]: "(f: (B ∐ C) → ((A ∐ B) ∐ C))"
by (typecheck_cfuncs, simp)
have f_prop: "(f ∘⇩c left_coproj B C = q) ∧ (f ∘⇩c right_coproj B C = right_coproj (A ∐ B) C)"
by (typecheck_cfuncs, simp add: f_def left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
then have f_unique: "(∃!f. (f: (B ∐ C) → ((A ∐ B) ∐ C)) ∧ (f ∘⇩c left_coproj B C = q) ∧ (f ∘⇩c right_coproj B C = right_coproj (A ∐ B) C))"
by (typecheck_cfuncs, metis cfunc_coprod_unique f_prop f_type)
obtain m where m_def: "m = (left_coproj (A ∐ B) C ) ∘⇩c (left_coproj A B)" and m_type[type_rule]: "m : A → (A ∐ B) ∐ C"
by (typecheck_cfuncs, simp)
obtain g where g_def: "g = m ⨿ f" and g_type[type_rule]: "g: A ∐ (B ∐ C) → (A ∐ B) ∐ C"
by (typecheck_cfuncs, simp)
have g_prop: "(g ∘⇩c (left_coproj A (B ∐ C)) = m) ∧ (g ∘⇩c (right_coproj A (B ∐ C)) = f)"
by (typecheck_cfuncs, simp add: g_def left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
have g_unique: "∃! g. ((g: A ∐ (B ∐ C) → (A ∐ B) ∐ C) ∧ (g ∘⇩c (left_coproj A (B ∐ C)) = m) ∧ (g ∘⇩c (right_coproj A (B ∐ C)) = f))"
by (typecheck_cfuncs, metis cfunc_coprod_unique g_prop g_type)
obtain p where p_def: "p = (right_coproj A (B ∐ C)) ∘⇩c (left_coproj B C)" and p_type[type_rule]: "p: B → A ∐ (B ∐ C)"
by (typecheck_cfuncs, simp)
obtain h where h_def: "h = (left_coproj A (B ∐ C)) ⨿ p" and h_type[type_rule]: "h: (A ∐ B) → A ∐ (B ∐ C)"
by (typecheck_cfuncs, simp)
have h_prop1: "h ∘⇩c (left_coproj A B) = (left_coproj A (B ∐ C))"
by (typecheck_cfuncs, simp add: h_def left_coproj_cfunc_coprod p_type)
have h_prop2: "h ∘⇩c (right_coproj A B) = p"
using h_def left_proj_type right_coproj_cfunc_coprod by (typecheck_cfuncs, blast)
have h_unique: "∃! h. ((h: (A ∐ B) → A ∐ (B ∐ C)) ∧ (h ∘⇩c (left_coproj A B) = (left_coproj A (B ∐ C))) ∧ (h ∘⇩c (right_coproj A B) =p))"
by (typecheck_cfuncs, metis cfunc_coprod_unique h_prop1 h_prop2 h_type)
obtain j where j_def: "j = (right_coproj A (B ∐ C)) ∘⇩c (right_coproj B C)" and j_type[type_rule]: "j : C → A ∐ (B ∐ C)"
by (typecheck_cfuncs, simp)
obtain k where k_def: "k = h ⨿ j" and k_type[type_rule]: "k: (A ∐ B) ∐ C → A ∐ (B ∐ C)"
by (typecheck_cfuncs, simp)
have fact1: "(k ∘⇩c g) ∘⇩c (left_coproj A (B ∐ C)) = (left_coproj A (B ∐ C))"
by (typecheck_cfuncs, smt (z3) comp_associative2 g_prop h_prop1 h_type j_type k_def left_coproj_cfunc_coprod left_proj_type m_def)
have fact2: "(g ∘⇩c k) ∘⇩c (left_coproj (A ∐ B) C) = (left_coproj (A ∐ B) C)"
by (typecheck_cfuncs, smt (verit) cfunc_coprod_comp cfunc_coprod_unique comp_associative2 comp_type f_prop g_prop g_type h_def h_type j_def k_def k_type left_coproj_cfunc_coprod left_proj_type m_def p_def p_type q_def right_proj_type)
have fact3: "(g ∘⇩c k) ∘⇩c (right_coproj (A ∐ B) C) = (right_coproj (A ∐ B) C)"
by (smt comp_associative2 comp_type f_def g_prop g_type h_type j_def k_def k_type q_type right_coproj_cfunc_coprod right_proj_type)
have fact4: "(k ∘⇩c g) ∘⇩c (right_coproj A (B ∐ C)) = (right_coproj A (B ∐ C))"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) cfunc_coprod_unique cfunc_type_def comp_associative comp_type f_prop g_prop h_prop2 h_type j_def k_def left_coproj_cfunc_coprod left_proj_type p_def q_def right_coproj_cfunc_coprod right_proj_type)
have fact5: "(k ∘⇩c g) = id( A ∐ (B ∐ C))"
by (typecheck_cfuncs, metis cfunc_coprod_unique fact1 fact4 id_coprod left_proj_type right_proj_type)
have fact6: "(g ∘⇩c k) = id((A ∐ B) ∐ C)"
by (typecheck_cfuncs, metis cfunc_coprod_unique fact2 fact3 id_coprod left_proj_type right_proj_type)
show ?thesis
by (metis cfunc_type_def fact5 fact6 g_type is_isomorphic_def isomorphism_def k_type)
qed
text ‹The lemma below corresponds to Proposition 2.5.10.›
lemma product_distribute_over_coproduct_left:
"A ×⇩c (X ∐ Y) ≅ (A ×⇩c X) ∐ (A ×⇩c Y)"
using factor_prod_coprod_left_type dist_prod_coprod_iso is_isomorphic_def isomorphic_is_symmetric by blast
lemma prod_pres_iso:
assumes "A ≅ C" "B ≅ D"
shows "A ×⇩c B ≅ C ×⇩c D"
proof -
obtain f where f_def: "f: A → C ∧ isomorphism(f)"
using assms(1) is_isomorphic_def by blast
obtain g where g_def: "g: B → D ∧ isomorphism(g)"
using assms(2) is_isomorphic_def by blast
have "isomorphism(f×⇩fg)"
by (meson cfunc_cross_prod_mono cfunc_cross_prod_surj epi_is_surj epi_mon_is_iso f_def g_def iso_imp_epi_and_monic surjective_is_epimorphism)
then show "A ×⇩c B ≅ C ×⇩c D"
by (meson cfunc_cross_prod_type f_def g_def is_isomorphic_def)
qed
lemma coprod_pres_iso:
assumes "A ≅ C" "B ≅ D"
shows "A ∐ B ≅ C ∐ D"
proof-
obtain f where f_def: "f: A → C" "isomorphism(f)"
using assms(1) is_isomorphic_def by blast
obtain g where g_def: "g: B → D" "isomorphism(g)"
using assms(2) is_isomorphic_def by blast
have surj_f: "surjective(f)"
using epi_is_surj f_def iso_imp_epi_and_monic by blast
have surj_g: "surjective(g)"
using epi_is_surj g_def iso_imp_epi_and_monic by blast
have coproj_f_inject: "injective(((left_coproj C D) ∘⇩c f))"
using cfunc_type_def composition_of_monic_pair_is_monic f_def iso_imp_epi_and_monic left_coproj_are_monomorphisms left_proj_type monomorphism_imp_injective by auto
have coproj_g_inject: "injective(((right_coproj C D) ∘⇩c g))"
using cfunc_type_def composition_of_monic_pair_is_monic g_def iso_imp_epi_and_monic right_coproj_are_monomorphisms right_proj_type monomorphism_imp_injective by auto
obtain φ where φ_def: "φ = (left_coproj C D ∘⇩c f) ⨿ (right_coproj C D ∘⇩c g)"
by simp
then have φ_type: "φ: A ∐ B → C ∐ D"
using cfunc_coprod_type cfunc_type_def codomain_comp domain_comp f_def g_def left_proj_type right_proj_type by auto
have "surjective(φ)"
unfolding surjective_def
proof(clarify)
fix y
assume y_type: "y ∈⇩c codomain φ"
then have y_type2: "y ∈⇩c C ∐ D"
using φ_type cfunc_type_def by auto
then have y_form: "(∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c)
∨ (∃ d. d ∈⇩c D ∧ y = right_coproj C D ∘⇩c d)"
using coprojs_jointly_surj by auto
show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
proof(cases "∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c")
assume "∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
then obtain c where c_def: "c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
by blast
then have "∃ a. a ∈⇩c A ∧ f ∘⇩c a = c"
using cfunc_type_def f_def surj_f surjective_def by auto
then obtain a where a_def: "a ∈⇩c A ∧ f ∘⇩c a = c"
by blast
obtain x where x_def: "x = left_coproj A B ∘⇩c a"
by blast
have x_type: "x ∈⇩c A ∐ B"
using a_def comp_type left_proj_type x_def by blast
have "φ ∘⇩c x = y"
using φ_def φ_type a_def c_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_def by (smt (verit))
then show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
using φ_type cfunc_type_def x_type by auto
next
assume "∄c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
then have y_def2: "∃ d. d ∈⇩c D ∧ y = right_coproj C D ∘⇩c d"
using y_form by blast
then obtain d where d_def: "d ∈⇩c D" "y = right_coproj C D ∘⇩c d"
by blast
then have "∃ b. b ∈⇩c B ∧ g ∘⇩c b = d"
using cfunc_type_def g_def surj_g surjective_def by auto
then obtain b where b_def: "b ∈⇩c B" "g ∘⇩c b = d"
by blast
obtain x where x_def: "x = right_coproj A B ∘⇩c b"
by blast
have x_type: "x ∈⇩c A ∐ B"
using b_def comp_type right_proj_type x_def by blast
have "φ ∘⇩c x = y"
using φ_def φ_type b_def cfunc_type_def comp_associative comp_type d_def f_def g_def left_proj_type right_coproj_cfunc_coprod right_proj_type x_def by (smt (verit))
then show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
using φ_type cfunc_type_def x_type by auto
qed
qed
have "injective(φ)"
unfolding injective_def
proof(clarify)
fix x y
assume x_type: "x ∈⇩c domain φ"
assume y_type: "y ∈⇩c domain φ"
assume equals: "φ ∘⇩c x = φ ∘⇩c y"
have x_type2: "x ∈⇩c A ∐ B"
using φ_type cfunc_type_def x_type by auto
have y_type2: "y ∈⇩c A ∐ B"
using φ_type cfunc_type_def y_type by auto
have phix_type: "φ ∘⇩c x ∈⇩c C ∐ D"
using φ_type comp_type x_type2 by blast
have phiy_type: "φ ∘⇩c y ∈⇩c C ∐ D"
using equals phix_type by auto
have x_form: "(∃ a. a ∈⇩c A ∧ x = left_coproj A B ∘⇩c a)
∨ (∃ b. b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b)"
using cfunc_type_def coprojs_jointly_surj x_type x_type2 y_type by auto
have y_form: "(∃ a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a)
∨ (∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b)"
using cfunc_type_def coprojs_jointly_surj x_type x_type2 y_type by auto
show "x=y"
proof(cases "∃ a. a ∈⇩c A ∧ x = left_coproj A B ∘⇩c a")
assume "∃ a. a ∈⇩c A ∧ x = left_coproj A B ∘⇩c a"
then obtain a where a_def: "a ∈⇩c A" "x = left_coproj A B ∘⇩c a"
by blast
show "x = y"
proof(cases "∃ a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a")
assume "∃ a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
then obtain a' where a'_def: "a' ∈⇩c A" "y = left_coproj A B ∘⇩c a'"
by blast
then have "a = a'"
proof -
have "(left_coproj C D ∘⇩c f) ∘⇩c a = φ ∘⇩c x"
using φ_def a_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_type by (smt (verit))
also have "... = φ ∘⇩c y"
by (meson equals)
also have "... = (φ ∘⇩c left_coproj A B) ∘⇩c a'"
using φ_type a'_def comp_associative2 by (typecheck_cfuncs, blast)
also have "... = (left_coproj C D ∘⇩c f) ∘⇩c a'"
unfolding φ_def using f_def g_def a'_def left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
ultimately show "a = a'"
by (smt a'_def a_def cfunc_type_def coproj_f_inject domain_comp f_def injective_def left_proj_type)
qed
then show "x=y"
by (simp add: a'_def(2) a_def(2))
next
assume "∄a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
then have "∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b"
using y_form by blast
then obtain b' where b'_def: "b' ∈⇩c B" "y = right_coproj A B ∘⇩c b'"
by blast
show "x = y"
proof -
have "left_coproj C D ∘⇩c (f ∘⇩c a) = (left_coproj C D ∘⇩c f) ∘⇩c a"
using a_def cfunc_type_def comp_associative f_def left_proj_type by auto
also have "... = φ ∘⇩c x"
using φ_def a_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_type by (smt (verit))
also have "... = φ ∘⇩c y"
by (meson equals)
also have "... = (φ ∘⇩c right_coproj A B) ∘⇩c b'"
using φ_type b'_def comp_associative2 by (typecheck_cfuncs, blast)
also have "... = (right_coproj C D ∘⇩c g) ∘⇩c b' "
unfolding φ_def using f_def g_def b'_def right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = right_coproj C D ∘⇩c (g ∘⇩c b')"
using g_def b'_def by (typecheck_cfuncs, simp add: comp_associative2)
ultimately show "x = y"
using a_def(1) b'_def(1) comp_type coproducts_disjoint f_def(1) g_def(1) by auto
qed
qed
next
assume "∄a. a ∈⇩c A ∧ x = left_coproj A B ∘⇩c a"
then have "∃ b. b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b"
using x_form by blast
then obtain b where b_def: "b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b"
by blast
show "x = y"
proof(cases "∃ a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a")
assume "∃ a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
then obtain a' where a'_def: "a' ∈⇩c A" "y = left_coproj A B ∘⇩c a'"
by blast
show "x = y"
proof -
have "right_coproj C D ∘⇩c (g ∘⇩c b) = (right_coproj C D ∘⇩c g) ∘⇩c b"
using b_def cfunc_type_def comp_associative g_def right_proj_type by auto
also have "... = φ ∘⇩c x"
by (smt φ_def φ_type b_def comp_associative2 comp_type f_def(1) g_def(1) left_proj_type right_coproj_cfunc_coprod right_proj_type)
also have "... = φ ∘⇩c y"
by (meson equals)
also have "... = (φ ∘⇩c left_coproj A B) ∘⇩c a'"
using φ_type a'_def comp_associative2 by (typecheck_cfuncs, blast)
also have "... = (left_coproj C D ∘⇩c f) ∘⇩c a' "
unfolding φ_def using f_def g_def a'_def left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = left_coproj C D ∘⇩c (f ∘⇩c a')"
using f_def a'_def by (typecheck_cfuncs, simp add: comp_associative2)
ultimately show "x = y"
by (metis a'_def(1) b_def comp_type coproducts_disjoint f_def(1) g_def(1))
qed
next
assume "∄a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
then have "∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b"
using y_form by blast
then obtain b' where b'_def: "b' ∈⇩c B" "y = right_coproj A B ∘⇩c b'"
by blast
then have "b = b'"
proof -
have "(right_coproj C D ∘⇩c g) ∘⇩c b = φ ∘⇩c x"
by (smt φ_def φ_type b_def comp_associative2 comp_type f_def(1) g_def(1) left_proj_type right_coproj_cfunc_coprod right_proj_type)
also have "... = φ ∘⇩c y"
by (meson equals)
also have "... = (φ ∘⇩c right_coproj A B) ∘⇩c b'"
using φ_type b'_def comp_associative2 by (typecheck_cfuncs, blast)
also have "... = (right_coproj C D ∘⇩c g) ∘⇩c b'"
unfolding φ_def using f_def g_def b'_def right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
ultimately show "b = b'"
by (smt b'_def b_def cfunc_type_def coproj_g_inject domain_comp g_def injective_def right_proj_type)
qed
then show "x = y"
by (simp add: b'_def(2) b_def)
qed
qed
qed
have "monomorphism φ"
using ‹injective φ› injective_imp_monomorphism by blast
have "epimorphism φ"
by (simp add: ‹surjective φ› surjective_is_epimorphism)
have "isomorphism φ"
using ‹epimorphism φ› ‹monomorphism φ› epi_mon_is_iso by blast
then show ?thesis
using φ_type is_isomorphic_def by blast
qed
lemma product_distribute_over_coproduct_right:
"(A ∐ B) ×⇩c C ≅ (A ×⇩c C) ∐ (B ×⇩c C)"
by (meson coprod_pres_iso isomorphic_is_transitive product_commutes product_distribute_over_coproduct_left)
lemma coproduct_with_self_iso:
"X ∐ X ≅ X ×⇩c Ω"
proof -
obtain ρ where ρ_def: "ρ = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ⨿ ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩" and ρ_type[type_rule]: "ρ : X ∐ X → X ×⇩c Ω"
by (typecheck_cfuncs, simp)
have ρ_inj: "injective ρ"
unfolding injective_def
proof(clarify)
fix x y
assume "x ∈⇩c domain ρ" then have x_type[type_rule]: "x ∈⇩c X ∐ X"
using ρ_type cfunc_type_def by auto
assume "y ∈⇩c domain ρ" then have y_type[type_rule]: "y ∈⇩c X ∐ X"
using ρ_type cfunc_type_def by auto
assume equals: "ρ ∘⇩c x = ρ ∘⇩c y"
show "x = y"
proof(cases "∃ lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X")
assume "∃lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
then obtain lx where lx_def: "x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
by blast
have ρx: "ρ ∘⇩c x = ⟨lx, 𝗍⟩"
proof -
have "ρ ∘⇩c x = (ρ ∘⇩c left_coproj X X) ∘⇩c lx"
using comp_associative2 lx_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ∘⇩c lx"
unfolding ρ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨lx, 𝗍⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left lx_def)
finally show ?thesis.
qed
show "x = y"
proof(cases "∃ ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X")
assume "∃ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
then obtain ly where ly_def: "y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
by blast
have "ρ ∘⇩c y = ⟨ly, 𝗍⟩"
proof -
have "ρ ∘⇩c y = (ρ ∘⇩c left_coproj X X) ∘⇩c ly"
using comp_associative2 ly_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ∘⇩c ly"
unfolding ρ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨ly, 𝗍⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left ly_def)
finally show ?thesis.
qed
then show "x = y"
using ρx cart_prod_eq2 equals lx_def ly_def true_func_type by auto
next
assume "∄ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
then obtain ry where ry_def: "y = right_coproj X X ∘⇩c ry" and ry_type[type_rule]: "ry ∈⇩c X"
by (meson y_type coprojs_jointly_surj)
have ρy: "ρ ∘⇩c y = ⟨ry, 𝖿⟩"
proof -
have "ρ ∘⇩c y = (ρ ∘⇩c right_coproj X X) ∘⇩c ry"
using comp_associative2 ry_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩ ∘⇩c ry"
unfolding ρ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨ry, 𝖿⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left)
finally show ?thesis.
qed
then show ?thesis
using ρx ρy cart_prod_eq2 equals false_func_type lx_def ry_type true_false_distinct true_func_type by force
qed
next
assume "∄lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
then obtain rx where rx_def: "x = right_coproj X X ∘⇩c rx ∧ rx ∈⇩c X"
by (typecheck_cfuncs, meson coprojs_jointly_surj)
have ρx: "ρ ∘⇩c x = ⟨rx, 𝖿⟩"
proof -
have "ρ ∘⇩c x = (ρ ∘⇩c right_coproj X X) ∘⇩c rx"
using comp_associative2 rx_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩ ∘⇩c rx"
unfolding ρ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨rx, 𝖿⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left rx_def)
finally show ?thesis.
qed
show "x = y"
proof(cases "∃ ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X")
assume "∃ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
then obtain ly where ly_def: "y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
by blast
have "ρ ∘⇩c y = ⟨ly, 𝗍⟩"
proof -
have "ρ ∘⇩c y = (ρ ∘⇩c left_coproj X X) ∘⇩c ly"
using comp_associative2 ly_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ∘⇩c ly"
unfolding ρ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨ly, 𝗍⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left ly_def)
finally show ?thesis.
qed
then show "x = y"
using ρx cart_prod_eq2 equals false_func_type ly_def rx_def true_false_distinct true_func_type by force
next
assume "∄ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
then obtain ry where ry_def: "y = right_coproj X X ∘⇩c ry ∧ ry ∈⇩c X"
using coprojs_jointly_surj by (typecheck_cfuncs, blast)
have ρy: "ρ ∘⇩c y = ⟨ry, 𝖿⟩"
proof -
have "ρ ∘⇩c y = (ρ ∘⇩c right_coproj X X) ∘⇩c ry"
using comp_associative2 ry_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩ ∘⇩c ry"
unfolding ρ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = ⟨ry, 𝖿⟩"
by (typecheck_cfuncs, metis cart_prod_extract_left ry_def)
finally show ?thesis.
qed
show "x = y"
using ρx ρy cart_prod_eq2 equals false_func_type rx_def ry_def by auto
qed
qed
qed
have "surjective ρ"
unfolding surjective_def
proof(clarify)
fix y
assume "y ∈⇩c codomain ρ" then have y_type[type_rule]: "y ∈⇩c X ×⇩c Ω"
using ρ_type cfunc_type_def by fastforce
then obtain x w where y_def: "y = ⟨x,w⟩ ∧ x ∈⇩c X ∧ w ∈⇩c Ω"
using cart_prod_decomp by fastforce
show "∃x. x ∈⇩c domain ρ ∧ ρ ∘⇩c x = y"
proof(cases "w = 𝗍")
assume "w = 𝗍"
obtain z where z_def: "z = left_coproj X X ∘⇩c x"
by simp
have "ρ ∘⇩c z = y"
proof -
have "ρ ∘⇩c z = (ρ ∘⇩c left_coproj X X) ∘⇩c x"
using comp_associative2 y_def z_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ∘⇩c x"
unfolding ρ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = y"
using ‹w = 𝗍› cart_prod_extract_left y_def by auto
finally show ?thesis.
qed
then show ?thesis
by (metis ρ_type cfunc_type_def codomain_comp domain_comp left_proj_type y_def z_def)
next
assume "w ≠ 𝗍" then have "w = 𝖿"
by (typecheck_cfuncs, meson true_false_only_truth_values y_def)
obtain z where z_def: "z = right_coproj X X ∘⇩c x"
by simp
have "ρ ∘⇩c z = y"
proof -
have "ρ ∘⇩c z = (ρ ∘⇩c right_coproj X X) ∘⇩c x"
using comp_associative2 y_def z_def by (typecheck_cfuncs, blast)
also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩ ∘⇩c x"
unfolding ρ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = y"
using ‹w = 𝖿› cart_prod_extract_left y_def by auto
finally show ?thesis.
qed
then show ?thesis
by (metis ρ_type cfunc_type_def codomain_comp domain_comp right_proj_type y_def z_def)
qed
qed
then show ?thesis
by (metis ρ_inj ρ_type epi_mon_is_iso injective_imp_monomorphism is_isomorphic_def surjective_is_epimorphism)
qed
lemma oneUone_iso_Ω:
"Ω ≅ 𝟭 ∐ 𝟭"
using case_bool_def2 case_bool_iso is_isomorphic_def by auto
text ‹The lemma below is dual to Proposition 2.2.2 in Halvorson.›
lemma "card {x. x ∈⇩c Ω ∐ Ω} = 4"
proof -
have f1: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝗍"
by (typecheck_cfuncs, simp add: coproducts_disjoint)
have f2: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (left_coproj Ω Ω) ∘⇩c 𝖿"
by (typecheck_cfuncs, metis cfunc_type_def left_coproj_are_monomorphisms monomorphism_def true_false_distinct)
have f3: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
by (typecheck_cfuncs, simp add: coproducts_disjoint)
have f4: "(right_coproj Ω Ω) ∘⇩c 𝗍 ≠ (left_coproj Ω Ω) ∘⇩c 𝖿"
by (typecheck_cfuncs, metis (no_types) coproducts_disjoint)
have f5: "(right_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
by (typecheck_cfuncs, metis cfunc_type_def monomorphism_def right_coproj_are_monomorphisms true_false_distinct)
have f6: "(left_coproj Ω Ω) ∘⇩c 𝖿 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
by (typecheck_cfuncs, simp add: coproducts_disjoint)
have "{x. x ∈⇩c Ω ∐ Ω} = {(left_coproj Ω Ω) ∘⇩c 𝗍 , (right_coproj Ω Ω) ∘⇩c 𝗍, (left_coproj Ω Ω) ∘⇩c 𝖿, (right_coproj Ω Ω) ∘⇩c 𝖿}"
using coprojs_jointly_surj true_false_only_truth_values
by (typecheck_cfuncs, auto)
then show "card {x. x ∈⇩c Ω ∐ Ω} = 4"
by (simp add: f1 f2 f3 f4 f5 f6)
qed
end