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 cart_prod_extract_left:
  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 cart_prod_extract_right:
  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