Theory Cardinality
section ‹Cardinality and Finiteness›
theory Cardinality
imports Exponential_Objects
begin
text ‹The definitions below correspond to Definition 2.6.1 in Halvorson.›
definition is_finite :: "cset ⇒ bool" where
"is_finite X ⟷ (∀m. (m : X → X ∧ monomorphism m) ⟶ isomorphism m)"
definition is_infinite :: "cset ⇒ bool" where
"is_infinite X ⟷ (∃ m. m : X → X ∧ monomorphism m ∧ ¬surjective m)"
lemma either_finite_or_infinite:
"is_finite X ∨ is_infinite X"
using epi_mon_is_iso is_finite_def is_infinite_def surjective_is_epimorphism by blast
text ‹The definition below corresponds to Definition 2.6.2 in Halvorson.›
definition is_smaller_than :: "cset ⇒ cset ⇒ bool" (infix "≤⇩c" 50) where
"X ≤⇩c Y ⟷ (∃ m. m : X → Y ∧ monomorphism m)"
text ‹The purpose of the following lemma is simply to unify the two notations used in the book.›
lemma subobject_iff_smaller_than:
"(X ≤⇩c Y) = (∃m. (X,m) ⊆⇩c Y)"
using is_smaller_than_def subobject_of_def2 by auto
lemma set_card_transitive:
assumes "A ≤⇩c B"
assumes "B ≤⇩c C"
shows "A ≤⇩c C"
by (typecheck_cfuncs, metis (full_types) assms cfunc_type_def comp_type composition_of_monic_pair_is_monic is_smaller_than_def)
lemma all_emptysets_are_finite:
assumes "is_empty X"
shows "is_finite X"
by (metis assms epi_mon_is_iso epimorphism_def3 is_finite_def is_empty_def one_separator)
lemma emptyset_is_smallest_set:
"∅ ≤⇩c X"
using empty_subset is_smaller_than_def subobject_of_def2 by auto
lemma truth_set_is_finite:
"is_finite Ω"
unfolding is_finite_def
proof(clarify)
fix m
assume m_type[type_rule]: "m : Ω → Ω"
assume m_mono: "monomorphism m"
have "surjective m"
unfolding surjective_def
proof(clarify)
fix y
assume "y ∈⇩c codomain m"
then have "y ∈⇩c Ω"
using cfunc_type_def m_type by force
then show "∃x. x ∈⇩c domain m ∧ m ∘⇩c x = y"
by (smt (verit, del_insts) cfunc_type_def codomain_comp domain_comp injective_def m_mono m_type monomorphism_imp_injective true_false_only_truth_values)
qed
then show "isomorphism m"
by (simp add: epi_mon_is_iso m_mono surjective_is_epimorphism)
qed
lemma smaller_than_finite_is_finite:
assumes "X ≤⇩c Y" "is_finite Y"
shows "is_finite X"
unfolding is_finite_def
proof(clarify)
fix x
assume x_type: "x : X → X"
assume x_mono: "monomorphism x"
obtain m where m_def: "m: X → Y ∧ monomorphism m"
using assms(1) is_smaller_than_def by blast
obtain φ where φ_def: "φ = into_super m ∘⇩c (x ⨝⇩f id(Y ∖ (X,m))) ∘⇩c try_cast m"
by auto
have φ_type: "φ : Y → Y"
unfolding φ_def
using x_type m_def by (typecheck_cfuncs, blast)
have "injective(x ⨝⇩f id(Y ∖ (X,m)))"
using cfunc_bowtieprod_inj id_isomorphism id_type iso_imp_epi_and_monic monomorphism_imp_injective x_mono x_type by blast
then have mono1: "monomorphism(x ⨝⇩f id(Y ∖ (X,m)))"
using injective_imp_monomorphism by auto
have mono2: "monomorphism(try_cast m)"
using m_def try_cast_mono by blast
have mono3: "monomorphism((x ⨝⇩f id(Y ∖ (X,m))) ∘⇩c try_cast m)"
using cfunc_type_def composition_of_monic_pair_is_monic m_def mono1 mono2 x_type by (typecheck_cfuncs, auto)
then have φ_mono: "monomorphism φ"
unfolding φ_def
using cfunc_type_def composition_of_monic_pair_is_monic
into_super_mono m_def mono3 x_type by (typecheck_cfuncs,auto)
then have "isomorphism φ"
using φ_def φ_type assms(2) is_finite_def by blast
have iso_x_bowtie_id: "isomorphism(x ⨝⇩f id(Y ∖ (X,m)))"
by (typecheck_cfuncs, smt ‹isomorphism φ› φ_def comp_associative2 id_left_unit2 into_super_iso into_super_try_cast into_super_type isomorphism_sandwich m_def try_cast_type x_type)
have "left_coproj X (Y ∖ (X,m)) ∘⇩c x = (x ⨝⇩f id(Y ∖ (X,m))) ∘⇩c left_coproj X (Y ∖ (X,m))"
using x_type
by (typecheck_cfuncs, simp add: left_coproj_cfunc_bowtie_prod)
have "epimorphism(x ⨝⇩f id(Y ∖ (X,m)))"
using iso_imp_epi_and_monic iso_x_bowtie_id by blast
then have "surjective(x ⨝⇩f id(Y ∖ (X,m)))"
using epi_is_surj x_type by (typecheck_cfuncs, blast)
then have "epimorphism x"
using x_type cfunc_bowtieprod_surj_converse id_type surjective_is_epimorphism by blast
then show "isomorphism x"
by (simp add: epi_mon_is_iso x_mono)
qed
lemma larger_than_infinite_is_infinite:
assumes "X ≤⇩c Y" "is_infinite X"
shows "is_infinite Y"
using assms either_finite_or_infinite epi_is_surj is_finite_def is_infinite_def
iso_imp_epi_and_monic smaller_than_finite_is_finite by blast
lemma iso_pres_finite:
assumes "X ≅ Y"
assumes "is_finite X"
shows "is_finite Y"
using assms is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic isomorphic_is_symmetric smaller_than_finite_is_finite by blast
lemma not_finite_and_infinite:
"¬(is_finite X ∧ is_infinite X)"
using epi_is_surj is_finite_def is_infinite_def iso_imp_epi_and_monic by blast
lemma iso_pres_infinite:
assumes "X ≅ Y"
assumes "is_infinite X"
shows "is_infinite Y"
using assms either_finite_or_infinite not_finite_and_infinite iso_pres_finite isomorphic_is_symmetric by blast
lemma size_2_sets:
"(X ≅ Ω) = (∃ x1. ∃ x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2 ∧ (∀x. x ∈⇩c X ⟶ x = x1 ∨ x = x2))"
proof
assume "X ≅ Ω"
then obtain φ where φ_type[type_rule]: "φ : X → Ω" and φ_iso: "isomorphism φ"
using is_isomorphic_def by blast
obtain x1 x2 where x1_type[type_rule]: "x1 ∈⇩c X" and x1_def: "φ ∘⇩c x1 = 𝗍" and
x2_type[type_rule]: "x2 ∈⇩c X" and x2_def: "φ ∘⇩c x2 = 𝖿" and
distinct: "x1 ≠ x2"
by (typecheck_cfuncs, smt (z3) φ_iso cfunc_type_def comp_associative comp_type id_left_unit2 isomorphism_def true_false_distinct)
then show "∃x1 x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2 ∧ (∀x. x ∈⇩c X ⟶ x = x1 ∨ x = x2)"
by (smt (verit, best) φ_iso φ_type cfunc_type_def comp_associative2 comp_type id_left_unit2 isomorphism_def true_false_only_truth_values)
next
assume exactly_two: "∃x1 x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2 ∧ (∀x. x ∈⇩c X ⟶ x = x1 ∨ x = x2)"
then obtain x1 x2 where x1_type[type_rule]: "x1 ∈⇩c X" and x2_type[type_rule]: "x2 ∈⇩c X" and distinct: "x1 ≠ x2"
by force
have iso_type: "((x1 ⨿ x2) ∘⇩c case_bool) : Ω → X"
by typecheck_cfuncs
have surj: "surjective ((x1 ⨿ x2) ∘⇩c case_bool)"
by (typecheck_cfuncs, smt (verit, best) exactly_two cfunc_type_def coprod_case_bool_false
coprod_case_bool_true distinct false_func_type surjective_def true_func_type)
have inj: "injective ((x1 ⨿ x2) ∘⇩c case_bool)"
by (typecheck_cfuncs, smt (verit, ccfv_SIG) distinct case_bool_true_and_false comp_associative2
coprod_case_bool_false injective_def2 left_coproj_cfunc_coprod true_false_only_truth_values)
then have "isomorphism ((x1 ⨿ x2) ∘⇩c case_bool)"
by (meson epi_mon_is_iso injective_imp_monomorphism singletonI surj surjective_is_epimorphism)
then show "X ≅ Ω"
using is_isomorphic_def iso_type isomorphic_is_symmetric by blast
qed
lemma size_2plus_sets:
"(Ω ≤⇩c X) = (∃ x1. ∃ x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2)"
proof standard
show "Ω ≤⇩c X ⟹ ∃x1 x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2"
by (meson comp_type false_func_type is_smaller_than_def monomorphism_def3 true_false_distinct true_func_type)
next
assume "∃x1 x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2"
then obtain x1 x2 where x1_type[type_rule]: "x1 ∈⇩c X" and
x2_type[type_rule]: "x2 ∈⇩c X" and
distinct: "x1 ≠ x2"
by blast
have mono_type: "((x1 ⨿ x2) ∘⇩c case_bool) : Ω → X"
by typecheck_cfuncs
have inj: "injective ((x1 ⨿ x2) ∘⇩c case_bool)"
by (typecheck_cfuncs, smt (verit, ccfv_SIG) distinct case_bool_true_and_false comp_associative2
coprod_case_bool_false injective_def2 left_coproj_cfunc_coprod true_false_only_truth_values)
then show "Ω ≤⇩c X"
using injective_imp_monomorphism is_smaller_than_def mono_type by blast
qed
lemma not_init_not_term:
"(¬(initial_object X) ∧ ¬(terminal_object X)) = (∃ x1. ∃ x2. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x1 ≠ x2)"
by (metis is_empty_def initial_iso_empty iso_empty_initial iso_to1_is_term no_el_iff_iso_empty single_elem_iso_one terminal_object_def)
lemma sets_size_3_plus:
"(¬(initial_object X) ∧ ¬(terminal_object X) ∧ ¬(X ≅ Ω)) = (∃ x1. ∃ x2. ∃ x3. x1 ∈⇩c X ∧ x2 ∈⇩c X ∧ x3 ∈⇩c X ∧ x1 ≠ x2 ∧ x2 ≠ x3 ∧ x1 ≠ x3)"
by (metis not_init_not_term size_2_sets)
text ‹The next two lemmas below correspond to Proposition 2.6.3 in Halvorson.›
lemma smaller_than_coproduct1:
"X ≤⇩c X ∐ Y"
using is_smaller_than_def left_coproj_are_monomorphisms left_proj_type by blast
lemma smaller_than_coproduct2:
"X ≤⇩c Y ∐ X"
using is_smaller_than_def right_coproj_are_monomorphisms right_proj_type by blast
text ‹The next two lemmas below correspond to Proposition 2.6.4 in Halvorson.›
lemma smaller_than_product1:
assumes "nonempty Y"
shows "X ≤⇩c X ×⇩c Y"
unfolding is_smaller_than_def
proof -
obtain y where y_type: "y ∈⇩c Y"
using assms nonempty_def by blast
have map_type: "⟨id(X),y ∘⇩c β⇘X⇙⟩ : X → X ×⇩c Y"
using y_type cfunc_prod_type cfunc_type_def codomain_comp domain_comp id_type terminal_func_type by auto
have mono: "monomorphism(⟨id X, y ∘⇩c β⇘X⇙⟩)"
using map_type
proof (unfold monomorphism_def3, clarify)
fix g h A
assume g_h_types: "g : A → X" "h : A → X"
assume "⟨id⇩c X,y ∘⇩c β⇘X⇙⟩ ∘⇩c g = ⟨id⇩c X,y ∘⇩c β⇘X⇙⟩ ∘⇩c h"
then have "⟨id⇩c X ∘⇩c g, y ∘⇩c β⇘X⇙ ∘⇩c g⟩ = ⟨id⇩c X ∘⇩c h, y ∘⇩c β⇘X⇙ ∘⇩c h⟩"
using y_type g_h_types by (typecheck_cfuncs, smt cfunc_prod_comp comp_associative2 comp_type)
then have "⟨g, y ∘⇩c β⇘A⇙⟩ = ⟨h, y ∘⇩c β⇘A⇙⟩"
using y_type g_h_types id_left_unit2 terminal_func_comp by (typecheck_cfuncs, auto)
then show "g = h"
using g_h_types y_type
by (metis (full_types) comp_type left_cart_proj_cfunc_prod terminal_func_type)
qed
show "∃m. m : X → X ×⇩c Y ∧ monomorphism m"
using mono map_type by auto
qed
lemma smaller_than_product2:
assumes "nonempty Y"
shows "X ≤⇩c Y ×⇩c X"
unfolding is_smaller_than_def
proof -
have "X ≤⇩c X ×⇩c Y"
by (simp add: assms smaller_than_product1)
then obtain m where m_def: "m : X → X ×⇩c Y ∧ monomorphism m"
using is_smaller_than_def by blast
obtain i where "i : (X ×⇩c Y) → (Y ×⇩c X) ∧ isomorphism i"
using is_isomorphic_def product_commutes by blast
then have "i ∘⇩c m : X → (Y ×⇩c X) ∧ monomorphism(i ∘⇩c m)"
using cfunc_type_def comp_type composition_of_monic_pair_is_monic iso_imp_epi_and_monic m_def by auto
then show "∃m. m : X → Y ×⇩c X ∧ monomorphism m"
by blast
qed
lemma coprod_leq_product:
assumes X_not_init: "¬(initial_object(X))"
assumes Y_not_init: "¬(initial_object(Y))"
assumes X_not_term: "¬(terminal_object(X))"
assumes Y_not_term: "¬(terminal_object(Y))"
shows "X ∐ Y ≤⇩c X ×⇩c Y"
proof -
obtain x1 x2 where x1x2_def[type_rule]: "(x1 ∈⇩c X)" "(x2 ∈⇩c X)" "(x1 ≠ x2)"
using is_empty_def X_not_init X_not_term iso_empty_initial iso_to1_is_term no_el_iff_iso_empty single_elem_iso_one by blast
obtain y1 y2 where y1y2_def[type_rule]: "(y1 ∈⇩c Y)" "(y2 ∈⇩c Y)" "(y1 ≠ y2)"
using is_empty_def Y_not_init Y_not_term iso_empty_initial iso_to1_is_term no_el_iff_iso_empty single_elem_iso_one by blast
then have y1_mono[type_rule]: "monomorphism(y1)"
using element_monomorphism by blast
obtain m where m_def: "m = ⟨id(X), y1 ∘⇩c β⇘X⇙⟩ ⨿ ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1)"
by simp
have type1: "⟨id(X), y1 ∘⇩c β⇘X⇙⟩ : X → (X ×⇩c Y)"
by (meson cfunc_prod_type comp_type id_type terminal_func_type y1y2_def)
have trycast_y1_type: "try_cast y1 : Y → 𝟭 ∐ (Y ∖ (𝟭,y1))"
by (meson element_monomorphism try_cast_type y1y2_def)
have y1'_type[type_rule]: "y1⇧c : Y ∖ (𝟭,y1) → Y"
using complement_morphism_type one_terminal_object terminal_el_monomorphism y1y2_def by blast
have type4: "⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩ : Y ∖ (𝟭,y1) → (X ×⇩c Y)"
using cfunc_prod_type comp_type terminal_func_type x1x2_def y1'_type by blast
have type5: "⟨x2, y2⟩ ∈⇩c (X ×⇩c Y)"
by (simp add: cfunc_prod_type x1x2_def y1y2_def)
then have type6: "⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩ :(𝟭 ∐ (Y ∖ (𝟭,y1))) → (X ×⇩c Y)"
using cfunc_coprod_type type4 by blast
then have type7: "((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1) : Y → (X ×⇩c Y)"
using comp_type trycast_y1_type by blast
then have m_type: "m : X ∐ Y → (X ×⇩c Y)"
by (simp add: cfunc_coprod_type m_def type1)
have relative: "⋀y. y ∈⇩c Y ⟹ (y ∈⇘Y⇙ (𝟭, y1)) = (y = y1)"
proof(safe)
fix y
assume y_type: "y ∈⇩c Y"
show "y ∈⇘Y⇙ (𝟭, y1) ⟹ y = y1"
by (metis cfunc_type_def factors_through_def id_right_unit2 id_type one_unique_element relative_member_def2)
next
show "y1 ∈⇩c Y ⟹ y1 ∈⇘Y⇙ (𝟭, y1)"
by (metis cfunc_type_def factors_through_def id_right_unit2 id_type relative_member_def2 y1_mono)
qed
have "injective(m)"
unfolding injective_def
proof(clarify)
fix a b
assume "a ∈⇩c domain m" "b ∈⇩c domain m"
then have a_type[type_rule]: "a ∈⇩c X ∐ Y" and b_type[type_rule]: "b ∈⇩c X ∐ Y"
using m_type unfolding cfunc_type_def by auto
assume eqs: "m ∘⇩c a = m ∘⇩c b"
have m_leftproj_l_equals: "⋀ l. l ∈⇩c X ⟹ m ∘⇩c left_coproj X Y ∘⇩c l = ⟨l, y1⟩"
proof-
fix l
assume l_type: "l ∈⇩c X"
have "m ∘⇩c left_coproj X Y ∘⇩c l = (⟨id(X), y1 ∘⇩c β⇘X⇙⟩ ⨿ ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1)) ∘⇩c left_coproj X Y ∘⇩c l"
by (simp add: m_def)
also have "... = (⟨id(X), y1 ∘⇩c β⇘X⇙⟩ ⨿ ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1) ∘⇩c left_coproj X Y) ∘⇩c l"
using comp_associative2 l_type by (typecheck_cfuncs, blast)
also have "... = ⟨id(X), y1 ∘⇩c β⇘X⇙⟩ ∘⇩c l"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
also have "... = ⟨id(X)∘⇩c l , (y1 ∘⇩c β⇘X⇙) ∘⇩c l⟩"
using l_type cfunc_prod_comp by (typecheck_cfuncs, auto)
also have "... = ⟨l , y1 ∘⇩c β⇘X⇙ ∘⇩c l⟩"
using l_type comp_associative2 id_left_unit2 by (typecheck_cfuncs, auto)
also have "... = ⟨l , y1⟩"
using l_type by (typecheck_cfuncs,metis id_right_unit2 id_type one_unique_element)
finally show "m ∘⇩c left_coproj X Y ∘⇩c l = ⟨l,y1⟩".
qed
have m_rightproj_y1_equals: "m ∘⇩c right_coproj X Y ∘⇩c y1 = ⟨x2, y2⟩"
proof -
have "m ∘⇩c right_coproj X Y ∘⇩c y1 = (m ∘⇩c right_coproj X Y) ∘⇩c y1"
using comp_associative2 m_type by (typecheck_cfuncs, auto)
also have "... = ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1) ∘⇩c y1"
using m_def right_coproj_cfunc_coprod type1 by (typecheck_cfuncs, auto)
also have "... = (⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1 ∘⇩c y1"
using comp_associative2 by (typecheck_cfuncs, auto)
also have "... = (⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c left_coproj 𝟭 (Y ∖ (𝟭,y1))"
using try_cast_m_m y1_mono y1y2_def(1) by auto
also have "... = ⟨x2, y2⟩"
using left_coproj_cfunc_coprod type4 type5 by blast
finally show ?thesis.
qed
have m_rightproj_not_y1_equals: "⋀ r. r ∈⇩c Y ∧ r ≠ y1 ⟹
∃k. k ∈⇩c Y ∖ (𝟭,y1) ∧ try_cast y1 ∘⇩c r = right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k ∧
m ∘⇩c right_coproj X Y ∘⇩c r = ⟨x1, y1⇧c ∘⇩c k⟩"
proof clarify
fix r
assume r_type: "r ∈⇩c Y"
assume r_not_y1: "r ≠ y1"
then obtain k where k_def: "k ∈⇩c Y ∖ (𝟭,y1) ∧ try_cast y1 ∘⇩c r = right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k"
using r_type relative try_cast_not_in_X y1_mono y1y2_def(1) by blast
have m_rightproj_l_equals: "m ∘⇩c right_coproj X Y ∘⇩c r = ⟨x1, y1⇧c ∘⇩c k⟩"
proof -
have "m ∘⇩c right_coproj X Y ∘⇩c r = (m ∘⇩c right_coproj X Y) ∘⇩c r"
using r_type comp_associative2 m_type by (typecheck_cfuncs, auto)
also have "... = ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c try_cast y1) ∘⇩c r"
using m_def right_coproj_cfunc_coprod type1 by (typecheck_cfuncs, auto)
also have "... = (⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c (try_cast y1 ∘⇩c r)"
using r_type comp_associative2 by (typecheck_cfuncs, auto)
also have "... = (⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c (right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k)"
using k_def by auto
also have "... = ((⟨x2, y2⟩ ⨿ ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩) ∘⇩c right_coproj 𝟭 (Y ∖ (𝟭,y1))) ∘⇩c k"
using comp_associative2 k_def by (typecheck_cfuncs, blast)
also have "... = ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙, y1⇧c⟩ ∘⇩c k"
using right_coproj_cfunc_coprod type4 type5 by auto
also have "... = ⟨x1 ∘⇩c β⇘Y ∖ (𝟭,y1)⇙ ∘⇩c k, y1⇧c ∘⇩c k ⟩"
using cfunc_prod_comp comp_associative2 k_def by (typecheck_cfuncs, auto)
also have "... = ⟨x1, y1⇧c ∘⇩c k⟩"
by (metis id_right_unit2 id_type k_def one_unique_element terminal_func_comp terminal_func_type x1x2_def(1))
finally show ?thesis.
qed
then show "∃k. k ∈⇩c Y ∖ (𝟭, y1) ∧
try_cast y1 ∘⇩c r = right_coproj 𝟭 (Y ∖ (𝟭, y1)) ∘⇩c k ∧
m ∘⇩c right_coproj X Y ∘⇩c r = ⟨x1,y1⇧c ∘⇩c k⟩"
using k_def by blast
qed
show "a = b"
proof(cases "∃x. a = left_coproj X Y ∘⇩c x ∧ x ∈⇩c X")
assume "∃x. a = left_coproj X Y ∘⇩c x ∧ x ∈⇩c X"
then obtain x where x_def: "a = left_coproj X Y ∘⇩c x ∧ x ∈⇩c X"
by auto
then have m_proj_a: "m ∘⇩c left_coproj X Y ∘⇩c x = ⟨x, y1⟩"
using m_leftproj_l_equals by (simp add: x_def)
show "a = b"
proof(cases "∃c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X")
assume "∃c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
then obtain c where c_def: "b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
by auto
then have "m ∘⇩c left_coproj X Y ∘⇩c c = ⟨c, y1⟩"
by (simp add: m_leftproj_l_equals)
then show ?thesis
using c_def element_pair_eq eqs m_proj_a x_def y1y2_def(1) by auto
next
assume "∄c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
then obtain c where c_def: "b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y"
using b_type coprojs_jointly_surj by blast
show "a = b"
proof(cases "c = y1")
assume "c = y1"
have m_rightproj_l_equals: "m ∘⇩c right_coproj X Y ∘⇩c c = ⟨x2, y2⟩"
by (simp add: ‹c = y1› m_rightproj_y1_equals)
then show ?thesis
using ‹c = y1› c_def cart_prod_eq2 eqs m_proj_a x1x2_def(2) x_def y1y2_def(2) y1y2_def(3) by auto
next
assume "c ≠ y1"
then obtain k where k_def: "m ∘⇩c right_coproj X Y ∘⇩c c = ⟨x1, y1⇧c ∘⇩c k⟩"
using c_def m_rightproj_not_y1_equals by blast
then have "⟨x, y1⟩ = ⟨x1, y1⇧c ∘⇩c k⟩"
using c_def eqs m_proj_a x_def by auto
then have "(x = x1) ∧ (y1 = y1⇧c ∘⇩c k)"
by (smt ‹c ≠ y1› c_def cfunc_type_def comp_associative comp_type element_pair_eq k_def m_rightproj_not_y1_equals monomorphism_def3 try_cast_m_m' try_cast_mono trycast_y1_type x1x2_def(1) x_def y1'_type y1_mono y1y2_def(1))
then have False
by (smt ‹c ≠ y1› c_def comp_type complement_disjoint element_pair_eq id_right_unit2 id_type k_def m_rightproj_not_y1_equals x_def y1'_type y1_mono y1y2_def(1))
then show ?thesis by auto
qed
qed
next
assume "∄x. a = left_coproj X Y ∘⇩c x ∧ x ∈⇩c X"
then obtain y where y_def: "a = right_coproj X Y ∘⇩c y ∧ y ∈⇩c Y"
using a_type coprojs_jointly_surj by blast
show "a = b"
proof(cases "y = y1")
assume "y = y1"
then have m_rightproj_y_equals: "m ∘⇩c right_coproj X Y ∘⇩c y = ⟨x2, y2⟩"
using m_rightproj_y1_equals by blast
then have "m ∘⇩c a = ⟨x2, y2⟩"
using y_def by blast
show "a = b"
proof(cases "∃c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X")
assume "∃c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
then obtain c where c_def: "b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
by blast
then show "a = b"
using cart_prod_eq2 eqs m_leftproj_l_equals m_rightproj_y_equals x1x2_def(2) y1y2_def y_def by auto
next
assume "∄c. b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
then obtain c where c_def: "b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y"
using b_type coprojs_jointly_surj by blast
show "a = b"
proof(cases "c = y")
assume "c = y"
show "a = b"
by (simp add: ‹c = y› c_def y_def)
next
assume "c ≠ y"
then have "c ≠ y1"
by (simp add: ‹y = y1›)
then obtain k where k_def: "k ∈⇩c Y ∖ (𝟭,y1) ∧ try_cast y1 ∘⇩c c = right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k ∧
m ∘⇩c right_coproj X Y ∘⇩c c = ⟨x1, y1⇧c ∘⇩c k⟩"
using c_def m_rightproj_not_y1_equals by blast
then have "⟨x2, y2⟩ = ⟨x1, y1⇧c ∘⇩c k⟩"
using ‹m ∘⇩c a = ⟨x2,y2⟩› c_def eqs by auto
then have False
using comp_type element_pair_eq k_def x1x2_def y1'_type y1y2_def(2) by auto
then show ?thesis
by simp
qed
qed
next
assume "y ≠ y1"
then obtain k where k_def: "k ∈⇩c Y ∖ (𝟭,y1) ∧ try_cast y1 ∘⇩c y = right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k ∧
m ∘⇩c right_coproj X Y ∘⇩c y = ⟨x1, y1⇧c ∘⇩c k⟩"
using m_rightproj_not_y1_equals y_def by blast
then have "m ∘⇩c a = ⟨x1, y1⇧c ∘⇩c k⟩"
using y_def by blast
show "a = b"
proof(cases "∃c. b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y")
assume "∃c. b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y"
then obtain c where c_def: "b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y"
by blast
show "a = b"
proof(cases "c = y1")
assume "c = y1"
show "a = b"
proof -
obtain cc :: cfunc where
f1: "cc ∈⇩c Y ∖ (𝟭, y1) ∧ try_cast y1 ∘⇩c y = right_coproj 𝟭 (Y ∖ (𝟭, y1)) ∘⇩c cc ∧ m ∘⇩c right_coproj X Y ∘⇩c y = ⟨x1,y1⇧c ∘⇩c cc⟩"
using ‹⋀thesis. (⋀k. k ∈⇩c Y ∖ (𝟭, y1) ∧ try_cast y1 ∘⇩c y = right_coproj 𝟭 (Y ∖ (𝟭, y1)) ∘⇩c k ∧ m ∘⇩c right_coproj X Y ∘⇩c y = ⟨x1,y1⇧c ∘⇩c k⟩ ⟹ thesis) ⟹ thesis› by blast
have "⟨x2,y2⟩ = m ∘⇩c a"
using ‹c = y1› c_def eqs m_rightproj_y1_equals by presburger
then show ?thesis
using f1 cart_prod_eq2 comp_type x1x2_def y1'_type y1y2_def(2) y_def by force
qed
next
assume "c ≠ y1"
then obtain k' where k'_def: "k' ∈⇩c Y ∖ (𝟭,y1) ∧ try_cast y1 ∘⇩c c = right_coproj 𝟭 (Y ∖ (𝟭,y1)) ∘⇩c k' ∧
m ∘⇩c right_coproj X Y ∘⇩c c = ⟨x1, y1⇧c ∘⇩c k'⟩"
using c_def m_rightproj_not_y1_equals by blast
then have "⟨x1, y1⇧c ∘⇩c k'⟩ = ⟨x1, y1⇧c ∘⇩c k⟩"
using c_def eqs k_def y_def by auto
then have "(x1 = x1) ∧ (y1⇧c ∘⇩c k' = y1⇧c ∘⇩c k)"
using element_pair_eq k'_def k_def by (typecheck_cfuncs, blast)
then have "k' = k"
by (metis cfunc_type_def complement_morphism_mono k'_def k_def monomorphism_def y1'_type y1_mono)
then have "c = y"
by (metis c_def cfunc_type_def k'_def k_def monomorphism_def try_cast_mono trycast_y1_type y1_mono y_def)
then show "a = b"
by (simp add: c_def y_def)
qed
next
assume "∄c. b = right_coproj X Y ∘⇩c c ∧ c ∈⇩c Y"
then obtain c where c_def: "b = left_coproj X Y ∘⇩c c ∧ c ∈⇩c X"
using b_type coprojs_jointly_surj by blast
then have "m ∘⇩c left_coproj X Y ∘⇩c c = ⟨c, y1⟩"
by (simp add: m_leftproj_l_equals)
then have "⟨c, y1⟩ = ⟨x1, y1⇧c ∘⇩c k⟩"
using ‹m ∘⇩c a = ⟨x1,y1⇧c ∘⇩c k⟩› ‹m ∘⇩c left_coproj X Y ∘⇩c c = ⟨c,y1⟩› c_def eqs by auto
then have "(c = x1) ∧ (y1 = y1⇧c ∘⇩c k)"
using c_def cart_prod_eq2 comp_type k_def x1x2_def(1) y1'_type y1y2_def(1) by auto
then have False
by (metis cfunc_type_def complement_disjoint id_right_unit id_type k_def y1_mono y1y2_def(1))
then show ?thesis
by simp
qed
qed
qed
qed
then have "monomorphism m"
using injective_imp_monomorphism by auto
then show ?thesis
using is_smaller_than_def m_type by blast
qed
lemma prod_leq_exp:
assumes "¬ terminal_object Y"
shows "X ×⇩c Y ≤⇩c Y⇗X⇖"
proof(cases "initial_object Y")
show "initial_object Y ⟹ X ×⇩c Y ≤⇩c Y⇗X⇖"
by (metis X_prod_empty initial_iso_empty initial_maps_mono initial_object_def is_smaller_than_def iso_empty_initial isomorphic_is_reflexive isomorphic_is_transitive prod_pres_iso)
next
assume "¬ initial_object Y"
then obtain y1 y2 where y1_type[type_rule]: "y1 ∈⇩c Y" and y2_type[type_rule]: "y2 ∈⇩c Y" and y1_not_y2: "y1 ≠ y2"
using assms not_init_not_term by blast
show "X ×⇩c Y ≤⇩c Y⇗X⇖"
proof(cases "X ≅ Ω")
assume "X ≅ Ω"
have "Ω ≤⇩c Y"
using ‹¬ initial_object Y› assms not_init_not_term size_2plus_sets by blast
then obtain m where m_type[type_rule]: "m : Ω → Y" and m_mono: "monomorphism m"
using is_smaller_than_def by blast
then have m_id_type[type_rule]: "m ×⇩f id(Y) : Ω ×⇩c Y → Y ×⇩c Y"
by typecheck_cfuncs
have m_id_mono: "monomorphism (m ×⇩f id(Y))"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_mono id_isomorphism iso_imp_epi_and_monic m_mono)
obtain n where n_type[type_rule]: "n : Y ×⇩c Y → Y⇗Ω⇖" and n_mono: "monomorphism n"
using is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric sets_squared by blast
obtain r where r_type[type_rule]: "r : Y⇗Ω⇖ → Y⇗X⇖" and r_mono: "monomorphism r"
by (meson ‹X ≅ Ω› exp_pres_iso_right is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric)
obtain q where q_type[type_rule]: "q : X ×⇩c Y → Ω ×⇩c Y" and q_mono: "monomorphism q"
by (meson ‹X ≅ Ω› id_isomorphism id_type is_isomorphic_def iso_imp_epi_and_monic prod_pres_iso)
have rnmq_type[type_rule]: "r ∘⇩c n ∘⇩c (m ×⇩f id(Y)) ∘⇩c q : X ×⇩c Y → Y⇗X⇖"
by typecheck_cfuncs
have "monomorphism(r ∘⇩c n ∘⇩c (m ×⇩f id(Y)) ∘⇩c q)"
by (typecheck_cfuncs, simp add: cfunc_type_def composition_of_monic_pair_is_monic m_id_mono n_mono q_mono r_mono)
then show ?thesis
by (meson is_smaller_than_def rnmq_type)
next
assume "¬ X ≅ Ω"
show "X ×⇩c Y ≤⇩c Y⇗X⇖"
proof(cases "initial_object X")
show "initial_object X ⟹ X ×⇩c Y ≤⇩c Y⇗X⇖"
by (metis is_empty_def initial_iso_empty initial_maps_mono initial_object_def
is_smaller_than_def isomorphic_is_transitive no_el_iff_iso_empty
not_init_not_term prod_with_empty_is_empty2 product_commutes terminal_object_def)
next
assume "¬ initial_object X"
show "X ×⇩c Y ≤⇩c Y⇗X⇖"
proof(cases "terminal_object X")
assume "terminal_object X"
then have "X ≅ 𝟭"
by (simp add: one_terminal_object terminal_objects_isomorphic)
have "X ×⇩c Y ≅ Y"
by (simp add: ‹terminal_object X› prod_with_term_obj1)
then have "X ×⇩c Y ≅ Y⇗X⇖"
by (meson ‹X ≅ 𝟭› exp_pres_iso_right exp_set_inj isomorphic_is_symmetric isomorphic_is_transitive exp_one)
then show ?thesis
using is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic by blast
next
assume "¬ terminal_object X"
obtain into where into_def: "into = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c (id Y ×⇩f eq_pred X) "
by simp
then have into_type[type_rule]: "into : Y ×⇩c (X ×⇩c X) → Y"
by (simp, typecheck_cfuncs)
obtain Θ where Θ_def: "Θ = (into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X))⇧♯ ∘⇩c swap X Y"
by auto
have Θ_type[type_rule]: "Θ : X ×⇩c Y → Y⇗X⇖"
unfolding Θ_def by typecheck_cfuncs
have f0: "⋀x. ⋀ y. ⋀ z. x ∈⇩c X ∧ y ∈⇩c Y ∧ z ∈⇩c X ⟹ (Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = into ∘⇩c ⟨y, ⟨x, z⟩⟩"
proof(clarify)
fix x y z
assume x_type[type_rule]: "x ∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c Y"
assume z_type[type_rule]: "z ∈⇩c X"
show "(Θ ∘⇩c ⟨x,y⟩)⇧♭ ∘⇩c ⟨id⇩c X,β⇘X⇙⟩ ∘⇩c z = into ∘⇩c ⟨y,⟨x,z⟩⟩"
proof -
have "(Θ ∘⇩c ⟨x,y⟩)⇧♭ ∘⇩c ⟨id⇩c X,β⇘X⇙⟩ ∘⇩c z = (Θ ∘⇩c ⟨x,y⟩)⇧♭ ∘⇩c ⟨id⇩c X ∘⇩c z,β⇘X⇙ ∘⇩c z⟩"
by (typecheck_cfuncs, simp add: cfunc_prod_comp)
also have "... = (Θ ∘⇩c ⟨x,y⟩)⇧♭ ∘⇩c ⟨z,id 𝟭⟩"
by (typecheck_cfuncs, metis id_left_unit2 one_unique_element)
also have "... = (Θ⇧♭ ∘⇩c (id(X) ×⇩f ⟨x,y⟩)) ∘⇩c ⟨z,id 𝟭⟩"
using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
also have "... = Θ⇧♭ ∘⇩c (id(X) ×⇩f ⟨x,y⟩) ∘⇩c ⟨z,id 𝟭⟩"
using comp_associative2 by (typecheck_cfuncs, auto)
also have "... = Θ⇧♭ ∘⇩c ⟨id(X) ∘⇩c z, ⟨x,y⟩ ∘⇩c id 𝟭⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = Θ⇧♭ ∘⇩c ⟨z,⟨x,y⟩⟩"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
also have "... = ((into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X))⇧♯ ∘⇩c swap X Y)⇧♭ ∘⇩c ⟨z,⟨x,y⟩⟩"
by (simp add: Θ_def)
also have "... = ((into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X))⇧♯⇧♭ ∘⇩c (id X ×⇩f swap X Y)) ∘⇩c ⟨z,⟨x,y⟩⟩"
using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
also have "... = (into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X)) ∘⇩c (id X ×⇩f swap X Y) ∘⇩c ⟨z,⟨x,y⟩⟩"
by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3 transpose_func_def)
also have "... = (into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X)) ∘⇩c ⟨id X ∘⇩c z, swap X Y ∘⇩c ⟨x,y⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X)) ∘⇩c ⟨z, ⟨y,x⟩⟩"
using id_left_unit2 swap_ap by (typecheck_cfuncs, presburger)
also have "... = into ∘⇩c associate_right Y X X ∘⇩c swap X (Y ×⇩c X) ∘⇩c ⟨z, ⟨y,x⟩⟩"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
also have "... = into ∘⇩c associate_right Y X X ∘⇩c ⟨⟨y,x⟩, z⟩"
using swap_ap by (typecheck_cfuncs, presburger)
also have "... = into ∘⇩c ⟨y, ⟨x, z⟩⟩"
using associate_right_ap by (typecheck_cfuncs, presburger)
finally show ?thesis.
qed
qed
have f1: "⋀x y. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ (Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c x = y"
proof -
fix x y
assume x_type[type_rule]: "x ∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c Y"
have "(Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c x = into ∘⇩c ⟨y, ⟨x, x⟩⟩"
by (simp add: f0 x_type y_type)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c (id Y ×⇩f eq_pred X) ∘⇩c ⟨y, ⟨x, x⟩⟩"
using cfunc_type_def comp_associative comp_type into_def by (typecheck_cfuncs, fastforce)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨id Y ∘⇩c y, eq_pred X ∘⇩c ⟨x, x⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨y, 𝗍⟩"
by (typecheck_cfuncs, metis eq_pred_iff_eq id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y, left_coproj 𝟭 𝟭⟩"
by (typecheck_cfuncs, simp add: case_bool_true cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y, left_coproj 𝟭 𝟭 ∘⇩c id 𝟭⟩"
by (typecheck_cfuncs, metis id_right_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c left_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭) ∘⇩c ⟨y,id 𝟭⟩"
using dist_prod_coprod_left_ap_left by (typecheck_cfuncs, auto)
also have "... = ((left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c left_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭)) ∘⇩c ⟨y,id 𝟭⟩"
by (typecheck_cfuncs, meson comp_associative2)
also have "... = left_cart_proj Y 𝟭 ∘⇩c ⟨y,id 𝟭⟩"
using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
also have "... = y"
by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod)
finally show "(Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c x = y".
qed
have f2: "⋀x y z. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ z ∈⇩c X ⟹ z ≠ x ⟹ y ≠ y1 ⟹ (Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y1"
proof -
fix x y z
assume x_type[type_rule]: "x ∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c Y"
assume z_type[type_rule]: "z ∈⇩c X"
assume "z ≠ x"
assume "y ≠ y1"
have "(Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = into ∘⇩c ⟨y, ⟨x, z⟩⟩"
by (simp add: f0 x_type y_type z_type)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c (id Y ×⇩f eq_pred X) ∘⇩c ⟨y, ⟨x, z⟩⟩"
using cfunc_type_def comp_associative comp_type into_def by (typecheck_cfuncs, fastforce)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨id Y ∘⇩c y, eq_pred X ∘⇩c ⟨x, z⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨y, 𝖿⟩"
by (typecheck_cfuncs, metis ‹z ≠ x› eq_pred_iff_eq_conv id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y, right_coproj 𝟭 𝟭⟩"
by (typecheck_cfuncs, simp add: case_bool_false cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y, right_coproj 𝟭 𝟭 ∘⇩c id 𝟭⟩"
by (typecheck_cfuncs, simp add: id_right_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c right_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭) ∘⇩c ⟨y,id 𝟭⟩"
using dist_prod_coprod_left_ap_right by (typecheck_cfuncs, auto)
also have "... = ((left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c right_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭)) ∘⇩c ⟨y,id 𝟭⟩"
by (typecheck_cfuncs, meson comp_associative2)
also have "... = ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)) ∘⇩c ⟨y,id 𝟭⟩"
using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1) ∘⇩c ⟨y,id 𝟭⟩"
using comp_associative2 by (typecheck_cfuncs, force)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c ⟨y,y1⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c 𝖿"
by (typecheck_cfuncs, metis ‹y ≠ y1› eq_pred_iff_eq_conv)
also have "... = y1"
using case_bool_false right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
finally show "(Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y1".
qed
have f3: "⋀x z. x ∈⇩c X ⟹ z ∈⇩c X ⟹ z ≠ x ⟹ (Θ ∘⇩c ⟨x, y1⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y2"
proof -
fix x y z
assume x_type[type_rule]: "x ∈⇩c X"
assume z_type[type_rule]: "z ∈⇩c X"
assume "z ≠ x"
have "(Θ ∘⇩c ⟨x, y1⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = into ∘⇩c ⟨y1, ⟨x, z⟩⟩"
by (simp add: f0 x_type y1_type z_type)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c (id Y ×⇩f eq_pred X) ∘⇩c ⟨y1, ⟨x, z⟩⟩"
using cfunc_type_def comp_associative comp_type into_def by (typecheck_cfuncs, fastforce)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨id Y ∘⇩c y1, eq_pred X ∘⇩c ⟨x, z⟩⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c (id Y ×⇩f case_bool) ∘⇩c ⟨y1, 𝖿⟩"
by (typecheck_cfuncs, metis ‹z ≠ x› eq_pred_iff_eq_conv id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y1, right_coproj 𝟭 𝟭⟩"
by (typecheck_cfuncs, simp add: case_bool_false cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c dist_prod_coprod_left Y 𝟭 𝟭 ∘⇩c ⟨y1, right_coproj 𝟭 𝟭 ∘⇩c id 𝟭⟩"
by (typecheck_cfuncs, simp add: id_right_unit2)
also have "... = (left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c right_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭) ∘⇩c ⟨y1,id 𝟭⟩"
using dist_prod_coprod_left_ap_right by (typecheck_cfuncs, auto)
also have "... = ((left_cart_proj Y 𝟭 ⨿ ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)))
∘⇩c right_coproj (Y ×⇩c 𝟭) (Y ×⇩c 𝟭)) ∘⇩c ⟨y1,id 𝟭⟩"
by (typecheck_cfuncs, meson comp_associative2)
also have "... = ((y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1)) ∘⇩c ⟨y1,id 𝟭⟩"
using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c (id Y ×⇩f y1) ∘⇩c ⟨y1,id 𝟭⟩"
using comp_associative2 by (typecheck_cfuncs, force)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c eq_pred Y ∘⇩c ⟨y1,y1⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (y2 ⨿ y1) ∘⇩c case_bool ∘⇩c 𝗍"
by (typecheck_cfuncs, metis eq_pred_iff_eq)
also have "... = y2"
using case_bool_true left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
finally show "(Θ ∘⇩c ⟨x, y1⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y2".
qed
have Θ_injective: "injective(Θ)"
unfolding injective_def
proof(clarify)
fix xy st
assume xy_type[type_rule]: "xy ∈⇩c domain Θ"
assume st_type[type_rule]: "st ∈⇩c domain Θ"
assume equals: "Θ ∘⇩c xy = Θ ∘⇩c st"
obtain x y where x_type[type_rule]: "x ∈⇩c X" and y_type[type_rule]: "y ∈⇩c Y" and xy_def: "xy = ⟨x,y⟩"
by (metis Θ_type cart_prod_decomp cfunc_type_def xy_type)
obtain s t where s_type[type_rule]: "s ∈⇩c X" and t_type[type_rule]: "t ∈⇩c Y" and st_def: "st = ⟨s,t⟩"
by (metis Θ_type cart_prod_decomp cfunc_type_def st_type)
have equals2: "Θ ∘⇩c ⟨x,y⟩ = Θ ∘⇩c ⟨s,t⟩"
using equals st_def xy_def by auto
have "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "y = y1")
assume "y = y1"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "t = y1")
show "t = y1 ⟹ ⟨x,y⟩ = ⟨s,t⟩"
by (typecheck_cfuncs, metis ‹y = y1› equals f1 f3 st_def xy_def y1_not_y2)
next
assume "t ≠ y1"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "s = x")
show "s = x ⟹ ⟨x,y⟩ = ⟨s,t⟩"
by (typecheck_cfuncs, metis equals2 f1)
next
assume "s ≠ x"
obtain z where z_type[type_rule]: "z ∈⇩c X" and z_not_x: "z ≠ x" and z_not_s: "z ≠ s"
by (metis ‹¬ X ≅ Ω› ‹¬ initial_object X› ‹¬ terminal_object X› sets_size_3_plus)
have t_sz: "(Θ ∘⇩c ⟨s, t⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y1"
by (simp add: ‹t ≠ y1› f2 s_type t_type z_not_s z_type)
have y_xz: "(Θ ∘⇩c ⟨x, y⟩)⇧♭ ∘⇩c ⟨id X, β⇘X⇙⟩ ∘⇩c z = y2"
by (simp add: ‹y = y1› f3 x_type z_not_x z_type)
then have "y1 = y2"
using equals2 t_sz by auto
then have False
using y1_not_y2 by auto
then show "⟨x,y⟩ = ⟨s,t⟩"
by simp
qed
qed
next
assume "y ≠ y1"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "y = y2")
assume "y = y2"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "t = y2", clarify)
show "t = y2 ⟹ ⟨x,y⟩ = ⟨s,y2⟩"
by (typecheck_cfuncs, metis ‹y = y2› ‹y ≠ y1› equals f1 f2 st_def xy_def)
next
assume "t ≠ y2"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "x = s", clarify)
show "x = s ⟹ ⟨s,y⟩ = ⟨s,t⟩"
by (metis equals2 f1 s_type t_type y_type)
next
assume "x ≠ s"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "t = y1",clarify)
show "t = y1 ⟹ ⟨x,y⟩ = ⟨s,y1⟩"
by (metis ‹¬ X ≅ Ω› ‹¬ initial_object X› ‹¬ terminal_object X› ‹y = y2› ‹y ≠ y1› equals f2 f3 s_type sets_size_3_plus st_def x_type xy_def y2_type)
next
assume "t ≠ y1"
show "⟨x,y⟩ = ⟨s,t⟩"
by (typecheck_cfuncs, metis ‹t ≠ y1› ‹y ≠ y1› equals f1 f2 st_def xy_def)
qed
qed
qed
next
assume "y ≠ y2"
show "⟨x,y⟩ = ⟨s,t⟩"
proof(cases "s = x", clarify)
show "s = x ⟹ ⟨x,y⟩ = ⟨x,t⟩"
by (metis equals2 f1 t_type x_type y_type)
show "s ≠ x ⟹ ⟨x,y⟩ = ⟨s,t⟩"
by (metis ‹y ≠ y1› ‹y ≠ y2› equals f1 f2 f3 s_type st_def t_type x_type xy_def y_type)
qed
qed
qed
then show "xy = st"
by (typecheck_cfuncs, simp add: st_def xy_def)
qed
then show ?thesis
using Θ_type injective_imp_monomorphism is_smaller_than_def by blast
qed
qed
qed
qed
lemma Y_nonempty_then_X_le_XtoY:
assumes "nonempty Y"
shows "X ≤⇩c X⇗Y⇖"
proof -
obtain f where f_def: "f = (right_cart_proj Y X)⇧♯"
by blast
then have f_type: "f : X → X⇗Y⇖"
by (simp add: right_cart_proj_type transpose_func_type)
have mono_f: "injective(f)"
unfolding injective_def
proof(clarify)
fix x y
assume x_type: "x ∈⇩c domain f"
assume y_type: "y ∈⇩c domain f"
assume equals: "f ∘⇩c x = f ∘⇩c y"
have x_type2 : "x ∈⇩c X"
using cfunc_type_def f_type x_type by auto
have y_type2 : "y ∈⇩c X"
using cfunc_type_def f_type y_type by auto
have "x ∘⇩c (right_cart_proj Y 𝟭) = (right_cart_proj Y X) ∘⇩c (id(Y) ×⇩f x)"
using right_cart_proj_cfunc_cross_prod x_type2 by (typecheck_cfuncs, auto)
also have "... = ((eval_func X Y) ∘⇩c (id(Y) ×⇩f f)) ∘⇩c (id(Y) ×⇩f x)"
by (typecheck_cfuncs, simp add: f_def transpose_func_def)
also have "... = (eval_func X Y) ∘⇩c ((id(Y) ×⇩f f) ∘⇩c (id(Y) ×⇩f x))"
using comp_associative2 f_type x_type2 by (typecheck_cfuncs, fastforce)
also have "... = (eval_func X Y) ∘⇩c (id(Y) ×⇩f (f ∘⇩c x))"
using f_type identity_distributes_across_composition x_type2 by auto
also have "... = (eval_func X Y) ∘⇩c (id(Y) ×⇩f (f ∘⇩c y))"
by (simp add: equals)
also have "... = (eval_func X Y) ∘⇩c ((id(Y) ×⇩f f) ∘⇩c (id(Y) ×⇩f y))"
using f_type identity_distributes_across_composition y_type2 by auto
also have "... = ((eval_func X Y) ∘⇩c (id(Y) ×⇩f f)) ∘⇩c (id(Y) ×⇩f y)"
using comp_associative2 f_type y_type2 by (typecheck_cfuncs, fastforce)
also have "... = (right_cart_proj Y X) ∘⇩c (id(Y) ×⇩f y)"
by (typecheck_cfuncs, simp add: f_def transpose_func_def)
also have "... = y ∘⇩c (right_cart_proj Y 𝟭)"
using right_cart_proj_cfunc_cross_prod y_type2 by (typecheck_cfuncs, auto)
ultimately show "x = y"
using assms epimorphism_def3 nonempty_left_imp_right_proj_epimorphism right_cart_proj_type x_type2 y_type2 by fastforce
qed
then show "X ≤⇩c X⇗Y⇖"
using f_type injective_imp_monomorphism is_smaller_than_def by blast
qed
lemma non_init_non_ter_sets:
assumes "¬(terminal_object X)"
assumes "¬(initial_object X)"
shows "Ω ≤⇩c X"
proof -
obtain x1 and x2 where x1_type[type_rule]: "x1 ∈⇩c X" and
x2_type[type_rule]: "x2 ∈⇩c X" and
distinct: "x1 ≠ x2"
using is_empty_def assms iso_empty_initial iso_to1_is_term no_el_iff_iso_empty single_elem_iso_one by blast
then have map_type: "(x1 ⨿ x2) ∘⇩c case_bool : Ω → X"
by typecheck_cfuncs
have injective: "injective((x1 ⨿ x2) ∘⇩c case_bool)"
unfolding injective_def
proof(clarify)
fix ω1 ω2
assume "ω1 ∈⇩c domain (x1 ⨿ x2 ∘⇩c case_bool)"
then have ω1_type[type_rule]: "ω1 ∈⇩c Ω"
using cfunc_type_def map_type by auto
assume "ω2 ∈⇩c domain (x1 ⨿ x2 ∘⇩c case_bool)"
then have ω2_type[type_rule]: "ω2 ∈⇩c Ω"
using cfunc_type_def map_type by auto
assume equals: "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω1 = (x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω2"
show "ω1 = ω2"
proof(cases "ω1 = 𝗍", clarify)
assume "ω1 = 𝗍"
show "𝗍 = ω2"
proof(rule ccontr)
assume " 𝗍 ≠ ω2"
then have "𝖿 = ω2"
using ‹𝗍 ≠ ω2› true_false_only_truth_values by (typecheck_cfuncs, blast)
then have RHS: "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω2 = x2"
by (meson coprod_case_bool_false x1_type x2_type)
have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω1 = x1"
using ‹ω1 = 𝗍› coprod_case_bool_true x1_type x2_type by blast
then show False
using RHS distinct equals by force
qed
next
assume "ω1 ≠ 𝗍"
then have "ω1 = 𝖿"
using true_false_only_truth_values by (typecheck_cfuncs, blast)
have "ω2 = 𝖿"
proof(rule ccontr)
assume "ω2 ≠ 𝖿"
then have "ω2 = 𝗍"
using true_false_only_truth_values by (typecheck_cfuncs, blast)
then have RHS: "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω2 = x2"
using ‹ω1 = 𝖿› coprod_case_bool_false equals x1_type x2_type by auto
have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c ω1 = x1"
using ‹ω2 = 𝗍› coprod_case_bool_true equals x1_type x2_type by presburger
then show False
using RHS distinct equals by auto
qed
show "ω1 = ω2"
by (simp add: ‹ω1 = 𝖿› ‹ω2 = 𝖿›)
qed
qed
then have "monomorphism((x1 ⨿ x2) ∘⇩c case_bool)"
using injective_imp_monomorphism by auto
then show "Ω ≤⇩c X"
using is_smaller_than_def map_type by blast
qed
lemma exp_preserves_card1:
assumes "A ≤⇩c B"
assumes "nonempty X"
shows "X⇗A⇖ ≤⇩c X⇗B⇖"
unfolding is_smaller_than_def
proof -
obtain x where x_type[type_rule]: "x ∈⇩c X"
using assms(2) unfolding nonempty_def by auto
obtain m where m_def[type_rule]: "m : A → B" "monomorphism m"
using assms(1) unfolding is_smaller_than_def by auto
show "∃m. m : X⇗A⇖ → X⇗B⇖ ∧ monomorphism m"
proof (intro exI[where x="(((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙))
∘⇩c dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m))
∘⇩c swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c (try_cast m ×⇩f id (X⇗A⇖)))⇧♯"], safe)
show "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯ : X⇗A⇖ → X⇗B⇖"
by typecheck_cfuncs
then show "monomorphism
(((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯)"
proof (unfold monomorphism_def3, clarify)
fix g h Z
assume g_type[type_rule]: "g : Z → X⇗A⇖"
assume h_type[type_rule]: "h : Z → X⇗A⇖"
assume eq: "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯ ∘⇩c g
=
((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯ ∘⇩c h"
show "g = h"
proof (typecheck_cfuncs, rule same_evals_equal[where Z=Z, where A=A, where X=X], clarify)
show "eval_func X A ∘⇩c id⇩c A ×⇩f g = eval_func X A ∘⇩c id⇩c A ×⇩f h"
proof (typecheck_cfuncs, rule one_separator[where X="A ×⇩c Z", where Y="X"], clarify)
fix az
assume az_type[type_rule]: "az ∈⇩c A ×⇩c Z"
obtain a z where az_types[type_rule]: "a ∈⇩c A" "z ∈⇩c Z" and az_def: "az = ⟨a,z⟩"
using cart_prod_decomp az_type by blast
have "(eval_func X B) ∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯ ∘⇩c g)) =
(eval_func X B) ∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯ ∘⇩c h))"
using eq by simp
then have "(eval_func X B)∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯)) ∘⇩c (id B ×⇩f g) =
(eval_func X B)∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯)) ∘⇩c (id B ×⇩f h)"
using identity_distributes_across_composition by (typecheck_cfuncs, auto)
then have "((eval_func X B)∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯))) ∘⇩c (id B ×⇩f g) =
((eval_func X B)∘⇩c (id B ×⇩f (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖))⇧♯))) ∘⇩c (id B ×⇩f h)"
by (typecheck_cfuncs, smt eq inv_transpose_func_def3 inv_transpose_of_composition)
then have "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f g)
= ((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f h)"
using transpose_func_def by (typecheck_cfuncs,auto)
then have "(((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f g)) ∘⇩c ⟨m ∘⇩c a, z⟩
= (((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f h)) ∘⇩c ⟨m ∘⇩c a, z⟩"
by auto
then have "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f g) ∘⇩c ⟨m ∘⇩c a, z⟩
= ((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c (id B ×⇩f h) ∘⇩c ⟨m ∘⇩c a, z⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
then have "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c ⟨m ∘⇩c a, g ∘⇩c z⟩
= ((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c ⟨m ∘⇩c a, h ∘⇩c z⟩"
by (typecheck_cfuncs, smt cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_type)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c (try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c ⟨m ∘⇩c a, g ∘⇩c z⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c (try_cast m ×⇩f id⇩c (X⇗A⇖)) ∘⇩c ⟨m ∘⇩c a, h ∘⇩c z⟩"
by (typecheck_cfuncs_prems, smt comp_associative2)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨try_cast m ∘⇩c m ∘⇩c a, g ∘⇩c z⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨try_cast m ∘⇩c m ∘⇩c a, h ∘⇩c z⟩"
using cfunc_cross_prod_comp_cfunc_prod id_left_unit2 by (typecheck_cfuncs_prems, smt)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨(try_cast m ∘⇩c m) ∘⇩c a, g ∘⇩c z⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨(try_cast m ∘⇩c m) ∘⇩c a, h ∘⇩c z⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨left_coproj A (B ∖ (A,m)) ∘⇩c a, g ∘⇩c z⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c
swap (A ∐ (B ∖ (A, m))) (X⇗A⇖) ∘⇩c ⟨left_coproj A (B ∖ (A,m)) ∘⇩c a, h ∘⇩c z⟩"
using m_def(2) try_cast_m_m by (typecheck_cfuncs, auto)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c ⟨g ∘⇩c z, left_coproj A (B ∖ (A,m)) ∘⇩c a⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
dist_prod_coprod_left (X⇗A⇖) A (B ∖ (A, m)) ∘⇩c ⟨h ∘⇩c z, left_coproj A (B ∖ (A,m)) ∘⇩c a⟩"
using swap_ap by (typecheck_cfuncs, auto)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
left_coproj (X⇗A⇖×⇩cA) (X⇗A⇖×⇩c(B ∖ (A,m))) ∘⇩c ⟨g ∘⇩c z, a⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
left_coproj (X⇗A⇖×⇩cA) (X⇗A⇖×⇩c(B ∖ (A,m))) ∘⇩c ⟨h ∘⇩c z,a⟩"
using dist_prod_coprod_left_ap_left by (typecheck_cfuncs, auto)
then have "((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
left_coproj (X⇗A⇖×⇩cA) (X⇗A⇖×⇩c(B ∖ (A,m)))) ∘⇩c ⟨g ∘⇩c z, a⟩
= ((eval_func X A ∘⇩c swap (X⇗A⇖) A) ⨿ (x ∘⇩c β⇘X⇗A⇖ ×⇩c (B ∖ (A, m))⇙) ∘⇩c
left_coproj (X⇗A⇖×⇩cA) (X⇗A⇖×⇩c(B ∖ (A,m)))) ∘⇩c ⟨h ∘⇩c z,a⟩"
by (typecheck_cfuncs_prems, auto simp add: comp_associative2)
then have "(eval_func X A ∘⇩c swap (X⇗A⇖) A) ∘⇩c ⟨g ∘⇩c z, a⟩
= (eval_func X A ∘⇩c swap (X⇗A⇖) A) ∘⇩c ⟨h ∘⇩c z,a⟩"
by (typecheck_cfuncs_prems, auto simp add: left_coproj_cfunc_coprod)
then have "eval_func X A ∘⇩c swap (X⇗A⇖) A ∘⇩c ⟨g ∘⇩c z, a⟩
= eval_func X A ∘⇩c swap (X⇗A⇖) A ∘⇩c ⟨h ∘⇩c z,a⟩"
by (typecheck_cfuncs_prems, auto simp add: comp_associative2)
then have "eval_func X A ∘⇩c ⟨a, g ∘⇩c z⟩ = eval_func X A ∘⇩c ⟨a, h ∘⇩c z⟩"
by (typecheck_cfuncs_prems, auto simp add: swap_ap)
then have "eval_func X A ∘⇩c (id A ×⇩f g) ∘⇩c ⟨a, z⟩ = eval_func X A ∘⇩c (id A ×⇩f h) ∘⇩c ⟨a, z⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
then show "(eval_func X A ∘⇩c id⇩c A ×⇩f g) ∘⇩c az = (eval_func X A ∘⇩c id⇩c A ×⇩f h) ∘⇩c az"
unfolding az_def by (typecheck_cfuncs_prems, auto simp add: comp_associative2)
qed
qed
qed
qed
qed
lemma exp_preserves_card2:
assumes "A ≤⇩c B"
shows "A⇗X⇖ ≤⇩c B⇗X⇖"
unfolding is_smaller_than_def
proof -
obtain m where m_def[type_rule]: "m : A → B" "monomorphism m"
using assms unfolding is_smaller_than_def by auto
show "∃m. m : A⇗X⇖ → B⇗X⇖ ∧ monomorphism m"
proof (intro exI[where x="(m ∘⇩c eval_func A X)⇧♯"], safe)
show "(m ∘⇩c eval_func A X)⇧♯ : A⇗X⇖ → B⇗X⇖"
by typecheck_cfuncs
then show "monomorphism((m ∘⇩c eval_func A X)⇧♯)"
proof (unfold monomorphism_def3, clarify)
fix g h Z
assume g_type[type_rule]: "g : Z → A⇗X⇖"
assume h_type[type_rule]: "h : Z → A⇗X⇖"
assume eq: "(m ∘⇩c eval_func A X)⇧♯ ∘⇩c g = (m ∘⇩c eval_func A X)⇧♯ ∘⇩c h"
show "g = h"
proof (typecheck_cfuncs, rule same_evals_equal[where Z=Z, where A=X, where X=A], clarify)
have "((eval_func B X) ∘⇩c (id X ×⇩f (m ∘⇩c eval_func A X)⇧♯)) ∘⇩c (id X ×⇩f g) =
((eval_func B X) ∘⇩c (id X ×⇩f (m ∘⇩c eval_func A X)⇧♯)) ∘⇩c (id X ×⇩f h)"
by (typecheck_cfuncs, smt comp_associative2 eq inv_transpose_func_def3 inv_transpose_of_composition)
then have "(m ∘⇩c eval_func A X) ∘⇩c (id X ×⇩f g) = (m ∘⇩c eval_func A X) ∘⇩c (id X ×⇩f h)"
by (smt comp_type eval_func_type m_def(1) transpose_func_def)
then have "m ∘⇩c (eval_func A X ∘⇩c (id X ×⇩f g)) = m ∘⇩c (eval_func A X ∘⇩c (id X ×⇩f h))"
by (typecheck_cfuncs, smt comp_associative2)
then have "eval_func A X ∘⇩c (id X ×⇩f g) = eval_func A X ∘⇩c (id X ×⇩f h)"
using m_def monomorphism_def3 by (typecheck_cfuncs, blast)
then show "(eval_func A X ∘⇩c (id X ×⇩f g)) = (eval_func A X ∘⇩c (id X ×⇩f h))"
by (typecheck_cfuncs, smt comp_associative2)
qed
qed
qed
qed
lemma exp_preserves_card3:
assumes "A ≤⇩c B"
assumes "X ≤⇩c Y"
assumes "nonempty(X)"
shows "X⇗A⇖ ≤⇩c Y⇗B⇖"
proof -
have leq1: "X⇗A⇖ ≤⇩c X⇗B⇖"
by (simp add: assms(1,3) exp_preserves_card1)
have leq2: "X⇗B⇖ ≤⇩c Y⇗B⇖"
by (simp add: assms(2) exp_preserves_card2)
show "X⇗A⇖ ≤⇩c Y⇗B⇖"
using leq1 leq2 set_card_transitive by blast
qed
end