Theory Truth

section β€ΉTruth Values and Characteristic Functionsβ€Ί

theory Truth
  imports Equalizer
begin

text β€ΉThe axiomatization below corresponds to Axiom 5 (Truth-Value Object) in Halvorson.β€Ί
axiomatization
  true_func :: "cfunc" ("𝗍") and
  false_func  :: "cfunc" ("𝖿") and
  truth_value_set :: "cset" ("Ξ©")
where
  true_func_type[type_rule]: "𝗍 ∈c Ξ©" and
  false_func_type[type_rule]: "𝖿 ∈c Ξ©" and
  true_false_distinct: "𝗍 β‰  𝖿" and
  true_false_only_truth_values: "x ∈c Ξ© ⟹ x = 𝖿 ∨ x = 𝗍" and
  characteristic_function_exists:
    "m : B β†’ X ⟹ monomorphism m ⟹ βˆƒ! Ο‡. is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m Ο‡"

definition characteristic_func :: "cfunc β‡’ cfunc" where
  "characteristic_func m =
    (THE Ο‡. monomorphism m ⟢ is_pullback (domain m) 𝟭 (codomain m) Ξ© (Ξ²β‡˜domain m⇙) 𝗍 m Ο‡)"

lemma characteristic_func_is_pullback:
  assumes "m : B β†’ X" "monomorphism m"
  shows "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m (characteristic_func m)"
proof -
  obtain Ο‡ where chi_is_pullback: "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m Ο‡"
    using assms characteristic_function_exists by blast

  have "monomorphism m ⟢ is_pullback (domain m) 𝟭 (codomain m) Ξ© (Ξ²β‡˜domain m⇙) 𝗍 m (characteristic_func m)"
    unfolding characteristic_func_def
  proof (rule theI', rule ex1I[where a= Ο‡], clarify)
    show "is_pullback (domain m) 𝟭 (codomain m) Ξ© (Ξ²β‡˜domain m⇙) 𝗍 m Ο‡"
      using assms(1) cfunc_type_def chi_is_pullback by auto
    show "β‹€x. monomorphism m ⟢ is_pullback (domain m) 𝟭 (codomain m) Ξ© (Ξ²β‡˜domain m⇙) 𝗍 m x ⟹ x = Ο‡"
      using assms cfunc_type_def characteristic_function_exists chi_is_pullback by fastforce
  qed
  then show "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m (characteristic_func m)"
    using assms cfunc_type_def by auto
qed

lemma characteristic_func_type[type_rule]:
  assumes "m : B β†’ X" "monomorphism m"
  shows "characteristic_func m : X β†’ Ξ©"
proof -
  have "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m (characteristic_func m)"
    using assms by (rule characteristic_func_is_pullback)
  then show "characteristic_func m : X β†’ Ξ©"
    unfolding is_pullback_def by auto
qed

lemma characteristic_func_eq:
  assumes "m : B β†’ X" "monomorphism m"
  shows "characteristic_func m ∘c m = 𝗍 ∘c Ξ²β‡˜B⇙"
  using assms characteristic_func_is_pullback unfolding is_pullback_def by auto

lemma monomorphism_equalizes_char_func:
  assumes m_type[type_rule]: "m : B β†’ X" and m_mono[type_rule]: "monomorphism m"
  shows "equalizer B m (characteristic_func m) (𝗍 ∘c Ξ²β‡˜X⇙)"
  unfolding equalizer_def
proof (rule exI[where x=X], rule exI[where x=Ξ©], safe)
  show "characteristic_func m : X β†’ Ξ©"
    by typecheck_cfuncs
  show "𝗍 ∘c Ξ²β‡˜X⇙ : X β†’ Ξ©"
    by typecheck_cfuncs
  show "m : B β†’ X"
    by typecheck_cfuncs
  have comm: "𝗍 ∘c Ξ²β‡˜B⇙ = characteristic_func m ∘c m"
    using characteristic_func_eq m_mono m_type by auto
  then have "Ξ²β‡˜B⇙ = Ξ²β‡˜X⇙ ∘c m"
    using m_type terminal_func_comp by auto
  then show "characteristic_func m ∘c m = (𝗍 ∘c Ξ²β‡˜X⇙) ∘c m"
    using comm comp_associative2 by (typecheck_cfuncs, auto)
next
  show "β‹€h F. h : F β†’ X ⟹ characteristic_func m ∘c h = (𝗍 ∘c Ξ²β‡˜X⇙) ∘c h ⟹ βˆƒk. k : F β†’ B ∧ m ∘c k = h"
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) cfunc_type_def characteristic_func_is_pullback comp_associative comp_type is_pullback_def m_mono)
next
  show "β‹€F k y.  characteristic_func m ∘c m ∘c k = (𝗍 ∘c Ξ²β‡˜X⇙) ∘c m ∘c k ⟹ k : F β†’ B ⟹ y : F β†’ B ⟹ m ∘c y = m ∘c k ⟹ k = y"
      by (typecheck_cfuncs, smt m_mono monomorphism_def2)
qed

lemma characteristic_func_true_relative_member:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes characteristic_func_true: "characteristic_func m ∘c x = 𝗍"
  shows "x βˆˆβ‡˜X⇙ (B,m)"
  unfolding relative_member_def2 factors_through_def
proof (insert assms, clarify)
  have "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m (characteristic_func m)"
    by (simp add: assms characteristic_func_is_pullback)
  then have "βˆƒj. j : 𝟭 β†’ B ∧ Ξ²β‡˜B⇙ ∘c j = id 𝟭 ∧ m ∘c j = x"
    unfolding is_pullback_def using assms by (metis id_right_unit2 id_type true_func_type)
  then show "βˆƒj. j : domain x β†’ domain m ∧ m ∘c j = x"
    using assms(1,3) cfunc_type_def by auto
qed

lemma characteristic_func_false_not_relative_member:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes characteristic_func_true: "characteristic_func m ∘c x = 𝖿"
  shows "Β¬ (x βˆˆβ‡˜X⇙ (B,m))"
  unfolding relative_member_def2 factors_through_def
proof (insert assms, clarify)
  fix h
  assume x_def: "x = m ∘c h"
  assume "h : domain (m ∘c h) β†’ domain m"
  then have h_type: "h ∈c B"
    using assms(1,3) cfunc_type_def x_def by auto

  have "is_pullback B 𝟭 X Ξ© (Ξ²β‡˜B⇙) 𝗍 m (characteristic_func m)"
    by (simp add: assms characteristic_func_is_pullback)
  then have char_m_true: "characteristic_func m ∘c m = 𝗍 ∘c Ξ²β‡˜B⇙"
    unfolding is_pullback_def by auto

  then have "characteristic_func m ∘c m ∘c h = 𝖿"
    using x_def characteristic_func_true by auto
  then have "(characteristic_func m ∘c m) ∘c h = 𝖿"
    using assms h_type by (typecheck_cfuncs, simp add: comp_associative2)
  then have "(𝗍 ∘c Ξ²β‡˜B⇙) ∘c h = 𝖿"    
    using char_m_true by auto
  then have "𝗍 = 𝖿"
    by (metis cfunc_type_def comp_associative h_type id_right_unit2 id_type one_unique_element
        terminal_func_comp terminal_func_type true_func_type)
  then show False
    using true_false_distinct by auto
qed

lemma rel_mem_char_func_true:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes "x βˆˆβ‡˜X⇙ (B,m)"
  shows "characteristic_func m ∘c x = 𝗍"
  by (meson assms(4) characteristic_func_false_not_relative_member characteristic_func_type comp_type relative_member_def2 true_false_only_truth_values)

lemma not_rel_mem_char_func_false:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes "Β¬ (x βˆˆβ‡˜X⇙ (B,m))"
  shows "characteristic_func m ∘c x = 𝖿"
  by (meson assms characteristic_func_true_relative_member characteristic_func_type comp_type true_false_only_truth_values)

text β€ΉThe lemma below corresponds to Proposition 2.2.2 in Halvorson.β€Ί
lemma "card {x. x ∈c Ξ© Γ—c Ξ©} = 4"
proof -
  have "{x. x ∈c Ξ© Γ—c Ξ©} = {βŸ¨π—,π—βŸ©, βŸ¨π—,π–ΏβŸ©, βŸ¨π–Ώ,π—βŸ©, βŸ¨π–Ώ,π–ΏβŸ©}"
    by (auto simp add: cfunc_prod_type true_func_type false_func_type,
        smt cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type true_false_only_truth_values)
  then show "card {x. x ∈c Ξ© Γ—c Ξ©} = 4"
    using element_pair_eq false_func_type true_false_distinct true_func_type by auto
qed

subsection β€ΉEquality Predicateβ€Ί

definition eq_pred :: "cset β‡’ cfunc" where
  "eq_pred X = (THE Ο‡. is_pullback X 𝟭 (X Γ—c X) Ξ© (Ξ²β‡˜X⇙) 𝗍 (diagonal X) Ο‡)"

lemma eq_pred_pullback: "is_pullback X 𝟭 (X Γ—c X) Ξ© (Ξ²β‡˜X⇙) 𝗍 (diagonal X) (eq_pred X)"
  unfolding eq_pred_def
  by (rule the1I2, simp_all add: characteristic_function_exists diag_mono diagonal_type)

lemma eq_pred_type[type_rule]:
  "eq_pred X : X Γ—c X β†’ Ξ©"
  using eq_pred_pullback unfolding is_pullback_def  by auto

lemma eq_pred_square: "eq_pred X ∘c diagonal X = 𝗍 ∘c Ξ²β‡˜X⇙"
  using eq_pred_pullback unfolding is_pullback_def  by auto

lemma eq_pred_iff_eq:
  assumes "x : 𝟭 β†’ X" "y : 𝟭 β†’ X"
  shows "(x = y) = (eq_pred X ∘c ⟨x, y⟩ = 𝗍)"
proof safe
  assume x_eq_y: "x = y"

  have "(eq_pred X ∘c ⟨idc X,idc X⟩) ∘c y = (𝗍 ∘c Ξ²β‡˜X⇙) ∘c y"
    using eq_pred_square unfolding diagonal_def by auto
  then have "eq_pred X ∘c ⟨y, y⟩ = (𝗍 ∘c Ξ²β‡˜X⇙) ∘c y"
    using assms diagonal_type id_type
    by (typecheck_cfuncs, smt cfunc_prod_comp comp_associative2 diagonal_def id_left_unit2)
  then show "eq_pred X ∘c ⟨y, y⟩ = 𝗍"
    using assms id_type
    by (typecheck_cfuncs, smt comp_associative2 terminal_func_comp terminal_func_type terminal_func_unique id_right_unit2)
