Theory Terminal
section ‹Terminal Objects and Elements›
theory Terminal
imports Cfunc Product
begin
text ‹The axiomatization below corresponds to Axiom 3 (Terminal Object) in Halvorson.›
axiomatization
terminal_func :: "cset ⇒ cfunc" ("β⇘_⇙" 100) and
one_set :: "cset" ("𝟭")
where
terminal_func_type[type_rule]: "β⇘X⇙ : X → 𝟭" and
terminal_func_unique: "h : X → 𝟭 ⟹ h = β⇘X⇙" and
one_separator: "f : X → Y ⟹ g : X → Y ⟹ (⋀ x. x : 𝟭 → X ⟹ f ∘⇩c x = g ∘⇩c x) ⟹ f = g"
lemma one_separator_contrapos:
assumes "f : X → Y" "g : X → Y"
shows "f ≠ g ⟹ ∃ x. x : 𝟭 → X ∧ f ∘⇩c x ≠ g ∘⇩c x"
using assms one_separator by (typecheck_cfuncs, blast)
lemma terminal_func_comp:
"x : X → Y ⟹ β⇘Y⇙ ∘⇩c x = β⇘X⇙"
by (simp add: comp_type terminal_func_type terminal_func_unique)
lemma terminal_func_comp_elem:
"x : 𝟭 → X ⟹ β⇘X⇙ ∘⇩c x = id 𝟭"
by (metis id_type terminal_func_comp terminal_func_unique)
subsection ‹Set Membership and Emptiness›
text ‹The abbreviation below captures Definition 2.1.16 in Halvorson.›
abbreviation member :: "cfunc ⇒ cset ⇒ bool" (infix "∈⇩c" 50) where
"x ∈⇩c X ≡ (x : 𝟭 → X)"
definition nonempty :: "cset ⇒ bool" where
"nonempty X ≡ (∃x. x ∈⇩c X)"
definition is_empty :: "cset ⇒ bool" where
"is_empty X ≡ ¬(∃x. x ∈⇩c X)"
text ‹The lemma below corresponds to Exercise 2.1.18 in Halvorson.›
lemma element_monomorphism:
"x ∈⇩c X ⟹ monomorphism x"
unfolding monomorphism_def
by (metis cfunc_type_def domain_comp terminal_func_unique)
lemma one_unique_element:
"∃! x. x ∈⇩c 𝟭"
using terminal_func_type terminal_func_unique by blast
lemma prod_with_empty_is_empty1:
assumes "is_empty (A)"
shows "is_empty(A ×⇩c B)"
by (meson assms comp_type left_cart_proj_type is_empty_def)
lemma prod_with_empty_is_empty2:
assumes "is_empty (B)"
shows "is_empty (A ×⇩c B)"
using assms cart_prod_decomp is_empty_def by blast
subsection ‹Terminal Objects (sets with one element)›
definition terminal_object :: "cset ⇒ bool" where
"terminal_object X ⟷ (∀ Y. ∃! f. f : Y → X)"
lemma one_terminal_object: "terminal_object(𝟭)"
unfolding terminal_object_def using terminal_func_type terminal_func_unique by blast
text ‹The lemma below is a generalisation of @{thm element_monomorphism}›
lemma terminal_el_monomorphism:
assumes "x : T → X"
assumes "terminal_object T"
shows "monomorphism x"
unfolding monomorphism_def
by (metis assms cfunc_type_def domain_comp terminal_object_def)
text ‹The lemma below corresponds to Exercise 2.1.15 in Halvorson.›
lemma terminal_objects_isomorphic:
assumes "terminal_object X" "terminal_object Y"
shows "X ≅ Y"
unfolding is_isomorphic_def
proof -
obtain f where f_type: "f : X → Y" and f_unique: "∀g. g : X → Y ⟶ f = g"
using assms(2) terminal_object_def by force
obtain g where g_type: "g : Y → X" and g_unique: "∀f. f : Y → X ⟶ g = f"
using assms(1) terminal_object_def by force
have g_f_is_id: "g ∘⇩c f = id X"
using assms(1) comp_type f_type g_type id_type terminal_object_def by blast
have f_g_is_id: "f ∘⇩c g = id Y"
using assms(2) comp_type f_type g_type id_type terminal_object_def by blast
have f_isomorphism: "isomorphism f"
unfolding isomorphism_def
using cfunc_type_def f_type g_type g_f_is_id f_g_is_id
by (intro exI[where x=g], auto)
show "∃f. f : X → Y ∧ isomorphism f"
using f_isomorphism f_type by auto
qed
text ‹The two lemmas below show the converse to Exercise 2.1.15 in Halvorson.›
lemma iso_to1_is_term:
assumes "X ≅ 𝟭"
shows "terminal_object X"
unfolding terminal_object_def
proof
fix Y
obtain x where x_type[type_rule]: "x : 𝟭 → X" and x_unique: "∀ y. y : 𝟭 → X ⟶ x = y"
by (smt assms is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric monomorphism_def2 terminal_func_comp terminal_func_unique)
show "∃!f. f : Y → X"
proof (rule ex1I[where a="x ∘⇩c β⇘Y⇙"], typecheck_cfuncs)
fix xa
assume xa_type: "xa : Y → X"
show "xa = x ∘⇩c β⇘Y⇙"
proof (rule ccontr)
assume "xa ≠ x ∘⇩c β⇘Y⇙"
then obtain y where elems_neq: "xa ∘⇩c y ≠ (x ∘⇩c β⇘Y⇙) ∘⇩c y" and y_type: "y : 𝟭 → Y"
using one_separator_contrapos comp_type terminal_func_type x_type xa_type by blast
then show False
by (smt (z3) comp_type elems_neq terminal_func_type x_unique xa_type y_type)
qed
qed
qed
lemma iso_to_term_is_term:
assumes "X ≅ Y"
assumes "terminal_object Y"
shows "terminal_object X"
by (meson assms iso_to1_is_term isomorphic_is_transitive one_terminal_object terminal_objects_isomorphic)
text ‹The lemma below corresponds to Proposition 2.1.19 in Halvorson.›
lemma single_elem_iso_one:
"(∃! x. x ∈⇩c X) ⟷ X ≅ 𝟭"
proof
assume X_iso_one: "X ≅ 𝟭"
then have "𝟭 ≅ X"
by (simp add: isomorphic_is_symmetric)
then obtain f where f_type: "f : 𝟭 → X" and f_iso: "isomorphism f"
using is_isomorphic_def by blast
show "∃!x. x ∈⇩c X"
proof(safe)
show "∃x. x ∈⇩c X"
by (meson f_type)
next
fix x y
assume x_type[type_rule]: "x ∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c X"
have βx_eq_βy: "β⇘X⇙ ∘⇩c x = β⇘X⇙ ∘⇩c y"
using one_unique_element by (typecheck_cfuncs, blast)
have "isomorphism (β⇘X⇙)"
using X_iso_one is_isomorphic_def terminal_func_unique by blast
then have "monomorphism (β⇘X⇙)"
by (simp add: iso_imp_epi_and_monic)
then show "x= y"
using βx_eq_βy monomorphism_def2 terminal_func_type by (typecheck_cfuncs, blast)
qed
next
assume "∃!x. x ∈⇩c X"
then obtain x where x_type: "x : 𝟭 → X" and x_unique: "∀ y. y : 𝟭 → X ⟶ x = y"
by blast
have "terminal_object X"
unfolding terminal_object_def
proof
fix Y
show "∃!f. f : Y → X"
proof (rule ex1I [where a="x ∘⇩c β⇘Y⇙"])
show "x ∘⇩c β⇘Y⇙ : Y → X"
using comp_type terminal_func_type x_type by blast
next
fix xa
assume xa_type: "xa : Y → X"
show "xa = x ∘⇩c β⇘Y⇙"
proof (rule ccontr)
assume "xa ≠ x ∘⇩c β⇘Y⇙"
then obtain y where elems_neq: "xa ∘⇩c y ≠ (x ∘⇩c β⇘Y⇙) ∘⇩c y" and y_type: "y : 𝟭 → Y"
using one_separator_contrapos[where f=xa, where g="x ∘⇩c β⇘Y⇙", where X=Y, where Y=X]
using comp_type terminal_func_type x_type xa_type by blast
have elem1: "xa ∘⇩c y ∈⇩c X"
using comp_type xa_type y_type by auto
have elem2: "(x ∘⇩c β⇘Y⇙) ∘⇩c y ∈⇩c X"
using comp_type terminal_func_type x_type y_type by blast
show False
using elem1 elem2 elems_neq x_unique by blast
qed
qed
qed
then show "X ≅ 𝟭"
by (simp add: one_terminal_object terminal_objects_isomorphic)
qed
subsection ‹Injectivity›
text ‹The definition below corresponds to Definition 2.1.24 in Halvorson.›
definition injective :: "cfunc ⇒ bool" where
"injective f ⟷ (∀ x y. (x ∈⇩c domain f ∧ y ∈⇩c domain f ∧ f ∘⇩c x = f ∘⇩c y) ⟶ x = y)"
lemma injective_def2:
assumes "f : X → Y"
shows "injective f ⟷ (∀ x y. (x ∈⇩c X ∧ y ∈⇩c X ∧ f ∘⇩c x = f ∘⇩c y) ⟶ x = y)"
using assms cfunc_type_def injective_def by force
text ‹The lemma below corresponds to Exercise 2.1.26 in Halvorson.›
lemma monomorphism_imp_injective:
"monomorphism f ⟹ injective f"
by (simp add: cfunc_type_def injective_def monomorphism_def)
text ‹The lemma below corresponds to Proposition 2.1.27 in Halvorson.›
lemma injective_imp_monomorphism:
"injective f ⟹ monomorphism f"
unfolding monomorphism_def injective_def
proof clarify
fix g h
assume f_inj: "∀x y. x ∈⇩c domain f ∧ y ∈⇩c domain f ∧ f ∘⇩c x = f ∘⇩c y ⟶ x = y"
assume cd_g_eq_d_f: "codomain g = domain f"
assume cd_h_eq_d_f: "codomain h = domain f"
assume fg_eq_fh: "f ∘⇩c g = f ∘⇩c h"
obtain X Y where f_type: "f : X → Y"
using cfunc_type_def by auto
obtain A where g_type: "g : A → X" and h_type: "h : A → X"
by (metis cd_g_eq_d_f cd_h_eq_d_f cfunc_type_def domain_comp f_type fg_eq_fh)
have "∀x. x ∈⇩c A ⟶ g ∘⇩c x = h ∘⇩c x"
proof clarify
fix x
assume x_in_A: "x ∈⇩c A"
have "f ∘⇩c g ∘⇩c x = f ∘⇩c h ∘⇩c x"
using g_type h_type x_in_A f_type comp_associative2 fg_eq_fh by (typecheck_cfuncs, auto)
then show "g ∘⇩c x = h ∘⇩c x"
using cd_h_eq_d_f cfunc_type_def comp_type f_inj g_type h_type x_in_A by presburger
qed
then show "g = h"
using g_type h_type one_separator by auto
qed
lemma cfunc_cross_prod_inj:
assumes type_assms: "f : X → Y" "g : Z → W"
assumes "injective f ∧ injective g"
shows "injective (f ×⇩f g)"
by (typecheck_cfuncs, metis assms cfunc_cross_prod_mono injective_imp_monomorphism monomorphism_imp_injective)
lemma cfunc_cross_prod_mono_converse:
assumes type_assms: "f : X → Y" "g : Z → W"
assumes fg_inject: "injective (f ×⇩f g)"
assumes nonempty: "nonempty X" "nonempty Z"
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 equals: "f ∘⇩c x = f ∘⇩c y"
have fg_type: "f ×⇩f g : X ×⇩c Z → Y ×⇩c W"
using assms by typecheck_cfuncs
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
show "x = y"
proof -
obtain b where b_def: "b ∈⇩c Z"
using nonempty(2) nonempty_def by blast
have xb_type: "⟨x,b⟩ ∈⇩c X ×⇩c Z"
by (simp add: b_def cfunc_prod_type x_type2)
have yb_type: "⟨y,b⟩ ∈⇩c X ×⇩c Z"
by (simp add: b_def cfunc_prod_type y_type2)
have "(f ×⇩f g) ∘⇩c ⟨x,b⟩ = ⟨f ∘⇩c x,g ∘⇩c b⟩"
using b_def cfunc_cross_prod_comp_cfunc_prod type_assms x_type2 by blast
also have "... = ⟨f ∘⇩c y,g ∘⇩c b⟩"
by (simp add: equals)
also have "... = (f ×⇩f g) ∘⇩c ⟨y,b⟩"
using b_def cfunc_cross_prod_comp_cfunc_prod type_assms y_type2 by auto
finally have "⟨x,b⟩ = ⟨y,b⟩"
by (metis cfunc_type_def fg_inject fg_type injective_def xb_type yb_type)
then show "x = y"
using b_def cart_prod_eq2 x_type2 y_type2 by auto
qed
next
fix x y
assume x_type: "x ∈⇩c domain g"
assume y_type: "y ∈⇩c domain g"
assume equals: "g ∘⇩c x = g ∘⇩c y"
have fg_type: "f ×⇩f g : X ×⇩c Z → Y ×⇩c W"
using assms by typecheck_cfuncs
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
show "x = y"
proof -
obtain b where b_def: "b ∈⇩c X"
using nonempty(1) nonempty_def by blast
have xb_type: "⟨b,x⟩ ∈⇩c X ×⇩c Z"
by (simp add: b_def cfunc_prod_type x_type2)
have yb_type: "⟨b,y⟩ ∈⇩c X ×⇩c Z"
by (simp add: b_def cfunc_prod_type y_type2)
have "(f ×⇩f g) ∘⇩c ⟨b,x⟩ = ⟨f ∘⇩c b,g ∘⇩c x⟩"
using b_def cfunc_cross_prod_comp_cfunc_prod type_assms(1) type_assms(2) x_type2 by blast
also have "... = (f ×⇩f g) ∘⇩c ⟨b,y⟩"
using b_def cfunc_cross_prod_comp_cfunc_prod equals type_assms(1) type_assms(2) y_type2 by auto
finally have "⟨b,x⟩ = ⟨b,y⟩"
using fg_inject fg_type injective_def2 xb_type yb_type by blast
then show "x = y"
using b_def cart_prod_eq2 x_type2 y_type2 by blast
qed
qed
text ‹The next lemma shows that unless both domains are nonempty we gain no new information.
That is, it will be the case that $f \times g$ is injective, and we cannot infer from this that $f$ or $g$ are
injective since $f \times g$ will be injective no matter what.›
lemma the_nonempty_assumption_above_is_always_required:
assumes "f : X → Y" "g : Z → W"
assumes "¬(nonempty X) ∨ ¬(nonempty Z)"
shows "injective (f ×⇩f g)"
unfolding injective_def
proof(cases "nonempty(X)", safe)
fix x y
assume nonempty: "nonempty X"
assume x_type: "x ∈⇩c domain (f ×⇩f g)"
assume "y ∈⇩c domain (f ×⇩f g)"
then have "¬(nonempty Z)"
using nonempty assms(3) by blast
have fg_type: "f ×⇩f g : X ×⇩c Z → Y ×⇩c W"
by (typecheck_cfuncs, simp add: assms(1,2))
then have "x ∈⇩c X ×⇩c Z"
using x_type cfunc_type_def by auto
then have "∃z. z∈⇩c Z"
using cart_prod_decomp by blast
then have False
using assms(3) nonempty nonempty_def by blast
then show "x=y"
by auto
next
fix x y
assume X_is_empty: "¬ nonempty X"
assume x_type: "x ∈⇩c domain (f ×⇩f g)"
assume "y ∈⇩c domain(f ×⇩f g)"
have fg_type: "f ×⇩f g : X ×⇩c Z → Y ×⇩c W"
by (typecheck_cfuncs, simp add: assms(1,2))
then have "x ∈⇩c X ×⇩c Z"
using x_type cfunc_type_def by auto
then have "∃z. z∈⇩c X"
using cart_prod_decomp by blast
then have False
using assms(3) X_is_empty nonempty_def by blast
then show "x=y"
by auto
qed
subsection ‹Surjectivity›
text ‹The definition below corresponds to Definition 2.1.28 in Halvorson.›
definition surjective :: "cfunc ⇒ bool" where
"surjective f ⟷ (∀y. y ∈⇩c codomain f ⟶ (∃x. x ∈⇩c domain f ∧ f ∘⇩c x = y))"
lemma surjective_def2:
assumes "f : X → Y"
shows "surjective f ⟷ (∀y. y ∈⇩c Y ⟶ (∃x. x ∈⇩c X ∧ f ∘⇩c x = y))"
using assms unfolding surjective_def cfunc_type_def by auto
text ‹The lemma below corresponds to Exercise 2.1.30 in Halvorson.›
lemma surjective_is_epimorphism:
"surjective f ⟹ epimorphism f"
unfolding surjective_def epimorphism_def
proof (cases "nonempty (codomain f)", safe)
fix g h
assume f_surj: "∀y. y ∈⇩c codomain f ⟶ (∃x. x ∈⇩c domain f ∧ f ∘⇩c x = y)"
assume d_g_eq_cd_f: "domain g = codomain f"
assume d_h_eq_cd_f: "domain h = codomain f"
assume gf_eq_hf: "g ∘⇩c f = h ∘⇩c f"
assume nonempty: "nonempty (codomain f)"
obtain X Y where f_type: "f : X → Y"
using nonempty cfunc_type_def f_surj nonempty_def by auto
obtain A where g_type: "g : Y → A" and h_type: "h : Y → A"
by (metis cfunc_type_def codomain_comp d_g_eq_cd_f d_h_eq_cd_f f_type gf_eq_hf)
show "g = h"
proof (rule ccontr)
assume "g ≠ h"
then obtain y where y_in_X: "y ∈⇩c Y" and gy_neq_hy: "g ∘⇩c y ≠ h ∘⇩c y"
using g_type h_type one_separator by blast
then obtain x where "x ∈⇩c X" and "f ∘⇩c x = y"
using cfunc_type_def f_surj f_type by auto
then have "g ∘⇩c f ≠ h ∘⇩c f"
using comp_associative2 f_type g_type gy_neq_hy h_type by auto
then show False
using gf_eq_hf by auto
qed
next
fix g h
assume empty: "¬ nonempty (codomain f)"
assume "domain g = codomain f" "domain h = codomain f"
then show "g ∘⇩c f = h ∘⇩c f ⟹ g = h"
by (metis empty cfunc_type_def codomain_comp nonempty_def one_separator)
qed
text ‹The lemma below corresponds to Proposition 2.2.10 in Halvorson.›
lemma cfunc_cross_prod_surj:
assumes type_assms: "f : A → C" "g : B → D"
assumes f_surj: "surjective f" and g_surj: "surjective g"
shows "surjective (f ×⇩f g)"
unfolding surjective_def
proof(clarify)
fix y
assume y_type: "y ∈⇩c codomain (f ×⇩f g)"
have fg_type: "f ×⇩f g: A ×⇩c B → C ×⇩c D"
using assms by typecheck_cfuncs
then have "y ∈⇩c C ×⇩c D"
using cfunc_type_def y_type by auto
then have "∃ c d. c ∈⇩c C ∧ d ∈⇩c D ∧ y = ⟨c,d⟩"
using cart_prod_decomp by blast
then obtain c d where y_def: "c ∈⇩c C ∧ d ∈⇩c D ∧ y = ⟨c,d⟩"
by blast
then have "∃ a b. a ∈⇩c A ∧ b ∈⇩c B ∧ f ∘⇩c a = c ∧ g ∘⇩c b = d"
by (metis cfunc_type_def f_surj g_surj surjective_def type_assms)
then obtain a b where ab_def: "a ∈⇩c A ∧ b ∈⇩c B ∧ f ∘⇩c a = c ∧ g ∘⇩c b = d"
by blast
then obtain x where x_def: "x = ⟨a,b⟩"
by auto
have x_type: "x ∈⇩c domain (f ×⇩f g)"
using ab_def cfunc_prod_type cfunc_type_def fg_type x_def by auto
have "(f ×⇩f g) ∘⇩c x = y"
using ab_def cfunc_cross_prod_comp_cfunc_prod type_assms(1) type_assms(2) x_def y_def by blast
then show "∃x. x ∈⇩c domain (f ×⇩f g) ∧ (f ×⇩f g) ∘⇩c x = y"
using x_type by blast
qed
lemma cfunc_cross_prod_surj_converse:
assumes type_assms: "f : A → C" "g : B → D"
assumes nonempty: "nonempty C ∧ nonempty D"
assumes "surjective (f ×⇩f g)"
shows "surjective f ∧ surjective g"
unfolding surjective_def
proof(safe)
fix c
assume c_type[type_rule]: "c ∈⇩c codomain f"
then have c_type2: "c ∈⇩c C"
using cfunc_type_def type_assms(1) by auto
obtain d where d_type[type_rule]: "d ∈⇩c D"
using nonempty nonempty_def by blast
then obtain ab where ab_type[type_rule]: "ab ∈⇩c A ×⇩c B" and ab_def: "(f ×⇩f g) ∘⇩c ab = ⟨c, d⟩"
using assms by (typecheck_cfuncs, metis assms(4) cfunc_type_def surjective_def2)
then obtain a b where a_type[type_rule]: "a ∈⇩c A" and b_type[type_rule]: "b ∈⇩c B" and ab_def2: "ab = ⟨a,b⟩"
using cart_prod_decomp by blast
have "a ∈⇩c domain f ∧ f ∘⇩c a = c"
using ab_def ab_def2 b_type cfunc_cross_prod_comp_cfunc_prod cfunc_type_def
comp_type d_type cart_prod_eq2 type_assms by (typecheck_cfuncs, auto)
then show "∃x. x ∈⇩c domain f ∧ f ∘⇩c x = c"
by blast
next
fix d
assume d_type[type_rule]: "d ∈⇩c codomain g"
then have y_type2: "d ∈⇩c D"
using cfunc_type_def type_assms(2) by auto
obtain c where d_type[type_rule]: "c ∈⇩c C"
using nonempty nonempty_def by blast
then obtain ab where ab_type[type_rule]: "ab ∈⇩c A ×⇩c B" and ab_def: "(f ×⇩f g) ∘⇩c ab = ⟨c, d⟩"
using assms by (typecheck_cfuncs, metis assms(4) cfunc_type_def surjective_def2)
then obtain a b where a_type[type_rule]: "a ∈⇩c A" and b_type[type_rule]: "b ∈⇩c B" and ab_def2: "ab = ⟨a,b⟩"
using cart_prod_decomp by blast
then obtain a b where a_type[type_rule]: "a ∈⇩c A" and b_type[type_rule]: "b ∈⇩c B" and ab_def2: "ab = ⟨a,b⟩"
using cart_prod_decomp by blast
have "b ∈⇩c domain g ∧ g ∘⇩c b = d"
using a_type ab_def ab_def2 cfunc_cross_prod_comp_cfunc_prod cfunc_type_def comp_type d_type cart_prod_eq2 type_assms by(typecheck_cfuncs, force)
then show "∃x. x ∈⇩c domain g ∧ g ∘⇩c x = d"
by blast
qed
subsection ‹Interactions of Cartesian Products with Terminal Objects›
lemma diag_on_elements:
assumes "x ∈⇩c X"
shows "diagonal X ∘⇩c x = ⟨x,x⟩"
using assms cfunc_prod_comp cfunc_type_def diagonal_def id_left_unit id_type by auto
lemma one_cross_one_unique_element:
"∃! x. x ∈⇩c 𝟭 ×⇩c 𝟭"
proof (rule ex1I[where a="diagonal 𝟭"])
show "diagonal 𝟭 ∈⇩c 𝟭 ×⇩c 𝟭"
by (simp add: cfunc_prod_type diagonal_def id_type)
next
fix x
assume x_type: "x ∈⇩c 𝟭 ×⇩c 𝟭"
have left_eq: "left_cart_proj 𝟭 𝟭 ∘⇩c x = id 𝟭"
using x_type one_unique_element by (typecheck_cfuncs, blast)
have right_eq: "right_cart_proj 𝟭 𝟭 ∘⇩c x = id 𝟭"
using x_type one_unique_element by (typecheck_cfuncs, blast)
then show "x = diagonal 𝟭"
unfolding diagonal_def using cfunc_prod_unique id_type left_eq x_type by blast
qed
text ‹The lemma below corresponds to Proposition 2.1.20 in Halvorson.›
lemma X_is_cart_prod1:
"is_cart_prod X (id X) (β⇘X⇙) X 𝟭"
unfolding is_cart_prod_def
proof safe
show "id⇩c X : X → X"
by typecheck_cfuncs
next
show "β⇘X⇙ : X → 𝟭"
by typecheck_cfuncs
next
fix f g Y
assume f_type: "f : Y → X" and g_type: "g : Y → 𝟭"
then show "∃h. h : Y → X ∧
id⇩c X ∘⇩c h = f ∧ β⇘X⇙ ∘⇩c h = g ∧ (∀h2. h2 : Y → X ∧ id⇩c X ∘⇩c h2 = f ∧ β⇘X⇙ ∘⇩c h2 = g ⟶ h2 = h)"
proof (intro exI[where x=f], safe)
show "id X ∘⇩c f = f"
using cfunc_type_def f_type id_left_unit by auto
show "β⇘X⇙ ∘⇩c f = g"
by (metis comp_type f_type g_type terminal_func_type terminal_func_unique)
show "⋀h2. h2 : Y → X ⟹ h2 = id⇩c X ∘⇩c h2"
using cfunc_type_def id_left_unit by auto
qed
qed
lemma X_is_cart_prod2:
"is_cart_prod X (β⇘X⇙) (id X) 𝟭 X"
unfolding is_cart_prod_def
proof safe
show "id⇩c X : X → X"
by typecheck_cfuncs
next
show "β⇘X⇙ : X → 𝟭"
by typecheck_cfuncs
next
fix f g Z
assume f_type: "f : Z → 𝟭" and g_type: "g : Z → X"
then show "∃h. h : Z → X ∧
β⇘X⇙ ∘⇩c h = f ∧ id⇩c X ∘⇩c h = g ∧ (∀h2. h2 : Z → X ∧ β⇘X⇙ ∘⇩c h2 = f ∧ id⇩c X ∘⇩c h2 = g ⟶ h2 = h)"
proof (intro exI[where x=g], safe)
show "id⇩c X ∘⇩c g = g"
using cfunc_type_def g_type id_left_unit by auto
show "β⇘X⇙ ∘⇩c g = f"
by (metis comp_type f_type g_type terminal_func_type terminal_func_unique)
show "⋀h2. h2 : Z → X ⟹ h2 = id⇩c X ∘⇩c h2"
using cfunc_type_def id_left_unit by auto
qed
qed
lemma A_x_one_iso_A:
"X ×⇩c 𝟭 ≅ X"
by (metis X_is_cart_prod1 canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def snd_conv)
lemma one_x_A_iso_A:
"𝟭 ×⇩c X ≅ X"
by (meson A_x_one_iso_A isomorphic_is_transitive product_commutes)
text ‹The following four lemmas provide some concrete examples of the above isomorphisms›
lemma left_cart_proj_one_left_inverse:
"⟨id X,β⇘X⇙⟩ ∘⇩c left_cart_proj X 𝟭 = id (X ×⇩c 𝟭)"
by (typecheck_cfuncs, smt (z3) cfunc_prod_comp cfunc_prod_unique id_left_unit2 id_right_unit2 right_cart_proj_type terminal_func_comp terminal_func_unique)
lemma left_cart_proj_one_right_inverse:
"left_cart_proj X 𝟭 ∘⇩c ⟨id X,β⇘X⇙⟩ = id X"
using left_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)
lemma right_cart_proj_one_left_inverse:
"⟨β⇘X⇙,id X⟩ ∘⇩c right_cart_proj 𝟭 X = id (𝟭 ×⇩c X)"
by (typecheck_cfuncs, smt (z3) cart_prod_decomp cfunc_prod_comp id_left_unit2 id_right_unit2 right_cart_proj_cfunc_prod terminal_func_comp terminal_func_unique)
lemma right_cart_proj_one_right_inverse:
"right_cart_proj 𝟭 X ∘⇩c ⟨β⇘X⇙,id X⟩ = id X"
using right_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)
lemma cfunc_cross_prod_right_terminal_decomp:
assumes "f : X → Y" "x : 𝟭 → Z"
shows "f ×⇩f x = ⟨f, x ∘⇩c β⇘X⇙⟩ ∘⇩c left_cart_proj X 𝟭"
using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_def cfunc_prod_comp cfunc_type_def
comp_associative2 right_cart_proj_type terminal_func_comp terminal_func_unique)
text ‹The lemma below corresponds to Proposition 2.1.21 in Halvorson.›
lemma cart_prod_elem_eq:
assumes "a ∈⇩c X ×⇩c Y" "b ∈⇩c X ×⇩c Y"
shows "a = b ⟷
(left_cart_proj X Y ∘⇩c a = left_cart_proj X Y ∘⇩c b
∧ right_cart_proj X Y ∘⇩c a = right_cart_proj X Y ∘⇩c b)"
by (metis (full_types) assms cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type)
text ‹The lemma below corresponds to Note 2.1.22 in Halvorson.›
lemma element_pair_eq:
assumes "x ∈⇩c X" "x' ∈⇩c X" "y ∈⇩c Y" "y' ∈⇩c Y"
shows "⟨x, y⟩ = ⟨x', y'⟩ ⟷ x = x' ∧ y = y'"
by (metis assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
text ‹The lemma below corresponds to Proposition 2.1.23 in Halvorson.›
lemma nonempty_right_imp_left_proj_epimorphism:
"nonempty Y ⟹ epimorphism (left_cart_proj X Y)"
proof -
assume "nonempty Y"
then obtain y where y_in_Y: "y : 𝟭 → Y"
using nonempty_def by blast
then have id_eq: "(left_cart_proj X Y) ∘⇩c ⟨id X, y ∘⇩c β⇘X⇙⟩ = id X"
using comp_type id_type left_cart_proj_cfunc_prod terminal_func_type by blast
then show "epimorphism (left_cart_proj X Y)"
unfolding epimorphism_def
proof clarify
fix g h
assume domain_g: "domain g = codomain (left_cart_proj X Y)"
assume domain_h: "domain h = codomain (left_cart_proj X Y)"
assume "g ∘⇩c left_cart_proj X Y = h ∘⇩c left_cart_proj X Y"
then have "g ∘⇩c left_cart_proj X Y ∘⇩c ⟨id X, y ∘⇩c β⇘X⇙⟩ = h ∘⇩c left_cart_proj X Y ∘⇩c ⟨id X, y ∘⇩c β⇘X⇙⟩"
using y_in_Y by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative domain_g domain_h)
then show "g = h"
by (metis cfunc_type_def domain_g domain_h id_eq id_right_unit left_cart_proj_type)
qed
qed
text ‹The lemma below is the dual of Proposition 2.1.23 in Halvorson.›
lemma nonempty_left_imp_right_proj_epimorphism:
"nonempty X ⟹ epimorphism (right_cart_proj X Y)"
proof -
assume "nonempty X"
then obtain y where y_in_Y: "y: 𝟭 → X"
using nonempty_def by blast
then have id_eq: "(right_cart_proj X Y) ∘⇩c ⟨y ∘⇩c β⇘Y⇙, id Y⟩ = id Y"
using comp_type id_type right_cart_proj_cfunc_prod terminal_func_type by blast
then show "epimorphism (right_cart_proj X Y)"
unfolding epimorphism_def
proof clarify
fix g h
assume domain_g: "domain g = codomain (right_cart_proj X Y)"
assume domain_h: "domain h = codomain (right_cart_proj X Y)"
assume "g ∘⇩c right_cart_proj X Y = h ∘⇩c right_cart_proj X Y"
then have "g ∘⇩c right_cart_proj X Y ∘⇩c ⟨y ∘⇩c β⇘Y⇙, id Y⟩ = h ∘⇩c right_cart_proj X Y ∘⇩c ⟨y ∘⇩c β⇘Y⇙, id Y⟩"
using y_in_Y by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative domain_g domain_h)
then show "g = h"
by (metis cfunc_type_def domain_g domain_h id_eq id_right_unit right_cart_proj_type)
qed
qed
lemma :
assumes "f : 𝟭 → X" "g : 𝟭 → Y"
shows "⟨f, g⟩ = ⟨id X, g ∘⇩c β⇘X⇙⟩ ∘⇩c f"
proof -
have "⟨f, g⟩ = ⟨id X ∘⇩c f, g ∘⇩c β⇘X⇙ ∘⇩c f⟩"
using assms by (typecheck_cfuncs, metis id_left_unit2 id_right_unit2 id_type one_unique_element)
also have "... = ⟨id X, g ∘⇩c β⇘X⇙⟩ ∘⇩c f"
using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
finally show ?thesis.
qed
lemma :
assumes "f : 𝟭 → X" "g : 𝟭 → Y"
shows "⟨f, g⟩ = ⟨f ∘⇩c β⇘Y⇙, id Y⟩ ∘⇩c g"
proof -
have "⟨f, g⟩ = ⟨f ∘⇩c β⇘Y⇙ ∘⇩c g, id Y ∘⇩c g⟩"
using assms by (typecheck_cfuncs, metis id_left_unit2 id_right_unit2 id_type one_unique_element)
also have "... = ⟨f ∘⇩c β⇘Y⇙, id Y⟩ ∘⇩c g"
using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
finally show ?thesis.
qed
subsubsection ‹Cartesian Products as Pullbacks›
text ‹The definition below corresponds to a definition stated between Definition 2.1.42 and Definition 2.1.43 in Halvorson.›
definition is_pullback :: "cset ⇒ cset ⇒ cset ⇒ cset ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ bool" where
"is_pullback A B C D ab bd ac cd ⟷
(ab : A → B ∧ bd : B → D ∧ ac : A → C ∧ cd : C → D ∧ bd ∘⇩c ab = cd ∘⇩c ac ∧
(∀ Z k h. (k : Z → B ∧ h : Z → C ∧ bd ∘⇩c k = cd ∘⇩c h) ⟶
(∃! j. j : Z → A ∧ ab ∘⇩c j = k ∧ ac ∘⇩c j = h)))"
lemma pullback_unique:
assumes "ab : A → B" "bd : B → D" "ac : A → C" "cd : C → D"
assumes "k : Z → B" "h : Z → C"
assumes "is_pullback A B C D ab bd ac cd"
shows "bd ∘⇩c k = cd ∘⇩c h ⟹ (∃! j. j : Z → A ∧ ab ∘⇩c j = k ∧ ac ∘⇩c j = h)"
using assms unfolding is_pullback_def by simp
lemma pullback_iff_product:
assumes "terminal_object(T)"
assumes f_type[type_rule]: "f : Y → T"
assumes g_type[type_rule]: "g : X → T"
shows "(is_pullback P Y X T (pY) f (pX) g) = (is_cart_prod P pX pY X Y)"
proof(safe)
assume pullback: "is_pullback P Y X T pY f pX g"
have f_type[type_rule]: "f : Y → T"
using is_pullback_def pullback by force
have g_type[type_rule]: "g : X → T"
using is_pullback_def pullback by force
show "is_cart_prod P pX pY X Y"
unfolding is_cart_prod_def
proof(safe)
show pX_type[type_rule]: "pX : P → X"
using pullback is_pullback_def by force
show pY_type[type_rule]: "pY : P → Y"
using pullback is_pullback_def by force
show "⋀x y Z.
x : Z → X ⟹
y : Z → Y ⟹
∃h. h : Z → P ∧
pX ∘⇩c h = x ∧ pY ∘⇩c h = y ∧ (∀h2. h2 : Z → P ∧ pX ∘⇩c h2 = x ∧ pY ∘⇩c h2 = y ⟶ h2 = h)"
proof -
fix x y Z
assume x_type[type_rule]: "x : Z → X"
assume y_type[type_rule]: "y : Z → Y"
have "⋀Z k h. k : Z → Y ⟹ h : Z → X ⟹ f ∘⇩c k = g ∘⇩c h ⟹ ∃j. j : Z → P ∧ pY ∘⇩c j = k ∧ pX ∘⇩c j = h"
using is_pullback_def pullback by blast
then have "∃h. h : Z → P ∧
pX ∘⇩c h = x ∧ pY ∘⇩c h = y"
by (smt (verit, ccfv_threshold) assms cfunc_type_def codomain_comp domain_comp f_type g_type terminal_object_def x_type y_type)
then show "∃h. h : Z → P ∧
pX ∘⇩c h = x ∧ pY ∘⇩c h = y ∧ (∀h2. h2 : Z → P ∧ pX ∘⇩c h2 = x ∧ pY ∘⇩c h2 = y ⟶ h2 = h)"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) comp_associative2 is_pullback_def pullback)
qed
qed
next
assume prod: "is_cart_prod P pX pY X Y"
then show "is_pullback P Y X T pY f pX g"
unfolding is_cart_prod_def is_pullback_def
proof(typecheck_cfuncs, safe)
assume pX_type[type_rule]: "pX : P → X"
assume pY_type[type_rule]: "pY : P → Y"
show "f ∘⇩c pY = g ∘⇩c pX"
using assms(1) terminal_object_def by (typecheck_cfuncs, auto)
show "⋀Z k h. k : Z → Y ⟹ h : Z → X ⟹ f ∘⇩c k = g ∘⇩c h ⟹ ∃j. j : Z → P ∧ pY ∘⇩c j = k ∧ pX ∘⇩c j = h"
using is_cart_prod_def prod by blast
show "⋀Z j y.
pY ∘⇩c j : Z → Y ⟹
pX ∘⇩c j : Z → X ⟹
f ∘⇩c pY ∘⇩c j = g ∘⇩c pX ∘⇩c j ⟹ j : Z → P ⟹ y : Z → P ⟹ pY ∘⇩c y = pY ∘⇩c j ⟹ pX ∘⇩c y = pX ∘⇩c j ⟹ j = y"
using is_cart_prod_def prod by blast
qed
qed
end