next
  assume "eq_pred X ∘c ⟨x,y⟩ = 𝗍"
  then have "eq_pred X ∘c ⟨x,y⟩ = 𝗍 ∘c id 𝟭"
    using id_right_unit2 true_func_type by auto
  then obtain j  where j_type: "j : 𝟭 β†’ X" and "diagonal X ∘c j = ⟨x,y⟩"
    using eq_pred_pullback assms unfolding is_pullback_def by (metis cfunc_prod_type id_type)
  then have "⟨j,j⟩ = ⟨x,y⟩"
    using diag_on_elements by auto
  then show "x = y"
    using assms element_pair_eq j_type by auto
qed

lemma eq_pred_iff_eq_conv:
  assumes "x : 𝟭 β†’ X" "y : 𝟭 β†’ X"
  shows "(x β‰  y) = (eq_pred X ∘c ⟨x, y⟩ = 𝖿)"
proof(safe)
  assume "x β‰  y"
  then show "eq_pred X ∘c ⟨x,y⟩ = 𝖿"
    using assms eq_pred_iff_eq true_false_only_truth_values by (typecheck_cfuncs, blast)
next
  show "eq_pred X ∘c ⟨y,y⟩ = 𝖿 ⟹ x = y ⟹ False"
    by (metis assms(1) eq_pred_iff_eq true_false_distinct)
qed

lemma eq_pred_iff_eq_conv2:
  assumes "x : 𝟭 β†’ X" "y : 𝟭 β†’ X"
  shows "(x β‰  y) = (eq_pred X ∘c ⟨x, y⟩ β‰  𝗍)"
  using assms eq_pred_iff_eq by presburger

lemma eq_pred_of_monomorphism:
  assumes m_type[type_rule]: "m : X β†’ Y" and m_mono: "monomorphism m"
  shows "eq_pred Y ∘c (m Γ—f m) = eq_pred X"
proof (rule one_separator[where X="X Γ—c X", where Y=Ξ©])
  show "eq_pred Y ∘c m Γ—f m : X Γ—c X β†’ Ξ©"
    by typecheck_cfuncs
  show "eq_pred X : X Γ—c X β†’ Ξ©"
    by typecheck_cfuncs
next
  fix x
  assume "x ∈c X Γ—c X"
  then obtain x1 x2 where x_def: "x = ⟨x1, x2⟩" and x1_type[type_rule]: "x1 ∈c X" and x2_type[type_rule]: "x2 ∈c X"
    using cart_prod_decomp by blast
  show "(eq_pred Y ∘c m Γ—f m) ∘c x = eq_pred X ∘c x"
    unfolding x_def
  proof (cases "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ = 𝗍")
    assume LHS: "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ = 𝗍"
    then have "eq_pred Y ∘c (m Γ—f m) ∘c ⟨x1,x2⟩ = 𝗍"
      by (typecheck_cfuncs, simp add: comp_associative2)
    then have "eq_pred Y ∘c ⟨m ∘c x1, m ∘c x2⟩ = 𝗍"
      by (typecheck_cfuncs, auto simp add: cfunc_cross_prod_comp_cfunc_prod)
    then have "m ∘c x1 = m ∘c x2"
      by (typecheck_cfuncs_prems, simp add: eq_pred_iff_eq)
    then have "x1 = x2"
      using m_mono m_type monomorphism_def3 x1_type x2_type by blast
    then have RHS: "eq_pred X ∘c ⟨x1,x2⟩ = 𝗍"
      by (typecheck_cfuncs, insert eq_pred_iff_eq, blast)
    show "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ = eq_pred X ∘c ⟨x1,x2⟩"
      using LHS RHS by auto
  next
    assume "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ β‰  𝗍"
    then have LHS: "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ = 𝖿"
      by (typecheck_cfuncs, meson true_false_only_truth_values)
    then have "eq_pred Y ∘c (m Γ—f m) ∘c ⟨x1,x2⟩ = 𝖿"
      by (typecheck_cfuncs, simp add: comp_associative2)
    then have "eq_pred Y ∘c ⟨m ∘c x1, m ∘c x2⟩ = 𝖿"
      by (typecheck_cfuncs, auto simp add: cfunc_cross_prod_comp_cfunc_prod)
    then have "m ∘c x1 β‰  m ∘c x2"
      using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)
    then have "x1 β‰  x2"
      by auto
    then have RHS: "eq_pred X ∘c ⟨x1,x2⟩ = 𝖿"
      using eq_pred_iff_eq_conv by (typecheck_cfuncs, blast)
    show "(eq_pred Y ∘c m Γ—f m) ∘c ⟨x1,x2⟩ = eq_pred X ∘c ⟨x1,x2⟩"
      using LHS RHS by auto
  qed
qed

lemma eq_pred_true_extract_right: 
    assumes "x ∈c X" 
    shows  "eq_pred X ∘c ⟨x ∘c Ξ²β‡˜X⇙, id X⟩ ∘c x = 𝗍"
    using assms cart_prod_extract_right eq_pred_iff_eq by fastforce

lemma eq_pred_false_extract_right: 
    assumes "x ∈c X"  "y ∈c X" "x β‰  y"
    shows  "eq_pred X ∘c ⟨x ∘c Ξ²β‡˜X⇙, id X⟩ ∘c y = 𝖿"
    using assms cart_prod_extract_right eq_pred_iff_eq true_false_only_truth_values  by (typecheck_cfuncs, fastforce)

subsection β€ΉProperties of Monomorphisms and Epimorphismsβ€Ί

text β€ΉThe lemma below corresponds to Exercise 2.2.3 in Halvorson.β€Ί
lemma regmono_is_mono: "regular_monomorphism m ⟹ monomorphism m"
  using equalizer_is_monomorphism regular_monomorphism_def by blast

text β€ΉThe lemma below corresponds to Proposition 2.2.4 in Halvorson.β€Ί
lemma mono_is_regmono:
  shows "monomorphism m ⟹ regular_monomorphism m"
  unfolding regular_monomorphism_def
  by (rule exI[where x="characteristic_func m"], 
      rule exI[where x="𝗍 ∘c Ξ²β‡˜codomain(m)⇙"], 
      typecheck_cfuncs, auto simp add: cfunc_type_def monomorphism_equalizes_char_func)

text β€ΉThe lemma below corresponds to Proposition 2.2.5 in Halvorson.β€Ί
lemma epi_mon_is_iso:
  assumes "epimorphism f" "monomorphism f"
  shows "isomorphism f"
  using assms epi_regmon_is_iso mono_is_regmono by auto

text β€ΉThe lemma below corresponds to Proposition 2.2.8 in Halvorson.β€Ί
lemma epi_is_surj:
  assumes "p: X β†’ Y" "epimorphism p"
  shows "surjective p"
  unfolding surjective_def
proof(rule ccontr)
  assume a1: "Β¬ (βˆ€y. y ∈c codomain p ⟢ (βˆƒx. x ∈c domain p ∧ p ∘c x = y))"
  have "βˆƒy. y ∈c Y ∧ Β¬(βˆƒx. x ∈c X ∧ p ∘c x = y)"
    using a1 assms(1) cfunc_type_def by auto
  then obtain y0 where y_def: "y0 ∈c Y ∧ (βˆ€x. x ∈c X ⟢ p ∘c x β‰  y0)"
    by auto
  have mono: "monomorphism y0"
    using element_monomorphism y_def by blast
  obtain g where g_def: "g = eq_pred Y ∘c ⟨y0 ∘c Ξ²β‡˜Y⇙, id Y⟩"
    by simp
  have g_right_arg_type: "⟨y0 ∘c Ξ²β‡˜Y⇙, id Y⟩ : Y β†’ Y Γ—c Y"
    by (meson cfunc_prod_type comp_type id_type terminal_func_type y_def)
  then have g_type[type_rule]: "g: Y β†’ Ξ©"
    using comp_type eq_pred_type g_def by blast

  have gpx_Eqs_f: "βˆ€x. x ∈c X ⟢ g ∘c p ∘c x = 𝖿"
  proof(rule ccontr)
    assume "Β¬ (βˆ€x. x ∈c X ⟢ g ∘c p ∘c x = 𝖿)"
    then obtain x where x_type: "x ∈c X" and bwoc: "g ∘c p ∘c x β‰  𝖿"
      by blast
    (* have contradiction: "βˆƒs. s ∈c p-1{y0}" *)
    show False
      by (smt (verit) assms(1) bwoc cfunc_type_def comp_associative comp_type eq_pred_false_extract_right eq_pred_type g_def g_right_arg_type x_type y_def)
  qed
  obtain h where h_def: "h = 𝖿 ∘c Ξ²β‡˜Y⇙" and h_type[type_rule]:"h: Y β†’ Ξ©"
    by (typecheck_cfuncs, simp)
  have hpx_eqs_f: "βˆ€x. x ∈c X ⟢ h ∘c p ∘c x = 𝖿"
    by (smt assms(1) cfunc_type_def codomain_comp comp_associative false_func_type h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
  have gp_eqs_hp: "g ∘c p = h ∘c p"
  proof(rule one_separator[where X=X,where Y=Ξ©])
    show "g ∘c p : X β†’ Ξ©"
      using assms by typecheck_cfuncs
    show "h ∘c p : X β†’ Ξ©"
      using assms by typecheck_cfuncs
    show "β‹€x. x ∈c X ⟹ (g ∘c p) ∘c x = (h ∘c p) ∘c x"
      using assms(1) comp_associative2 g_type gpx_Eqs_f h_type hpx_eqs_f by auto
  qed
  have g_not_h: "g β‰  h"
  proof -
   have f1: "βˆ€c. Ξ²β‡˜codomain c⇙ ∘c c = Ξ²β‡˜domain c⇙"
    by (simp add: cfunc_type_def terminal_func_comp)
   have f2: "domain ⟨y0 ∘c Ξ²β‡˜Y⇙,idc Y⟩ = Y"
    using cfunc_type_def g_right_arg_type by blast
  have f3: "codomain ⟨y0 ∘c Ξ²β‡˜Y⇙,idc Y⟩ = Y Γ—c Y"
    using cfunc_type_def g_right_arg_type by blast
  have f4: "codomain y0 = Y"
    using cfunc_type_def y_def by presburger
  have "βˆ€c. domain (eq_pred c) = c Γ—c c"
    using cfunc_type_def eq_pred_type by auto
  then have "g ∘c y0 β‰  𝖿"
    using f4 f3 f2 by (metis (no_types) eq_pred_true_extract_right comp_associative g_def true_false_distinct y_def)
  then show ?thesis
    using f1 by (metis (no_types) cfunc_type_def comp_associative false_func_type h_def id_right_unit2 id_type one_unique_element terminal_func_type y_def)
qed
  then show False
    using gp_eqs_hp assms cfunc_type_def epimorphism_def g_type h_type by auto
qed

text β€ΉThe lemma below corresponds to Proposition 2.2.9 in Halvorson.β€Ί
lemma pullback_of_epi_is_epi1:
assumes "f: Y β†’ Z" "epimorphism f" "is_pullback A Y X Z q1 f q0 g"
shows "epimorphism q0" 
proof - 
  have surj_f: "surjective f"
    using assms(1,2) epi_is_surj by auto
  have "surjective (q0)"
    unfolding surjective_def
  proof(clarify)
    fix y
    assume y_type: "y ∈c codomain q0"
    then have codomain_gy: "g ∘c y ∈c Z"
      using assms(3) cfunc_type_def is_pullback_def  by (typecheck_cfuncs, auto)
    then have z_exists: "βˆƒ z. z ∈c Y ∧ f ∘c z = g ∘c y"
      using assms(1) cfunc_type_def surj_f surjective_def by auto
    then obtain z where z_def: "z ∈c Y ∧ f ∘c z = g ∘c y"
      by blast
    then have "βˆƒ! k. k: 𝟭 β†’ A ∧ q0 ∘c k = y ∧ q1 ∘c k =z"
      by (smt (verit, ccfv_threshold) assms(3) cfunc_type_def is_pullback_def y_type)
    then show "βˆƒx. x ∈c domain q0 ∧ q0 ∘c x = y"
      using assms(3) cfunc_type_def is_pullback_def  by auto
  qed 
  then show ?thesis
    using surjective_is_epimorphism by blast
qed

text β€ΉThe lemma below corresponds to Proposition 2.2.9b in Halvorson.β€Ί
lemma pullback_of_epi_is_epi2:
assumes "g: X β†’ Z" "epimorphism g" "is_pullback A Y X Z q1 f q0 g"
shows "epimorphism q1" 
proof - 
  have surj_g: "surjective g"
    using assms(1) assms(2) epi_is_surj by auto
  have "surjective q1"
    unfolding surjective_def
  proof(clarify)
    fix y
    assume y_type: "y ∈c codomain q1"
    then have codomain_gy: "f ∘c y ∈c Z"
      using assms(3) cfunc_type_def comp_type is_pullback_def  by auto
    then have z_exists: "βˆƒ z. z ∈c X ∧ g ∘c z = f ∘c y"
      using assms(1) cfunc_type_def surj_g surjective_def by auto
    then obtain z where z_def: "z ∈c X ∧ g ∘c z = f ∘c y"
      by blast
    then have "βˆƒ! k. k: 𝟭 β†’ A ∧ q0 ∘c k = z ∧ q1 ∘c k =y"
      by (smt (verit, ccfv_threshold) assms(3) cfunc_type_def is_pullback_def  y_type)      
    then show "βˆƒx. x ∈c domain q1 ∧ q1 ∘c x = y"
      using assms(3) cfunc_type_def is_pullback_def  by auto
  qed
  then show ?thesis
    using surjective_is_epimorphism by blast
qed

text β€ΉThe lemma below corresponds to Proposition 2.2.9c in Halvorson.β€Ί
lemma pullback_of_mono_is_mono1:
assumes "g: X β†’ Z" "monomorphism f" "is_pullback A Y X Z q1 f q0 g"
shows "monomorphism q0" 
  unfolding monomorphism_def2
proof(clarify)
  fix u v Q a x
  assume u_type: "u : Q β†’ a"  
  assume v_type: "v : Q β†’ a"
  assume q0_type: "q0 :  a β†’ x"    
  assume equals: "q0 ∘c u = q0 ∘c v" 

  have a_is_A: "a = A"
    using assms(3) cfunc_type_def is_pullback_def q0_type  by force
  have x_is_X: "x = X"
    using assms(3) cfunc_type_def is_pullback_def q0_type  by fastforce
  have u_type2[type_rule]: "u : Q β†’ A"
    using a_is_A u_type by blast
  have v_type2[type_rule]: "v : Q β†’ A"
    using a_is_A v_type by blast
  have q1_type2[type_rule]: "q0 : A β†’ X"
    using a_is_A q0_type x_is_X by blast

  have eqn1: "g ∘c (q0 ∘c u) = f ∘c (q1 ∘c v)"
  proof - 
    have "g ∘c (q0 ∘c u) = g ∘c q0 ∘c v"
      by (simp add: equals)
    also have "... = f ∘c (q1 ∘c v)"
      using assms(3) cfunc_type_def comp_associative is_pullback_def by (typecheck_cfuncs, force)
    finally show ?thesis.
  qed 

  have eqn2: "q1 ∘c u =  q1  ∘c v"
  proof - 
    have f1: "f ∘c q1 ∘c u = g ∘c q0 ∘c u"
      using assms(3) comp_associative2 is_pullback_def  by (typecheck_cfuncs, auto)
    also have "... = g ∘c q0 ∘c v"
      by (simp add: equals)
    also have "... = f ∘c q1 ∘c v"
      using eqn1 equals by fastforce
    then show ?thesis
      by (typecheck_cfuncs, smt (verit, ccfv_threshold) f1 assms(2,3) eqn1 is_pullback_def monomorphism_def3)
  qed

  have uniqueness: "βˆƒ! j. (j : Q β†’ A ∧ q1 ∘c j = q1 ∘c v ∧ q0 ∘c j = q0 ∘c u)"
   by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(3) eqn1 is_pullback_def)
  then show "u = v"
    using eqn2 equals uniqueness by (typecheck_cfuncs, auto)
qed

text β€ΉThe lemma below corresponds to Proposition 2.2.9d in Halvorson.β€Ί
lemma pullback_of_mono_is_mono2:
assumes "g: X β†’ Z" "monomorphism g" "is_pullback A Y X Z q1 f q0 g"
shows "monomorphism q1" 
  unfolding monomorphism_def2
proof(clarify)
  fix u v Q a y
  assume u_type: "u : Q β†’ a"  
  assume v_type: "v : Q β†’ a"
  assume q1_type: "q1 :  a β†’ y" 
  assume equals: "q1 ∘c u = q1 ∘c v" 

  have a_is_A: "a = A"
    using assms(3) cfunc_type_def is_pullback_def q1_type  by force
  have y_is_Y: "y = Y"
    using assms(3) cfunc_type_def is_pullback_def q1_type  by fastforce
  have u_type2[type_rule]: "u : Q β†’ A"
    using a_is_A u_type by blast
  have v_type2[type_rule]: "v : Q β†’ A"
    using a_is_A v_type by blast
  have q1_type2[type_rule]: "q1 : A β†’ Y"
    using a_is_A q1_type y_is_Y by blast

  have eqn1: "f ∘c (q1 ∘c u) = g ∘c (q0 ∘c v)"
  proof - 
    have "f ∘c (q1 ∘c u) = f ∘c q1 ∘c v"
      by (simp add: equals)
    also have "... = g ∘c (q0 ∘c v)"
      using assms(3) cfunc_type_def comp_associative is_pullback_def  by (typecheck_cfuncs, force)
    finally show ?thesis.
  qed 

  have eqn2: "q0 ∘c u =  q0  ∘c v"
  proof - 
    have f1: "g ∘c q0 ∘c u = f ∘c q1 ∘c u"
      using assms(3) comp_associative2 is_pullback_def  by (typecheck_cfuncs, auto)
    also have "... = f ∘c q1 ∘c v"
      by (simp add: equals)
    also have "... = g ∘c q0 ∘c v"
      using eqn1 equals by fastforce
    then show ?thesis
      by (typecheck_cfuncs, smt (verit, ccfv_threshold) f1 assms(2,3) eqn1 is_pullback_def monomorphism_def3)
  qed
  have uniqueness: "βˆƒ! j. (j : Q β†’ A ∧ q0 ∘c j = q0 ∘c v ∧ q1 ∘c j = q1 ∘c u)"
   by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(3) eqn1 is_pullback_def)
  then show "u = v"
    using eqn2 equals uniqueness by (typecheck_cfuncs, auto)
qed

subsection β€ΉFiber Over an Element and its Connection to the Fibered Productβ€Ί

text β€ΉThe definition below corresponds to Definition 2.2.6 in Halvorson.β€Ί
definition fiber :: "cfunc β‡’ cfunc β‡’ cset" ("_-1{_}" [100,100]100) where
  "f-1{y} = (f-1β¦‡πŸ­β¦ˆβ‡˜y⇙)"

definition fiber_morphism :: "cfunc β‡’ cfunc β‡’ cfunc" where
  "fiber_morphism f y = left_cart_proj (domain f) 𝟭 ∘c inverse_image_mapping f 𝟭 y"

lemma fiber_morphism_type[type_rule]:
  assumes "f : X β†’ Y" "y ∈c Y"
  shows "fiber_morphism f y : f-1{y} β†’ X"
  unfolding fiber_def fiber_morphism_def
  using assms cfunc_type_def element_monomorphism inverse_image_subobject subobject_of_def2
  by (typecheck_cfuncs, auto)

lemma fiber_subset: 
  assumes "f : X β†’ Y" "y ∈c Y"
  shows "(f-1{y}, fiber_morphism f y) βŠ†c X"
  unfolding fiber_def fiber_morphism_def
  using assms cfunc_type_def element_monomorphism inverse_image_subobject inverse_image_subobject_mapping_def
  by (typecheck_cfuncs, auto)

lemma fiber_morphism_monomorphism:
  assumes "f : X β†’ Y" "y ∈c Y"
  shows "monomorphism (fiber_morphism f y)"
  using assms cfunc_type_def element_monomorphism fiber_morphism_def inverse_image_monomorphism by auto

lemma fiber_morphism_eq:
  assumes "f : X β†’ Y" "y ∈c Y"
  shows "f ∘c fiber_morphism f y  = y ∘c Ξ²β‡˜f-1{y}⇙"
proof -
  have "f ∘c fiber_morphism f y = f ∘c left_cart_proj (domain f) 𝟭 ∘c inverse_image_mapping f 𝟭 y"
    unfolding fiber_morphism_def by auto
  also have "... = y ∘c right_cart_proj X 𝟭 ∘c inverse_image_mapping f 𝟭 y"
    using assms cfunc_type_def element_monomorphism inverse_image_mapping_eq by auto
  also have "... = y ∘c Ξ²β‡˜f-1β¦‡πŸ­β¦ˆβ‡˜y⇙⇙"
    using assms by (typecheck_cfuncs, metis element_monomorphism terminal_func_unique)
  also have "... = y ∘c Ξ²β‡˜f-1{y}⇙"
    unfolding fiber_def by auto
  finally show ?thesis.
qed

text β€ΉThe lemma below corresponds to Proposition 2.2.7 in Halvorson.β€Ί
lemma not_surjective_has_some_empty_preimage:
  assumes p_type[type_rule]: "p: X β†’ Y" and p_not_surj: "Β¬ surjective p"
  shows "βˆƒ y. y ∈c Y ∧ is_empty(p-1{y})"
proof -
  have nonempty: "nonempty(Y)"
    using assms cfunc_type_def nonempty_def surjective_def by auto
  obtain y0 where y0_type[type_rule]: "y0 ∈c Y" "βˆ€ x. x ∈c X ⟢ p∘c x β‰  y0"
    using assms cfunc_type_def surjective_def by auto

  have "Β¬nonempty(p-1{y0})"
  proof (rule ccontr, clarify)
    assume a1: "nonempty(p-1{y0})"
    obtain z where z_type[type_rule]: "z ∈c p-1{y0}"
      using a1 nonempty_def by blast
    have fiber_z_type: "fiber_morphism p y0 ∘c z ∈c X"
      using assms(1) comp_type fiber_morphism_type y0_type z_type by auto
    have contradiction: "p ∘c fiber_morphism p y0 ∘c z = y0"
      by (typecheck_cfuncs, smt (z3) comp_associative2 fiber_morphism_eq id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
    have "p ∘c (fiber_morphism p y0 ∘c z) β‰  y0"
      by (simp add: fiber_z_type y0_type)
    then show False
      using contradiction by blast
  qed
  then show ?thesis
    using is_empty_def nonempty_def y0_type by blast
qed

lemma fiber_iso_fibered_prod:
  assumes f_type[type_rule]: "f : X β†’ Y"
  assumes y_type[type_rule]: "y : 𝟭 β†’ Y"
  shows "f-1{y} β‰… X β‡˜f⇙×cβ‡˜yβ‡™πŸ­"
  using element_monomorphism equalizers_isomorphic f_type fiber_def fibered_product_equalizer inverse_image_is_equalizer is_isomorphic_def y_type by moura

lemma fib_prod_left_id_iso:
  assumes "g : Y β†’ X"
  shows "(X β‡˜id(X)⇙×cβ‡˜g⇙ Y) β‰… Y"
proof - 
  have is_pullback: "is_pullback (X β‡˜id(X)⇙×cβ‡˜g⇙ Y) Y X X (fibered_product_right_proj X (id(X)) g Y) g (fibered_product_left_proj X (id(X)) g Y) (id(X))"
    using assms fibered_product_is_pullback by (typecheck_cfuncs, blast)
  then have mono: "monomorphism(fibered_product_right_proj X (id(X)) g Y)"
    using assms by (typecheck_cfuncs, meson id_isomorphism iso_imp_epi_and_monic pullback_of_mono_is_mono2)
  have "epimorphism(fibered_product_right_proj X (id(X)) g Y)"
    by (meson id_isomorphism id_type is_pullback iso_imp_epi_and_monic pullback_of_epi_is_epi2)
  then have "isomorphism(fibered_product_right_proj X (id(X)) g Y)"
    by (simp add: epi_mon_is_iso mono)
  then show ?thesis
    using assms fibered_product_right_proj_type id_type is_isomorphic_def by blast
qed

lemma fib_prod_right_id_iso:
  assumes "f : X β†’ Y"
  shows "(X β‡˜f⇙×cβ‡˜id(Y)⇙ Y) β‰… X"
proof - 
  have is_pullback: "is_pullback (X β‡˜f⇙×cβ‡˜id(Y)⇙ Y) Y X Y (fibered_product_right_proj X f (id(Y)) Y) (id(Y)) (fibered_product_left_proj X f (id(Y)) Y) f "
    using assms fibered_product_is_pullback by (typecheck_cfuncs, blast)
    
  then have mono: "monomorphism(fibered_product_left_proj X f (id(Y)) Y)"
    using assms by (typecheck_cfuncs, meson id_isomorphism is_pullback iso_imp_epi_and_monic pullback_of_mono_is_mono1)
  have "epimorphism(fibered_product_left_proj X f (id(Y)) Y)"
    by (meson id_isomorphism id_type is_pullback iso_imp_epi_and_monic pullback_of_epi_is_epi1)
  then have "isomorphism(fibered_product_left_proj X f (id(Y)) Y)"
    by (simp add: epi_mon_is_iso mono)
  then show ?thesis
    using assms fibered_product_left_proj_type id_type is_isomorphic_def by blast
qed

text β€ΉThe lemma below corresponds to the discussion at the top of page 42 in Halvorson.β€Ί
lemma kernel_pair_connection:
  assumes f_type[type_rule]: "f : X β†’ Y" and g_type[type_rule]: "g : X β†’ E"
  assumes g_epi: "epimorphism g"
  assumes h_g_eq_f: "h ∘c g = f"
  assumes g_eq: "g ∘c fibered_product_left_proj X f f X = g ∘c fibered_product_right_proj X f f X "
  assumes h_type[type_rule]: "h : E β†’ Y"
  shows "βˆƒ! b. b : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E ∧
    fibered_product_left_proj E h h E ∘c b = g ∘c fibered_product_left_proj X f f X ∧
    fibered_product_right_proj E h h E ∘c b = g ∘c fibered_product_right_proj X f f X ∧
    epimorphism b"
proof -
  have gxg_fpmorph_eq: "(h ∘c left_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X
        = (h ∘c right_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X"
  proof -
    have "(h ∘c left_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X
        = h ∘c (left_cart_proj E E ∘c (g Γ—f g)) ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = h ∘c (g ∘c left_cart_proj X X) ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
    also have "... = (h ∘c g) ∘c left_cart_proj X X ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, smt comp_associative2)
    also have "... = f ∘c left_cart_proj X X ∘c fibered_product_morphism X f f X"
      by (simp add: h_g_eq_f)
    also have "... = f ∘c right_cart_proj X X ∘c fibered_product_morphism X f f X"
      using f_type fibered_product_left_proj_def fibered_product_proj_eq fibered_product_right_proj_def by auto
    also have "... = (h ∘c g) ∘c right_cart_proj X X ∘c fibered_product_morphism X f f X"
      by (simp add: h_g_eq_f)
    also have "... = h ∘c (g ∘c right_cart_proj X X) ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, smt comp_associative2)
    also have "... = h ∘c right_cart_proj E E ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
    also have "... = (h ∘c right_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X"
      by (typecheck_cfuncs, smt comp_associative2)
    finally show ?thesis.
  qed
  have h_equalizer: "equalizer (E β‡˜h⇙×cβ‡˜h⇙ E) (fibered_product_morphism E h h E) (h ∘c left_cart_proj E E) (h ∘c right_cart_proj E E)"
    using fibered_product_morphism_equalizer h_type by auto
  then have "βˆ€j F. j : F β†’ E Γ—c E ∧ (h ∘c left_cart_proj E E) ∘c j = (h ∘c right_cart_proj E E) ∘c j ⟢
               (βˆƒ!k. k : F β†’ E β‡˜h⇙×cβ‡˜h⇙ E ∧ fibered_product_morphism E h h E ∘c k = j)"
    unfolding equalizer_def using cfunc_type_def fibered_product_morphism_type h_type by (smt (verit))
  then have "(g Γ—f g) ∘c fibered_product_morphism X f f X  : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E Γ—c E ∧ (h ∘c left_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X = (h ∘c right_cart_proj E E) ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X ⟢
               (βˆƒ!k. k : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E ∧ fibered_product_morphism E h h E ∘c k = (g Γ—f g) ∘c fibered_product_morphism X f f X)"
    by auto
  then obtain b where b_type[type_rule]: "b : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E"
          and b_eq: "fibered_product_morphism E h h E ∘c b = (g Γ—f g) ∘c fibered_product_morphism X f f X"
    by (meson cfunc_cross_prod_type comp_type f_type fibered_product_morphism_type g_type gxg_fpmorph_eq)

  have "is_pullback (X β‡˜f⇙×cβ‡˜f⇙ X) (X Γ—c X) (E β‡˜h⇙×cβ‡˜h⇙ E) (E Γ—c E)
      (fibered_product_morphism X f f X) (g Γ—f g) b (fibered_product_morphism E h h E)"
    unfolding is_pullback_def
  proof (typecheck_cfuncs, safe, metis b_eq)
    fix Z k j
    assume k_type[type_rule]: "k : Z β†’ X Γ—c X" and h_type[type_rule]: "j : Z β†’ E β‡˜h⇙×cβ‡˜h⇙ E"
    assume k_h_eq: "(g Γ—f g) ∘c k = fibered_product_morphism E h h E ∘c j"

    have left_k_right_k_eq: "f ∘c left_cart_proj X X ∘c k = f ∘c right_cart_proj X X ∘c k"
    proof -
      have "f ∘c left_cart_proj X X ∘c k = h ∘c g ∘c left_cart_proj X X ∘c k"
        by (smt (z3) assms(6) comp_associative2 comp_type g_type h_g_eq_f k_type left_cart_proj_type)
      also have "... = h ∘c left_cart_proj E E ∘c (g Γ—f g) ∘c k"
        by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
      also have "... = h ∘c left_cart_proj E E ∘c fibered_product_morphism E h h E ∘c j"
        by (simp add: k_h_eq)
      also have "... = ((h ∘c left_cart_proj E E) ∘c fibered_product_morphism E h h E) ∘c j"
        by (typecheck_cfuncs, smt comp_associative2)
      also have "... = ((h ∘c right_cart_proj E E) ∘c fibered_product_morphism E h h E) ∘c j"
        using equalizer_def h_equalizer by auto
      also have "... = h ∘c right_cart_proj E E ∘c fibered_product_morphism E h h E ∘c j"
        by (typecheck_cfuncs, smt comp_associative2)
      also have "... = h ∘c right_cart_proj E E ∘c (g Γ—f g) ∘c k"
        by (simp add: k_h_eq)
      also have "... = h ∘c g ∘c right_cart_proj X X ∘c k"
        by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
      also have "... = f ∘c right_cart_proj X X ∘c k"
        using assms(6) comp_associative2 comp_type g_type h_g_eq_f k_type right_cart_proj_type by blast
      finally show ?thesis.
    qed

    have "is_pullback (X β‡˜f⇙×cβ‡˜f⇙ X) X X Y
        (fibered_product_right_proj X f f X) f (fibered_product_left_proj X f f X) f"
      by (simp add: f_type fibered_product_is_pullback)
    then have "right_cart_proj X X ∘c k : Z β†’ X ⟹ left_cart_proj X X ∘c k : Z β†’ X ⟹ f ∘c right_cart_proj X X ∘c k = f ∘c left_cart_proj X X ∘c k ⟹
      (βˆƒ!j. j : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X ∧
        fibered_product_right_proj X f f X ∘c j = right_cart_proj X X ∘c k
        ∧ fibered_product_left_proj X f f X ∘c j = left_cart_proj X X ∘c k)"
      unfolding is_pullback_def by auto
    then obtain z where z_type[type_rule]: "z : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X"
        and k_right_eq: "fibered_product_right_proj X f f X ∘c z = right_cart_proj X X ∘c k" 
        and k_left_eq: "fibered_product_left_proj X f f X ∘c z = left_cart_proj X X ∘c k"
        and z_unique: "β‹€j. j : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X 
          ∧ fibered_product_right_proj X f f X ∘c j = right_cart_proj X X ∘c k
          ∧ fibered_product_left_proj X f f X ∘c j = left_cart_proj X X ∘c k ⟹ z = j"
      using left_k_right_k_eq by (typecheck_cfuncs, auto)

    have k_eq: "fibered_product_morphism X f f X ∘c z = k"
      using k_right_eq k_left_eq
      unfolding fibered_product_right_proj_def fibered_product_left_proj_def
      by (typecheck_cfuncs_prems, smt cfunc_prod_comp cfunc_prod_unique)

    then show "βˆƒl. l : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X ∧ fibered_product_morphism X f f X ∘c l = k ∧ b ∘c l = j"
    proof (intro exI[where x=z], clarify)
      assume k_def: "k = fibered_product_morphism X f f X ∘c z"
      have "fibered_product_morphism E h h E ∘c j = (g Γ—f g) ∘c k"
        by (simp add: k_h_eq)
      also have "... = (g Γ—f g) ∘c fibered_product_morphism X f f X ∘c z"
        by (simp add: k_eq)
      also have "... = fibered_product_morphism E h h E ∘c b ∘c z"
        by (typecheck_cfuncs, simp add: b_eq comp_associative2)
      then show "z : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X ∧ fibered_product_morphism X f f X ∘c z = fibered_product_morphism X f f X ∘c z ∧ b ∘c z = j"
        by (typecheck_cfuncs, metis assms(6) fibered_product_morphism_monomorphism fibered_product_morphism_type k_def k_h_eq monomorphism_def3)
    qed

    show "β‹€ j y. j : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X ⟹ y : Z β†’ X β‡˜f⇙×cβ‡˜f⇙ X ⟹
        fibered_product_morphism X f f X ∘c y = fibered_product_morphism X f f X ∘c j ⟹
        j = y"
      using fibered_product_morphism_monomorphism monomorphism_def2 by (typecheck_cfuncs_prems, metis)
  qed
  then have b_epi: "epimorphism b"
    using g_epi g_type cfunc_cross_prod_type cfunc_cross_prod_surj  pullback_of_epi_is_epi1 h_type
    by (meson epi_is_surj surjective_is_epimorphism)

  have existence: "βˆƒb. b : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E ∧
        fibered_product_left_proj E h h E ∘c b = g ∘c fibered_product_left_proj X f f X ∧
        fibered_product_right_proj E h h E ∘c b = g ∘c fibered_product_right_proj X f f X ∧
        epimorphism b"
  proof (intro exI[where x=b], safe)
    show "b : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E"
      by typecheck_cfuncs
    show "fibered_product_left_proj E h h E ∘c b = g ∘c fibered_product_left_proj X f f X"
    proof -
      have "fibered_product_left_proj E h h E ∘c b
          = left_cart_proj E E ∘c fibered_product_morphism E h h E ∘c b"
        unfolding fibered_product_left_proj_def by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = left_cart_proj E E ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X"
        by (simp add: b_eq)
      also have "... = g ∘c left_cart_proj X X ∘c fibered_product_morphism X f f X"
        by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
      also have "... = g ∘c fibered_product_left_proj X f f X"
        unfolding fibered_product_left_proj_def by (typecheck_cfuncs)
      finally show ?thesis.
    qed
    show "fibered_product_right_proj E h h E ∘c b = g ∘c fibered_product_right_proj X f f X"
    proof -
      have "fibered_product_right_proj E h h E ∘c b
          = right_cart_proj E E ∘c fibered_product_morphism E h h E ∘c b"
        unfolding fibered_product_right_proj_def by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = right_cart_proj E E ∘c (g Γ—f g) ∘c fibered_product_morphism X f f X"
        by (simp add: b_eq)
      also have "... = g ∘c right_cart_proj X X ∘c fibered_product_morphism X f f X"
        by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
      also have "... = g ∘c fibered_product_right_proj X f f X"
        unfolding fibered_product_right_proj_def by (typecheck_cfuncs)
      finally show ?thesis.
    qed
    show "epimorphism b"
      by (simp add: b_epi)
  qed  
  show "βˆƒ!b. b : X β‡˜f⇙×cβ‡˜f⇙ X β†’ E β‡˜h⇙×cβ‡˜h⇙ E ∧
         fibered_product_left_proj E h h E ∘c b = g ∘c fibered_product_left_proj X f f X ∧
         fibered_product_right_proj E h h E ∘c b = g ∘c fibered_product_right_proj X f f X ∧
         epimorphism b"
    by (typecheck_cfuncs, metis epimorphism_def2 existence g_eq iso_imp_epi_and_monic kern_pair_proj_iso_TFAE2 monomorphism_def3)
qed

section β€ΉSet Subtractionβ€Ί

definition set_subtraction :: "cset β‡’ cset Γ— cfunc β‡’ cset" (infix "βˆ–" 60) where
  "Y βˆ– X = (SOME E. βˆƒ m'.  equalizer E m' (characteristic_func (snd X)) (𝖿 ∘c Ξ²β‡˜Y⇙))"

lemma set_subtraction_equalizer:
  assumes "m : X β†’ Y" "monomorphism m"
  shows "βˆƒ m'.  equalizer (Y βˆ– (X,m)) m' (characteristic_func m) (𝖿 ∘c Ξ²β‡˜Y⇙)"
proof -
  have "βˆƒ E m'. equalizer E m' (characteristic_func m) (𝖿 ∘c Ξ²β‡˜Y⇙)"
    using assms equalizer_exists by (typecheck_cfuncs, auto)
  then have "βˆƒ m'.  equalizer (Y βˆ– (X,m)) m' (characteristic_func (snd (X,m))) (𝖿 ∘c Ξ²β‡˜Y⇙)"
    unfolding set_subtraction_def by (subst someI_ex, auto)
  then show "βˆƒ m'.  equalizer (Y βˆ– (X,m)) m' (characteristic_func m) (𝖿 ∘c Ξ²β‡˜Y⇙)"
    by auto
qed

definition complement_morphism :: "cfunc β‡’ cfunc" ("_c" [1000]) where
  "mc = (SOME m'.  equalizer (codomain m βˆ– (domain m, m)) m' (characteristic_func m) (𝖿 ∘c Ξ²β‡˜codomain m⇙))"

lemma complement_morphism_equalizer:
  assumes "m : X β†’ Y" "monomorphism m"
  shows "equalizer (Y βˆ– (X,m)) mc (characteristic_func m) (𝖿 ∘c Ξ²β‡˜Y⇙)"
proof -
  have "βˆƒ m'. equalizer (codomain m βˆ– (domain m, m)) m' (characteristic_func m) (𝖿 ∘c Ξ²β‡˜codomain m⇙)"
    by (simp add: assms cfunc_type_def set_subtraction_equalizer)
  then have "equalizer (codomain m βˆ– (domain m, m)) mc (characteristic_func m) (𝖿 ∘c Ξ²β‡˜codomain m⇙)"
    unfolding complement_morphism_def by (subst someI_ex, auto)
  then show "equalizer (Y βˆ– (X, m)) mc (characteristic_func m) (𝖿 ∘c Ξ²β‡˜Y⇙)"
    using assms unfolding cfunc_type_def by auto
qed

lemma complement_morphism_type[type_rule]:
  assumes "m : X β†’ Y" "monomorphism m"
  shows "mc : Y βˆ– (X,m) β†’ Y"
  using assms cfunc_type_def characteristic_func_type complement_morphism_equalizer equalizer_def by auto

lemma complement_morphism_mono:
  assumes "m : X β†’ Y" "monomorphism m"
  shows "monomorphism mc"
  using assms complement_morphism_equalizer equalizer_is_monomorphism by blast

lemma complement_morphism_eq:
  assumes "m : X β†’ Y" "monomorphism m"
  shows "characteristic_func m ∘c mc  = (𝖿 ∘c Ξ²β‡˜Y⇙) ∘c mc"
  using assms complement_morphism_equalizer unfolding equalizer_def by auto

lemma characteristic_func_true_not_complement_member:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes characteristic_func_true: "characteristic_func m ∘c x = 𝗍"
  shows "Β¬ x βˆˆβ‡˜X⇙ (X βˆ– (B, m),mc)"
proof
  assume in_complement: "x βˆˆβ‡˜X⇙ (X βˆ– (B, m), mc)"
  then obtain x' where x'_type: "x' ∈c X βˆ– (B,m)" and x'_def: "mc ∘c x' = x"
    using assms cfunc_type_def complement_morphism_type factors_through_def relative_member_def2
    by auto
  then have "characteristic_func m ∘c mc = (𝖿 ∘c Ξ²β‡˜X⇙) ∘c mc"
    using assms complement_morphism_equalizer equalizer_def by blast
  then have "characteristic_func m ∘c x = 𝖿 ∘c Ξ²β‡˜X⇙ ∘c x"
    using assms x'_type complement_morphism_type
    by (typecheck_cfuncs, smt x'_def assms cfunc_type_def comp_associative domain_comp)
  then have "characteristic_func m ∘c x = 𝖿"
    using assms by (typecheck_cfuncs, metis id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
  then show False
    using characteristic_func_true true_false_distinct by auto
qed

lemma characteristic_func_false_complement_member:
  assumes "m : B β†’ X" "monomorphism m" "x ∈c X"
  assumes characteristic_func_false: "characteristic_func m ∘c x = 𝖿"
  shows "x βˆˆβ‡˜X⇙ (X βˆ– (B, m),mc)"
proof -
  have x_equalizes: "characteristic_func m ∘c x = 𝖿 ∘c Ξ²β‡˜X⇙ ∘c x"
    by (metis assms(3) characteristic_func_false false_func_type id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
  have "β‹€h F. h : F β†’ X ∧ characteristic_func m ∘c h = (𝖿 ∘c Ξ²β‡˜X⇙) ∘c h ⟢
                  (βˆƒ!k. k : F β†’ X βˆ– (B, m) ∧ mc ∘c k = h)"
    using assms complement_morphism_equalizer unfolding equalizer_def
    by (smt cfunc_type_def characteristic_func_type) 
  then obtain x' where x'_type: "x' ∈c X βˆ– (B, m)" and x'_def: "mc ∘c x' = x"
    by (metis assms(3) cfunc_type_def comp_associative false_func_type terminal_func_type x_equalizes)
  then show "x βˆˆβ‡˜X⇙ (X βˆ– (B, m),mc)"
    unfolding relative_member_def factors_through_def
    using assms complement_morphism_mono complement_morphism_type cfunc_type_def by auto
qed

lemma in_complement_not_in_subset:
  assumes "m : X β†’ Y" "monomorphism m" "x ∈c Y"
  assumes "x βˆˆβ‡˜Y⇙ (Y βˆ– (X,m), mc)"
  shows "Β¬ x βˆˆβ‡˜Y⇙ (X, m)"
  using assms characteristic_func_false_not_relative_member
    characteristic_func_true_not_complement_member characteristic_func_type comp_type
    true_false_only_truth_values by blast

lemma not_in_subset_in_complement:
  assumes "m : X β†’ Y" "monomorphism m" "x ∈c Y"
  assumes "Β¬ x βˆˆβ‡˜Y⇙ (X, m)"
  shows "x βˆˆβ‡˜Y⇙ (Y βˆ– (X,m), mc)"
  using assms characteristic_func_false_complement_member characteristic_func_true_relative_member
    characteristic_func_type comp_type true_false_only_truth_values by blast

lemma complement_disjoint:
  assumes "m : X β†’ Y" "monomorphism m"
  assumes "x ∈c X" "x' ∈c Y βˆ– (X,m)"
  shows "m ∘c x β‰  mc ∘c x'"
proof 
  assume "m ∘c x = mc ∘c x'"
  then have "characteristic_func m ∘c m ∘c x = characteristic_func m ∘c mc ∘c x'"
    by auto
  then have "(characteristic_func m ∘c m) ∘c x = (characteristic_func m ∘c mc) ∘c x'"
    using assms comp_associative2 by (typecheck_cfuncs, auto)
  then have "(𝗍 ∘c Ξ²β‡˜X⇙) ∘c x = ((𝖿 ∘c Ξ²β‡˜Y⇙) ∘c mc) ∘c x'"
    using assms characteristic_func_eq complement_morphism_eq by auto
  then have "𝗍 ∘c Ξ²β‡˜X⇙ ∘c x = 𝖿 ∘c Ξ²β‡˜Y⇙ ∘c mc ∘c x'"
    using assms comp_associative2 by (typecheck_cfuncs, smt terminal_func_comp terminal_func_type)
  then have "𝗍 ∘c id 𝟭 = 𝖿 ∘c id 𝟭"
    using assms by (smt cfunc_type_def comp_associative complement_morphism_type id_type one_unique_element terminal_func_comp terminal_func_type)
  then have "𝗍 = 𝖿"
    using false_func_type id_right_unit2 true_func_type by auto
  then show False
    using true_false_distinct by auto
qed

lemma set_subtraction_right_iso:
  assumes m_type[type_rule]: "m : A β†’ C" and m_mono[type_rule]: "monomorphism m"
  assumes i_type[type_rule]: "i : B β†’ A" and i_iso: "isomorphism i"
  shows "C βˆ– (A,m) = C βˆ– (B, m ∘c i)"
proof -
  have mi_mono[type_rule]: "monomorphism (m ∘c i)"
    using cfunc_type_def composition_of_monic_pair_is_monic i_iso i_type iso_imp_epi_and_monic m_mono m_type by presburger
  obtain Ο‡m where Ο‡m_type[type_rule]: "Ο‡m : C β†’ Ξ©" and Ο‡m_def: "Ο‡m = characteristic_func m"
    using characteristic_func_type m_mono m_type by blast
  obtain Ο‡mi where Ο‡mi_type[type_rule]: "Ο‡mi : C β†’ Ξ©" and Ο‡mi_def: "Ο‡mi = characteristic_func (m ∘c i)"
    by (typecheck_cfuncs, simp)
  have "β‹€ c. c ∈c C ⟹ (Ο‡m ∘c c = 𝗍) = (Ο‡mi ∘c c = 𝗍)"
  proof -
    fix c
    assume c_type[type_rule]: "c ∈c C"
    have "(Ο‡m ∘c c = 𝗍) = (c βˆˆβ‡˜C⇙ (A,m))"
      by (typecheck_cfuncs, metis Ο‡m_def m_mono not_rel_mem_char_func_false rel_mem_char_func_true true_false_distinct)
    also have "... = (βˆƒ a. a ∈c A ∧ c = m ∘c a)"
      using cfunc_type_def factors_through_def m_mono relative_member_def2 by (typecheck_cfuncs, auto)
    also have "... = (βˆƒ b. b ∈c B ∧ c = m ∘c i ∘c b)"
      by (typecheck_cfuncs, smt (z3) cfunc_type_def comp_type epi_is_surj i_iso iso_imp_epi_and_monic surjective_def)
    also have "... = (c βˆˆβ‡˜C⇙ (B,m ∘c i))"
      using cfunc_type_def comp_associative2 composition_of_monic_pair_is_monic factors_through_def2 i_iso iso_imp_epi_and_monic m_mono relative_member_def2
      by (typecheck_cfuncs, auto)
    also have "... = (Ο‡mi ∘c c = 𝗍)"
      by (typecheck_cfuncs, metis Ο‡mi_def mi_mono not_rel_mem_char_func_false rel_mem_char_func_true true_false_distinct)
    finally show "(Ο‡m ∘c c = 𝗍) = (Ο‡mi ∘c c = 𝗍)".
  qed
  then have "Ο‡m = Ο‡mi"
    by (typecheck_cfuncs, smt (verit, best) comp_type one_separator true_false_only_truth_values) 
  then show "C βˆ– (A,m) = C βˆ– (B, m ∘c i)"
    using Ο‡m_def Ο‡mi_def isomorphic_is_reflexive set_subtraction_def by auto
qed

lemma set_subtraction_left_iso:
  assumes m_type[type_rule]: "m : C β†’ A" and m_mono[type_rule]: "monomorphism m"
  assumes i_type[type_rule]: "i : A β†’ B" and i_iso: "isomorphism i"
  shows "A βˆ– (C,m) β‰… B βˆ– (C, i ∘c m)"
proof -
  have im_mono[type_rule]: "monomorphism (i ∘c m)"
    using cfunc_type_def composition_of_monic_pair_is_monic i_iso i_type iso_imp_epi_and_monic m_mono m_type by presburger
  obtain Ο‡m where Ο‡m_type[type_rule]: "Ο‡m : A β†’ Ξ©" and Ο‡m_def: "Ο‡m = characteristic_func m"
    using characteristic_func_type m_mono m_type by blast
  obtain Ο‡im where Ο‡im_type[type_rule]: "Ο‡im : B β†’ Ξ©" and Ο‡im_def: "Ο‡im = characteristic_func (i ∘c m)"
    by (typecheck_cfuncs, simp)
  have Ο‡im_pullback: "is_pullback C 𝟭 B Ξ© (Ξ²β‡˜C⇙) 𝗍 (i ∘c m) Ο‡im"
    using Ο‡im_def characteristic_func_is_pullback comp_type i_type im_mono m_type by blast
  have "is_pullback C 𝟭 A Ξ© (Ξ²β‡˜C⇙) 𝗍 m (Ο‡im ∘c i)"
    unfolding is_pullback_def
  proof (typecheck_cfuncs, safe)
    show "𝗍 ∘c Ξ²β‡˜C⇙ = (Ο‡im ∘c i) ∘c m"
      by (typecheck_cfuncs, etcs_assocr, metis Ο‡im_def characteristic_func_eq comp_type im_mono)
  next
    fix Z k h
    assume k_type[type_rule]: "k : Z β†’ 𝟭" and h_type[type_rule]: "h : Z β†’ A"
    assume eq: "𝗍 ∘c k = (Ο‡im ∘c i) ∘c h"
    then obtain j where j_type[type_rule]: "j : Z β†’ C" and j_def: "i ∘c h = (i ∘c m) ∘c j"
      using Ο‡im_pullback unfolding is_pullback_def by (typecheck_cfuncs, smt (verit, ccfv_threshold) comp_associative2 k_type)
    then show "βˆƒj. j : Z β†’ C ∧ Ξ²β‡˜C⇙ ∘c j = k ∧ m ∘c j = h"
      by (intro exI[where x=j], typecheck_cfuncs, smt comp_associative2 i_iso iso_imp_epi_and_monic monomorphism_def2 terminal_func_unique)
  next
    fix Z j y
    assume j_type[type_rule]: "j : Z β†’ C" and y_type[type_rule]: "y : Z β†’ C"
    assume "𝗍 ∘c Ξ²β‡˜C⇙ ∘c j = (Ο‡im ∘c i) ∘c m ∘c j" "Ξ²β‡˜C⇙ ∘c y = Ξ²β‡˜C⇙ ∘c j" "m ∘c y = m ∘c j"
    then show "j = y"
      using m_mono monomorphism_def2 by (typecheck_cfuncs_prems, blast)
  qed
  then have Ο‡im_i_eq_Ο‡m: "Ο‡im ∘c i = Ο‡m"
    using Ο‡m_def characteristic_func_is_pullback characteristic_function_exists m_mono m_type by blast
  then have "Ο‡im ∘c (i ∘c mc) = 𝖿 ∘c Ξ²β‡˜B⇙ ∘c (i ∘c mc)"
    by (etcs_assocl, typecheck_cfuncs, smt (verit, best) Ο‡m_def comp_associative2 complement_morphism_eq m_mono terminal_func_comp)
  then obtain i' where i'_type[type_rule]: "i' : A βˆ– (C, m) β†’ B βˆ– (C, i ∘c m)" and i'_def: "i ∘c mc = (i ∘c m)c ∘c i'"
    using complement_morphism_equalizer unfolding equalizer_def
    by (-, typecheck_cfuncs, smt Ο‡im_def cfunc_type_def comp_associative2 im_mono)

  have "Ο‡m ∘c (iΒ― ∘c (i ∘c m)c) = 𝖿 ∘c Ξ²β‡˜A⇙ ∘c (iΒ― ∘c (i ∘c m)c)"
  proof -
    have "Ο‡m ∘c (iΒ― ∘c (i ∘c m)c) = Ο‡im ∘c (i ∘c iΒ―) ∘c (i ∘c m)c"
      by (typecheck_cfuncs, simp add: Ο‡im_i_eq_Ο‡m cfunc_type_def comp_associative i_iso)
    also have "... = Ο‡im ∘c (i ∘c m)c"
      using i_iso id_left_unit2 inv_right by (typecheck_cfuncs, auto)
    also have "... = 𝖿 ∘c Ξ²β‡˜B⇙ ∘c (i ∘c m)c"
      by (typecheck_cfuncs, simp add: Ο‡im_def comp_associative2 complement_morphism_eq im_mono)
    also have "... = 𝖿 ∘c Ξ²β‡˜A⇙ ∘c (iΒ― ∘c (i ∘c m)c)"
      by (typecheck_cfuncs, metis i_iso terminal_func_unique)
    finally show ?thesis.
  qed
  then obtain i'_inv where i'_inv_type[type_rule]: "i'_inv : B βˆ– (C, i ∘c m) β†’ A βˆ– (C, m)"
    and i'_inv_def: "(i ∘c m)c = (i ∘c mc) ∘c i'_inv"
    using complement_morphism_equalizer[where m="m", where X=C, where Y=A] unfolding equalizer_def
    by (-, typecheck_cfuncs, smt (z3) Ο‡m_def cfunc_type_def comp_associative2 i_iso id_left_unit2 inv_right m_mono)

  have "isomorphism i'"
  proof (etcs_subst isomorphism_def3, intro exI[where x = "i'_inv"], safe)
    show "i'_inv : B βˆ– (C, i ∘c m) β†’ A βˆ– (C, m)"
      by typecheck_cfuncs
    have "i ∘c mc = (i ∘c mc) ∘c i'_inv ∘c i'"
      using i'_inv_def by (etcs_subst i'_def, etcs_assocl, auto)
    then show "i'_inv ∘c i' = idc (A βˆ– (C, m))"
      by (typecheck_cfuncs_prems, smt (verit, best) cfunc_type_def complement_morphism_mono composition_of_monic_pair_is_monic i_iso id_right_unit2 id_type iso_imp_epi_and_monic m_mono monomorphism_def3)
  next
    have "(i ∘c m)c = (i ∘c m)c ∘c i' ∘c i'_inv"
      using i'_def by (etcs_subst i'_inv_def, etcs_assocl, auto)
    then show "i' ∘c i'_inv = idc (B βˆ– (C, i ∘c m))"
      by (typecheck_cfuncs_prems, metis complement_morphism_mono id_right_unit2 id_type im_mono monomorphism_def3)
  qed
  then show "A βˆ– (C, m) β‰… B βˆ– (C, i ∘c m)"
    using i'_type is_isomorphic_def by blast
qed

section  β€ΉGraphsβ€Ί

definition functional_on :: "cset β‡’ cset β‡’ cset Γ— cfunc β‡’ bool" where
  "functional_on X Y R = (R  βŠ†c X Γ—c Y ∧
    (βˆ€x. x ∈c X ⟢ (βˆƒ! y.  y ∈c Y ∧  
      ⟨x,y⟩ βˆˆβ‡˜XΓ—cY⇙ R)))" 

text β€ΉThe definition below corresponds to Definition 2.3.12 in Halvorson.β€Ί
definition graph :: "cfunc β‡’ cset" where
 "graph f = (SOME E. βˆƒ m. equalizer E m (f ∘c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f)))"

lemma graph_equalizer:
  "βˆƒ m. equalizer (graph f) m (f ∘c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f))"
  unfolding graph_def
  by (typecheck_cfuncs, rule someI_ex, simp add: cfunc_type_def equalizer_exists)
  
lemma graph_equalizer2:
  assumes "f : X β†’ Y"
  shows "βˆƒ m. equalizer (graph f) m (f ∘c left_cart_proj X Y) (right_cart_proj X Y)"
  using assms by (typecheck_cfuncs, metis cfunc_type_def graph_equalizer)

definition graph_morph :: "cfunc β‡’ cfunc" where
 "graph_morph f = (SOME m. equalizer (graph f) m (f ∘c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f)))"

lemma graph_equalizer3:
  "equalizer (graph f) (graph_morph f) (f ∘c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f))"
  unfolding graph_morph_def by (rule someI_ex, simp add: graph_equalizer)

lemma graph_equalizer4:
  assumes "f : X β†’ Y"
  shows "equalizer (graph f) (graph_morph f) (f ∘c left_cart_proj X Y) (right_cart_proj X Y)"
  using assms cfunc_type_def graph_equalizer3 by auto

lemma graph_subobject:
  assumes "f : X β†’ Y"
  shows "(graph f, graph_morph f) βŠ†c (X Γ—c Y)"
  by (metis assms cfunc_type_def equalizer_def equalizer_is_monomorphism graph_equalizer3 right_cart_proj_type subobject_of_def2)

lemma graph_morph_type[type_rule]:
  assumes "f : X β†’ Y"
  shows "graph_morph(f) : graph f β†’ X Γ—c Y"
  using graph_subobject subobject_of_def2 assms by auto

text β€ΉThe lemma below corresponds to Exercise 2.3.13 in Halvorson.β€Ί
lemma graphs_are_functional:
  assumes "f : X β†’ Y"
  shows "functional_on X Y (graph f, graph_morph f)"
  unfolding functional_on_def
proof(safe)
  show graph_subobj: "(graph f, graph_morph f)  βŠ†c (XΓ—c Y)"
    by (simp add: assms graph_subobject)
  show "β‹€x. x ∈c X ⟹ βˆƒy. y ∈c Y ∧ ⟨x,y⟩ βˆˆβ‡˜X Γ—c Y⇙ (graph f, graph_morph f)"
  proof - 
    fix x 
    assume x_type[type_rule]: "x ∈c X"
    obtain y where y_def: "y = f ∘c x"
      by simp
    then have y_type[type_rule]: "y ∈c Y"
      using assms comp_type x_type y_def by blast

    have "⟨x,y⟩ βˆˆβ‡˜X Γ—c Y⇙ (graph f, graph_morph f)"
      unfolding relative_member_def
    proof(typecheck_cfuncs, safe)
      show "monomorphism (snd (graph f, graph_morph f))"
        using graph_subobj subobject_of_def by auto
      show " snd (graph f, graph_morph f) : fst (graph f, graph_morph f) β†’ X Γ—c Y"
        by (simp add: assms graph_morph_type)
      have "⟨x,y⟩ factorsthru graph_morph f"
      proof(subst xfactorthru_equalizer_iff_fx_eq_gx[where E = "graph f", where m = "graph_morph f",  
                                                     where f = "(f ∘c left_cart_proj X Y)", where g = "right_cart_proj X Y", where X = "X Γ—c Y", where Y = Y,
                                                     where x ="⟨x,y⟩"])
        show "f ∘c left_cart_proj X Y : X Γ—c Y β†’ Y"
          using assms by typecheck_cfuncs
        show "right_cart_proj X Y : X Γ—c Y β†’ Y"
          by  typecheck_cfuncs
        show "equalizer (graph f) (graph_morph f) (f ∘c left_cart_proj X Y) (right_cart_proj X Y)"
          by (simp add: assms graph_equalizer4)
        show "⟨x,y⟩ ∈c X Γ—c Y"
          by typecheck_cfuncs
        show "(f ∘c left_cart_proj X Y) ∘c ⟨x,y⟩ = right_cart_proj X Y ∘c ⟨x,y⟩"
          using assms  
          by (typecheck_cfuncs, smt (z3) comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_def)
      qed
      then show "⟨x,y⟩ factorsthru snd (graph f, graph_morph f)"
        by simp
    qed
    then show "βˆƒy. y ∈c Y ∧ ⟨x,y⟩ βˆˆβ‡˜X Γ—c Y⇙ (graph f, graph_morph f)"
      using y_type by blast
  qed
  show "β‹€x y ya.
       x ∈c X ⟹
       y ∈c Y ⟹
       ⟨x,y⟩ βˆˆβ‡˜X Γ—c Y⇙ (graph f, graph_morph f) ⟹ 
        ya ∈c Y ⟹ 
        ⟨x,ya⟩ βˆˆβ‡˜X Γ—c Y⇙ (graph f, graph_morph f)
         ⟹ y = ya"
    using assms  
    by (smt (z3) comp_associative2 equalizer_def factors_through_def2 graph_equalizer4 left_cart_proj_cfunc_prod left_cart_proj_type relative_member_def2 right_cart_proj_cfunc_prod)
qed

lemma functional_on_isomorphism:
  assumes "functional_on X Y (R,m)"
  shows "isomorphism(left_cart_proj X Y ∘c m)"
proof-
  have m_mono: "monomorphism(m)"
    using assms functional_on_def subobject_of_def2 by blast
  have pi0_m_type[type_rule]: "left_cart_proj X Y ∘c m : R β†’ X"
    using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
  have surj: "surjective(left_cart_proj X Y ∘c m)"
    unfolding surjective_def
  proof(clarify)
    fix x 
    assume "x ∈c codomain (left_cart_proj X Y ∘c m)"
    then have [type_rule]: "x ∈c X"
      using cfunc_type_def pi0_m_type by force
    then have "βˆƒ! y. (y ∈c Y ∧  ⟨x,y⟩ βˆˆβ‡˜XΓ—cY⇙ (R,m))"
      using assms functional_on_def  by force
    then show "βˆƒz. z ∈c domain (left_cart_proj X Y ∘c m) ∧ (left_cart_proj X Y ∘c m) ∘c z = x"
      by (typecheck_cfuncs, smt (verit, best) cfunc_type_def comp_associative factors_through_def2 left_cart_proj_cfunc_prod relative_member_def2)
  qed
  have inj: "injective(left_cart_proj X Y ∘c m)"
  proof(unfold injective_def, clarify)
    fix r1 r2 
    assume "r1 ∈c domain (left_cart_proj X Y ∘c m)" then have r1_type[type_rule]: "r1 ∈c R"
      by (metis cfunc_type_def pi0_m_type)
    assume "r2 ∈c domain (left_cart_proj X Y ∘c m)" then have r2_type[type_rule]: "r2 ∈c R"
      by (metis cfunc_type_def pi0_m_type)
    assume "(left_cart_proj X Y ∘c m) ∘c r1 = (left_cart_proj X Y ∘c m) ∘c r2"
    then have eq: "left_cart_proj X Y ∘c m ∘c r1 = left_cart_proj X Y ∘c m ∘c r2"
      using assms cfunc_type_def comp_associative functional_on_def subobject_of_def2 by (typecheck_cfuncs, auto)
    have mx_type[type_rule]: "m ∘c r1 ∈c XΓ—cY"
      using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
    then obtain x1 and y1 where m1r1_eqs: "m ∘c r1 = ⟨x1, y1⟩ ∧ x1 ∈c X ∧ y1 ∈c Y"
      using cart_prod_decomp by presburger
    have my_type[type_rule]: "m ∘c r2 ∈c XΓ—cY"
      using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
    then obtain x2 and y2 where m2r2_eqs:"m ∘c r2 = ⟨x2, y2⟩ ∧ x2 ∈c X ∧ y2 ∈c Y"
      using cart_prod_decomp by presburger
    have x_equal: "x1 = x2"
      using eq left_cart_proj_cfunc_prod m1r1_eqs m2r2_eqs by force
    have functional: "βˆƒ! y. (y ∈c Y ∧  ⟨x1,y⟩ βˆˆβ‡˜XΓ—cY⇙ (R,m))"
      using assms functional_on_def m1r1_eqs by force
    then have y_equal: "y1 = y2"
      by (metis prod.sel factors_through_def2 m1r1_eqs m2r2_eqs mx_type my_type r1_type r2_type relative_member_def x_equal)
    then show "r1 = r2"
      by (metis functional cfunc_type_def m1r1_eqs m2r2_eqs monomorphism_def r1_type r2_type relative_member_def2 x_equal)
  qed
  show "isomorphism(left_cart_proj X Y ∘c m)"
    by (metis epi_mon_is_iso inj injective_imp_monomorphism surj surjective_is_epimorphism)
qed

text β€ΉThe lemma below corresponds to Proposition 2.3.14 in Halvorson.β€Ί
lemma functional_relations_are_graphs:
  assumes "functional_on X Y (R,m)"
  shows "βˆƒ! f. f : X β†’ Y ∧ 
    (βˆƒ i. i : R β†’ graph(f) ∧ isomorphism(i) ∧ m = graph_morph(f) ∘c i)"
proof safe
  have m_type[type_rule]: "m : R β†’ X Γ—c Y"
    using assms unfolding functional_on_def subobject_of_def2 by auto
  have m_mono[type_rule]: "monomorphism(m)"
    using assms functional_on_def subobject_of_def2 by blast
  have isomorphism[type_rule]: "isomorphism(left_cart_proj X Y ∘c m)"
    using assms functional_on_isomorphism by force
  
  obtain h where h_type[type_rule]: "h: X β†’ R" and h_def: "h = (left_cart_proj X Y ∘c m)Β―"
    by (typecheck_cfuncs, simp)
  obtain f where f_def: "f = (right_cart_proj X Y) ∘c m ∘c h"
    by auto
  then have f_type[type_rule]: "f : X β†’ Y"
    by (metis assms comp_type f_def functional_on_def h_type right_cart_proj_type subobject_of_def2)

  have eq: "f ∘c left_cart_proj X Y ∘c m = right_cart_proj X Y ∘c m"
    unfolding f_def h_def by (typecheck_cfuncs, smt comp_associative2 id_right_unit2 inv_left isomorphism)

  show "βˆƒf. f : X β†’ Y ∧ (βˆƒi. i : R β†’ graph f ∧ isomorphism i ∧ m = graph_morph f ∘c i)"
  proof (intro exI[where x=f], safe, typecheck_cfuncs)
    have graph_equalizer: "equalizer (graph f) (graph_morph f) (f ∘c left_cart_proj X Y) (right_cart_proj X Y)"
      by (simp add: f_type graph_equalizer4)
    then have "βˆ€h F. h : F β†’ X Γ—c Y ∧ (f ∘c left_cart_proj X Y) ∘c h = right_cart_proj X Y ∘c h ⟢
          (βˆƒ!k. k : F β†’ graph f ∧ graph_morph f ∘c k = h)"
      unfolding equalizer_def using cfunc_type_def by (typecheck_cfuncs, auto)
    then obtain i where i_type[type_rule]: "i : R β†’ graph f" and i_eq: "graph_morph f ∘c i = m"
      by (typecheck_cfuncs, smt comp_associative2 eq left_cart_proj_type)
    have "surjective i"
    proof (etcs_subst surjective_def2, clarify)
      fix y'
      assume y'_type[type_rule]: "y' ∈c graph f"

      define x where "x = left_cart_proj X Y ∘c graph_morph(f) ∘c y'"
      then have x_type[type_rule]: "x ∈c X"
        unfolding x_def by typecheck_cfuncs

      obtain y where y_type[type_rule]: "y ∈c Y" and x_y_in_R: "⟨x,y⟩ βˆˆβ‡˜X Γ—c Y⇙ (R, m)"
        and y_unique: "βˆ€ z. (z ∈c Y ∧ ⟨x,z⟩ βˆˆβ‡˜X Γ—c Y⇙ (R, m)) ⟢ z = y"
        by (metis assms functional_on_def x_type)

      obtain x' where x'_type[type_rule]: "x' ∈c R" and x'_eq: "m ∘c x' = ⟨x, y⟩"
        using x_y_in_R unfolding relative_member_def2 by (-, etcs_subst_asm factors_through_def2, auto)

      have "graph_morph(f) ∘c i ∘c x' = graph_morph(f) ∘c y'"
      proof (typecheck_cfuncs, rule cart_prod_eqI, safe)
        show left: "left_cart_proj X Y ∘c graph_morph f ∘c i ∘c x' = left_cart_proj X Y ∘c graph_morph f ∘c y'"
        proof -
          have "left_cart_proj X Y ∘c graph_morph(f) ∘c i ∘c x' = left_cart_proj X Y ∘c m ∘c x'"
            by (typecheck_cfuncs, smt comp_associative2 i_eq)
          also have "... = x"
            unfolding x'_eq using left_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)
          also have "... = left_cart_proj X Y ∘c graph_morph f ∘c y'"
            unfolding x_def by auto
          finally show ?thesis.
        qed

        show "right_cart_proj X Y ∘c graph_morph f ∘c i ∘c x' = right_cart_proj X Y ∘c graph_morph f ∘c y'"
        proof -
          have "right_cart_proj X Y ∘c graph_morph f ∘c i ∘c x' = f ∘c left_cart_proj X Y ∘c graph_morph f ∘c i ∘c x'"
            by (etcs_assocl, typecheck_cfuncs, metis graph_equalizer equalizer_eq)
          also have "... = f ∘c left_cart_proj X Y ∘c graph_morph f ∘c y'"
            by (subst left, simp)
          also have "... = right_cart_proj X Y ∘c graph_morph f ∘c y'"
            by (etcs_assocl, typecheck_cfuncs, metis graph_equalizer equalizer_eq)
          finally show ?thesis.
        qed
      qed
      then have "i ∘c x' = y'"
        using equalizer_is_monomorphism graph_equalizer monomorphism_def2 by (typecheck_cfuncs_prems, blast)
      then show "βˆƒx'. x' ∈c R ∧ i ∘c x' = y'"
        by (intro exI[where x=x'], simp add: x'_type)
    qed
    then have "isomorphism i"
      by (metis comp_monic_imp_monic' epi_mon_is_iso f_type graph_morph_type i_eq i_type m_mono surjective_is_epimorphism)
    then show "βˆƒi. i : R β†’ graph f ∧ isomorphism i ∧ m = graph_morph f ∘c i"
      by (intro exI[where x=i], simp add: i_type i_eq)
  qed
next
  fix f1 f2 i1 i2
  assume f1_type[type_rule]: "f1 : X β†’ Y"
  assume f2_type[type_rule]: "f2 : X β†’ Y"
  assume i1_type[type_rule]: "i1 : R β†’ graph f1"
  assume i2_type[type_rule]: "i2 : R β†’ graph f2"
  assume i1_iso: "isomorphism i1"
  assume i2_iso: "isomorphism i2"
  assume eq1: "m = graph_morph f1 ∘c i1"
  assume eq2: "graph_morph f1 ∘c i1 = graph_morph f2 ∘c i2" 

  have m_type[type_rule]: "m : R β†’ X Γ—c Y"
    using assms unfolding functional_on_def subobject_of_def2 by auto
  have isomorphism[type_rule]: "isomorphism(left_cart_proj X Y ∘c m)"
    using assms functional_on_isomorphism by force  
  obtain h where h_type[type_rule]: "h: X β†’ R" and h_def: "h = (left_cart_proj X Y ∘c m)Β―"
    by (typecheck_cfuncs, simp)
  have "f1 ∘c left_cart_proj X Y ∘c m = f2 ∘c left_cart_proj X Y ∘c m"
  proof - 
    have "f1 ∘c left_cart_proj X Y ∘c m = (f1 ∘c left_cart_proj X Y) ∘c graph_morph f1 ∘c i1"
      using comp_associative2 eq1 eq2 by (typecheck_cfuncs, force)
    also have "... = (right_cart_proj X Y) ∘c graph_morph f1 ∘c i1"
      by (typecheck_cfuncs, smt comp_associative2 equalizer_def graph_equalizer4)
    also have "... = (right_cart_proj X Y) ∘c graph_morph f2 ∘c i2"
      by (simp add: eq2)
    also have "... = (f2 ∘c left_cart_proj X Y) ∘c graph_morph f2 ∘c i2"
      by (typecheck_cfuncs, smt comp_associative2 equalizer_eq graph_equalizer4)
    also have "... = f2 ∘c left_cart_proj X Y ∘c m"
      by (typecheck_cfuncs, metis comp_associative2 eq1 eq2)
    finally show ?thesis.
  qed
  then show "f1 = f2"
    by (typecheck_cfuncs, metis cfunc_type_def comp_associative h_def h_type id_right_unit2 inverse_def2 isomorphism)
qed

end