Theory Coproduct

section ‹Coproducts›

theory Coproduct
  imports Equivalence
begin

(* We define our own (ETCS) case_bool later, so we need to hide the HOL version. *)
hide_const case_bool

text ‹The axiomatization below corresponds to Axiom 7 (Coproducts) in Halvorson.›
axiomatization
  coprod :: "cset ⇒ cset ⇒ cset" (infixr "∐" 65) and
  left_coproj :: "cset ⇒ cset ⇒ cfunc" and
  right_coproj :: "cset ⇒ cset ⇒ cfunc" and
  cfunc_coprod :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "⨿" 65)
where
  left_proj_type[type_rule]: "left_coproj X Y : X → X∐Y" and
  right_proj_type[type_rule]: "right_coproj X Y : Y → X∐Y" and
  cfunc_coprod_type[type_rule]: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g :  X∐Y → Z" and
  left_coproj_cfunc_coprod: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g ∘⇩c (left_coproj X Y)  = f" and
  right_coproj_cfunc_coprod: "f : X → Z ⟹ g : Y → Z ⟹ f⨿g ∘⇩c (right_coproj X Y)  = g" and
  cfunc_coprod_unique: "f : X → Z ⟹ g : Y → Z ⟹ h : X ∐ Y → Z ⟹ 
    h ∘⇩c left_coproj X Y = f ⟹ h ∘⇩c right_coproj X Y = g ⟹ h = f ⨿ g"

definition is_coprod :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cset ⇒ bool" where
  "is_coprod W i⇩0 i⇩1 X Y ⟷ 
    (i⇩0 : X → W ∧ i⇩1 : Y → W ∧
    (∀ f g Z. (f : X → Z ∧ g : Y → Z) ⟶ 
      (∃ h. h :  W → Z ∧ h ∘⇩c i⇩0 = f ∧ h ∘⇩c i⇩1 = g ∧
        (∀ h2. (h2 : W → Z ∧ h2 ∘⇩c i⇩0 = f ∧ h2 ∘⇩c i⇩1 = g) ⟶ h2 = h))))"

lemma is_coprod_def2:
  assumes "i⇩0 : X → W" "i⇩1 : Y → W"
  shows "is_coprod W i⇩0 i⇩1 X Y ⟷ 
    (∀ f g Z. (f : X → Z ∧ g : Y → Z) ⟶ 
      (∃ h. h :  W → Z ∧ h ∘⇩c i⇩0 = f ∧ h ∘⇩c i⇩1 = g ∧
        (∀ h2. (h2 : W → Z ∧ h2 ∘⇩c i⇩0 = f ∧ h2 ∘⇩c i⇩1 = g) ⟶ h2 = h)))"
  unfolding is_coprod_def using assms by auto

abbreviation is_coprod_triple :: "cset × cfunc × cfunc ⇒ cset ⇒ cset ⇒ bool" where
  "is_coprod_triple Wi X Y ≡ is_coprod (fst Wi) (fst (snd Wi)) (snd (snd Wi)) X Y"

lemma canonical_coprod_is_coprod:
 "is_coprod (X ∐ Y) (left_coproj X Y) (right_coproj X Y) X Y"
  unfolding is_coprod_def
proof (typecheck_cfuncs)
  fix f g Z
  assume f_type: "f : X → Z"
  assume g_type: "g : Y → Z"
  show "∃h. h : X ∐ Y → Z ∧
           h ∘⇩c left_coproj X Y = f ∧
           h ∘⇩c right_coproj X Y = g ∧ (∀h2. h2 : X ∐ Y → Z ∧ h2 ∘⇩c left_coproj X Y = f ∧ h2 ∘⇩c right_coproj X Y = g ⟶ h2 = h)"
    using cfunc_coprod_type cfunc_coprod_unique f_type g_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod 
    by(intro exI[where x="f⨿g"], auto)
qed

text ‹The lemma below is dual to Proposition 2.1.8 in Halvorson.›
lemma coprods_isomorphic:
  assumes W_coprod:  "is_coprod_triple (W, i⇩0, i⇩1) X Y"
  assumes W'_coprod: "is_coprod_triple (W', i'⇩0, i'⇩1) X Y"
  shows "∃ g. g : W → W' ∧ isomorphism g ∧ g ∘⇩c i⇩0  = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
proof -
  obtain f where f_def: "f : W' → W ∧ f ∘⇩c i'⇩0  = i⇩0 ∧ f ∘⇩c i'⇩1 = i⇩1"
    using W_coprod W'_coprod unfolding is_coprod_def
    by (metis split_pairs)

  obtain g where g_def: "g : W → W' ∧ g ∘⇩c i⇩0  = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
    using W_coprod W'_coprod unfolding is_coprod_def
    by (metis split_pairs)

  have fg0: "(f ∘⇩c g) ∘⇩c  i⇩0   = i⇩0"
    by (metis W_coprod comp_associative2 f_def g_def is_coprod_def split_pairs)
  have fg1: "(f ∘⇩c g) ∘⇩c  i⇩1   = i⇩1"
    by (metis W_coprod comp_associative2 f_def g_def is_coprod_def split_pairs)
    
  obtain idW where "idW : W → W ∧ (∀ h2. (h2 : W → W ∧ h2 ∘⇩c i⇩0  = i⇩0 ∧ h2 ∘⇩c i⇩1 = i⇩1) ⟶ h2 = idW)"
    by (smt (verit, best) W_coprod is_coprod_def prod.sel)
  then have fg: "f ∘⇩c g = id W"
  proof clarify
    assume idW_unique: "∀h2. h2 : W → W ∧ h2 ∘⇩c i⇩0 = i⇩0 ∧ h2 ∘⇩c i⇩1 = i⇩1 ⟶ h2 = idW"
    have 1: "f ∘⇩c g = idW"
      using comp_type f_def fg0 fg1 g_def idW_unique by blast
    have 2: "id W = idW"
      using W_coprod idW_unique id_left_unit2 id_type is_coprod_def by auto
    from 1 2 show "f ∘⇩c g = id W"
      by auto
  qed

  have gf0: "(g ∘⇩c f) ∘⇩c i'⇩0= i'⇩0"
    using W'_coprod comp_associative2 f_def g_def is_coprod_def by auto
  have gf1: "(g ∘⇩c f) ∘⇩c i'⇩1 = i'⇩1"
    using W'_coprod comp_associative2 f_def g_def is_coprod_def by auto

  obtain idW' where "idW': W'→ W'∧ (∀ h2. (h2 : W'→ W'∧  h2 ∘⇩c i'⇩0= i'⇩0 ∧ h2 ∘⇩c i'⇩1= i'⇩1) ⟶ h2 = idW')"
    by (smt (verit, best) W'_coprod is_coprod_def prod.sel)
  then have gf: "g ∘⇩c f = id W'"
  proof clarify
    assume idW'_unique: "∀h2. h2 : W' → W' ∧ h2 ∘⇩c i'⇩0 = i'⇩0 ∧ h2 ∘⇩c i'⇩1 = i'⇩1 ⟶ h2 = idW'"
    have 1: "g ∘⇩c f = idW'"
      using comp_type f_def g_def gf0 gf1 idW'_unique by blast
    have 2: "id W' = idW'"
      using W'_coprod idW'_unique id_left_unit2 id_type is_coprod_def by auto      
    from 1 2 show "g ∘⇩c f = id W'"
      by auto
  qed

  have g_iso: "isomorphism g"
    using f_def fg g_def gf isomorphism_def3 by blast
  from g_iso g_def show "∃ g. g : W → W' ∧ isomorphism g ∧ g ∘⇩c i⇩0  = i'⇩0 ∧ g ∘⇩c i⇩1 = i'⇩1"
    by blast
qed

subsection  ‹Coproduct Function Properities›

lemma cfunc_coprod_comp:
  assumes "a : Y → Z" "b : X → Y" "c : W → Y"
  shows "(a ∘⇩c b) ⨿ (a ∘⇩c c) = a ∘⇩c (b ⨿ c)"
proof -
  have "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (left_coproj X W) = a ∘⇩c (b ⨿ c) ∘⇩c (left_coproj X W)"
    using assms by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
  then have left_coproj_eq: "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (left_coproj X W) = (a ∘⇩c (b ⨿ c)) ∘⇩c (left_coproj X W)"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  have "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (right_coproj X W) = a ∘⇩c (b ⨿ c) ∘⇩c (right_coproj X W)"
    using assms by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
  then have right_coproj_eq: "((a ∘⇩c b) ⨿ (a ∘⇩c c)) ∘⇩c (right_coproj X W) = (a ∘⇩c (b ⨿ c)) ∘⇩c (right_coproj X W)"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)

  show "(a ∘⇩c b) ⨿ (a ∘⇩c c) = a ∘⇩c (b ⨿ c)"
    using assms left_coproj_eq right_coproj_eq
    by (typecheck_cfuncs, smt cfunc_coprod_unique left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
qed

lemma id_coprod:
  "id(A ∐ B) = (left_coproj A B) ⨿ (right_coproj A B)"
    by (typecheck_cfuncs, simp add: cfunc_coprod_unique id_left_unit2)

text ‹The lemma below corresponds to Proposition 2.4.1 in Halvorson.›
lemma coproducts_disjoint:
  " x∈⇩c X ⟹  y ∈⇩c Y ⟹  (left_coproj X Y) ∘⇩c x ≠ (right_coproj X Y) ∘⇩c y"
proof (rule ccontr, clarify)
  assume x_type[type_rule]: "x∈⇩c X" 
  assume y_type[type_rule]: "y ∈⇩c Y"
  assume BWOC: "((left_coproj X Y) ∘⇩c x = (right_coproj X Y) ∘⇩c y)"
  obtain g where g_def: "g factorsthru  𝗍" and g_type[type_rule]: "g: X → Ω"
    by (typecheck_cfuncs, meson comp_type factors_through_def2 terminal_func_type)
  then have fact1: "𝗍 = g ∘⇩c x"
    by (metis cfunc_type_def comp_associative factors_through_def id_right_unit2 id_type
        terminal_func_comp terminal_func_unique true_func_type x_type)
     
  obtain h where h_def: "h factorsthru 𝖿" and h_type[type_rule]: "h: Y → Ω"
    by (typecheck_cfuncs, meson comp_type factors_through_def2 one_terminal_object terminal_object_def)
  then have gUh_type[type_rule]: "g ⨿ h: X ∐ Y → Ω" and 
                        gUh_def: "(g ⨿ h) ∘⇩c (left_coproj X Y) = g ∧  (g ⨿ h) ∘⇩c (right_coproj X Y) = h"
    using left_coproj_cfunc_coprod right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
  then have fact2: "𝖿 = ((g ⨿ h) ∘⇩c (right_coproj X Y)) ∘⇩c y"
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 factors_through_def2 gUh_def h_def id_right_unit2 terminal_func_comp_elem terminal_func_unique)
  also have "... = ((g ⨿ h) ∘⇩c (left_coproj X Y)) ∘⇩c x"
    by (smt BWOC comp_associative2 gUh_type left_proj_type right_proj_type x_type y_type) 
  also have "... = 𝗍"
    by (simp add: fact1 gUh_def)
  ultimately show False
    using true_false_distinct by auto
qed

text ‹The lemma below corresponds to Proposition 2.4.2 in Halvorson.›
lemma left_coproj_are_monomorphisms:
  "monomorphism(left_coproj X Y)"
proof (cases "∃x. x ∈⇩c X")
  assume X_nonempty: "∃x. x ∈⇩c X"
  then obtain x where x_type[type_rule]: "x ∈⇩c X"
    by auto
  then have "(id X ⨿ (x ∘⇩c β⇘Y⇙)) ∘⇩c left_coproj X Y = id X"
    by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
  then show "monomorphism (left_coproj X Y)"
    by (typecheck_cfuncs, metis (mono_tags) cfunc_coprod_type comp_monic_imp_monic'
        comp_type id_isomorphism id_type iso_imp_epi_and_monic terminal_func_type x_type)
next
  show "∄x. x ∈⇩c X ⟹ monomorphism (left_coproj X Y)"
    by (typecheck_cfuncs, metis cfunc_type_def injective_def injective_imp_monomorphism)
qed

lemma right_coproj_are_monomorphisms:
  "monomorphism(right_coproj X Y)"
proof (cases "∃y. y ∈⇩c Y")
  assume Y_nonempty: "∃y. y ∈⇩c Y"
  then obtain y where y_type[type_rule]:  "y ∈⇩c Y"
    by auto
  have "((y ∘⇩c β⇘X⇙) ⨿ id Y) ∘⇩c right_coproj X Y = id Y"
    by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
  then show "monomorphism (right_coproj X Y)"
    by (typecheck_cfuncs, metis (mono_tags) cfunc_coprod_type comp_monic_imp_monic'
        comp_type id_isomorphism id_type iso_imp_epi_and_monic terminal_func_type y_type)
next
  show "∄y. y ∈⇩c Y ⟹ monomorphism (right_coproj X Y)"
    by (typecheck_cfuncs, metis cfunc_type_def injective_def injective_imp_monomorphism)
qed

text ‹The lemma below corresponds to Exercise 2.4.3 in Halvorson.›
lemma coprojs_jointly_surj:
  assumes z_type[type_rule]: "z ∈⇩c X ∐ Y"
  shows "(∃ x. (x ∈⇩c X ∧ z = (left_coproj X Y) ∘⇩c x))
      ∨  (∃ y. (y ∈⇩c Y ∧ z = (right_coproj X Y) ∘⇩c y))"
proof (clarify, rule ccontr)
  assume not_in_right_image: "∄y. y ∈⇩c Y ∧ z = right_coproj X Y ∘⇩c y"
  assume not_in_left_image: "∄x. x ∈⇩c X ∧ z = left_coproj X Y ∘⇩c x"
  
  obtain h where h_def: "h = 𝖿 ∘⇩c β⇘X ∐ Y⇙" and h_type[type_rule]: "h : X ∐ Y → Ω"
    by (typecheck_cfuncs, simp)

  have fact1: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c left_coproj X Y = h ∘⇩c left_coproj X Y"
  proof(etcs_rule one_separator[where X=X, where Y = Ω])
    show "⋀x. x ∈⇩c X ⟹ ((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x =
                          (h ∘⇩c left_coproj X Y) ∘⇩c x"
    proof - 
      fix x
      assume x_type: "x ∈⇩c X"
      have "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x = 
              eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩ ∘⇩c (left_coproj X Y ∘⇩c  x)"
             using x_type by (typecheck_cfuncs, metis assms cfunc_type_def comp_associative)
      also have "... = 𝖿"
        using assms eq_pred_false_extract_right not_in_left_image x_type by (typecheck_cfuncs, presburger)
      also have "... = h ∘⇩c (left_coproj X Y ∘⇩c x)"
        using x_type by (typecheck_cfuncs, smt comp_associative2 h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
      also have "... = (h ∘⇩c left_coproj X Y) ∘⇩c x"
             using x_type cfunc_type_def comp_associative comp_type false_func_type h_def terminal_func_type by (typecheck_cfuncs, force)
      finally show "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c left_coproj X Y) ∘⇩c x  = (h ∘⇩c left_coproj X Y) ∘⇩c x".
    qed
  qed

  have fact2: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c right_coproj X Y = h ∘⇩c right_coproj X Y"
  proof(etcs_rule one_separator[where X = Y, where Y = Ω])
    show "⋀x. x ∈⇩c Y ⟹
           ((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c x =
           (h ∘⇩c right_coproj X Y) ∘⇩c x"
    proof - 
      fix x
      assume x_type[type_rule]: "x ∈⇩c Y"
      have "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c x = 𝖿"
        by (typecheck_cfuncs, smt (verit) assms cfunc_type_def eq_pred_false_extract_right comp_associative comp_type not_in_right_image)
      also have "... = (h ∘⇩c right_coproj X Y) ∘⇩c x"
        by (etcs_assocr,typecheck_cfuncs, metis cfunc_type_def comp_associative h_def id_right_unit2 terminal_func_comp_elem terminal_func_type)
      finally show "((eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c right_coproj X Y) ∘⇩c  x = (h ∘⇩c right_coproj X Y) ∘⇩c x".
    qed
  qed
  have indicator_is_false:"eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩ = h"
  proof(etcs_rule one_separator[where X = "X ∐ Y", where Y = Ω])
    show "⋀x. x ∈⇩c X ∐ Y ⟹ (eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙,id⇩c (X ∐ Y)⟩) ∘⇩c x = h ∘⇩c x"
      by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp fact1 fact2 id_coprod id_right_unit2 left_proj_type right_proj_type)
  qed
  have hz_gives_false: "h ∘⇩c z = 𝖿"
    using assms by (typecheck_cfuncs, smt comp_associative2 h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
  then have indicator_z_gives_false: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c z = 𝖿"
    using assms indicator_is_false  by (typecheck_cfuncs, blast)
  then have indicator_z_gives_true: "(eq_pred (X ∐ Y) ∘⇩c ⟨z ∘⇩c β⇘X ∐ Y⇙, id (X ∐ Y)⟩) ∘⇩c z = 𝗍"
    using assms by (typecheck_cfuncs, smt (verit, del_insts) comp_associative2 eq_pred_true_extract_right)
  then show False
    using indicator_z_gives_false true_false_distinct by auto
qed

lemma maps_into_1u1:
  assumes x_type:  "x∈⇩c (𝟭 ∐ 𝟭)"
  shows "(x = left_coproj 𝟭 𝟭) ∨ (x = right_coproj 𝟭 𝟭)"
  using assms by (typecheck_cfuncs, metis coprojs_jointly_surj terminal_func_unique)

lemma coprod_preserves_left_epi:
  assumes "f: X → Z" "g: Y → Z"
  assumes "surjective(f)"
  shows "surjective(f ⨿ g)"
  unfolding surjective_def
proof(clarify)
  fix z
  assume y_type[type_rule]: "z ∈⇩c codomain (f ⨿ g)"
  then obtain x where x_def: "x ∈⇩c X ∧ f ∘⇩c x  = z"
    using assms cfunc_coprod_type cfunc_type_def cfunc_type_def surjective_def by auto
  have "(f ⨿ g) ∘⇩c (left_coproj X Y ∘⇩c x) = z"
    by (typecheck_cfuncs, smt assms comp_associative2 left_coproj_cfunc_coprod x_def)
  then show "∃x. x ∈⇩c domain(f ⨿ g) ∧ f ⨿ g ∘⇩c x = z"
    by (typecheck_cfuncs, metis assms(1,2) cfunc_type_def codomain_comp domain_comp left_proj_type x_def)
qed

lemma coprod_preserves_right_epi:
  assumes "f: X → Z" "g: Y → Z"
  assumes "surjective(g)"
  shows "surjective(f ⨿ g)"
  unfolding surjective_def
proof(clarify)
  fix z
  assume y_type: "z ∈⇩c codomain (f ⨿ g)"
  have fug_type: "(f ⨿ g) : (X ∐ Y) → Z"
    by (typecheck_cfuncs, simp add: assms)
  then have y_type2: "z ∈⇩c Z"
    using cfunc_type_def y_type by auto
  then have "∃ y. y ∈⇩c Y ∧ g ∘⇩c y  = z"
    using assms(2,3) cfunc_type_def surjective_def by auto
  then obtain y where y_def: "y ∈⇩c Y ∧ g ∘⇩c y  = z"
    by blast
  have coproj_x_type: "right_coproj X Y ∘⇩c y  ∈⇩c X ∐ Y"
    using comp_type right_proj_type y_def by blast
  have "(f ⨿ g) ∘⇩c (right_coproj X Y ∘⇩c y) = z"
    using assms(1) assms(2) cfunc_type_def comp_associative fug_type right_coproj_cfunc_coprod right_proj_type y_def by auto
  then show "∃y. y ∈⇩c domain(f ⨿ g) ∧ f ⨿ g ∘⇩c y = z"
    using cfunc_type_def coproj_x_type fug_type by auto
qed

lemma coprod_eq:
  assumes "a : X ∐ Y → Z" "b : X ∐ Y →  Z"
  shows "a = b ⟷ 
    (a ∘⇩c left_coproj X Y   = b ∘⇩c left_coproj X Y 
      ∧ a ∘⇩c right_coproj X Y  = b ∘⇩c right_coproj X Y)"
  by (smt assms cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type)

lemma coprod_eqI:
  assumes "a : X ∐ Y → Z" "b : X ∐ Y → Z"
  assumes "(a ∘⇩c left_coproj X Y   = b ∘⇩c left_coproj X Y 
      ∧ a ∘⇩c right_coproj X Y  = b ∘⇩c right_coproj X Y)"
  shows "a = b"
  using assms coprod_eq by blast

lemma coprod_eq2:
  assumes "a : X → Z" "b : Y → Z" "c : X →  Z" "d : Y →  Z"
  shows "(a ⨿ b) = (c ⨿ d) ⟷ (a = c ∧ b = d)"
  by (metis assms left_coproj_cfunc_coprod right_coproj_cfunc_coprod)

lemma coprod_decomp:
  assumes "a : X ∐ Y → A"
  shows "∃ x y. a = (x ⨿ y) ∧ x : X → A ∧ y : Y → A"
proof (rule exI[where x="a ∘⇩c left_coproj X Y"], intro exI[where x="a ∘⇩c right_coproj X Y"], safe)
  show "a = (a ∘⇩c left_coproj X Y) ⨿ (a ∘⇩c right_coproj X Y)"
    using assms cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type by auto
  show "a ∘⇩c left_coproj X Y : X → A"
    by (meson assms comp_type left_proj_type)
  show "a ∘⇩c right_coproj X Y : Y → A"
    by (meson assms comp_type right_proj_type)
qed

text ‹The lemma below corresponds to Proposition 2.4.4 in Halvorson.›
lemma truth_value_set_iso_1u1:
  "isomorphism(𝗍⨿𝖿)"
  by (typecheck_cfuncs, smt (verit, best) CollectI epi_mon_is_iso injective_def2
      injective_imp_monomorphism left_coproj_cfunc_coprod left_proj_type maps_into_1u1
      right_coproj_cfunc_coprod right_proj_type surjective_def2 surjective_is_epimorphism 
      true_false_distinct true_false_only_truth_values)

subsubsection  ‹Equality Predicate with Coproduct Properities›

lemma eq_pred_left_coproj:
  assumes u_type[type_rule]: "u ∈⇩c X ∐ Y" and x_type[type_rule]: "x ∈⇩c X"
  shows "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩ = ((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c u"
proof (cases "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩= 𝗍")
  assume case1: "eq_pred (X ∐ Y) ∘⇩c ⟨u, left_coproj X Y ∘⇩c x⟩ = 𝗍"
  then have u_is_left_coproj: "u = left_coproj X Y ∘⇩c x"
    using eq_pred_iff_eq by (typecheck_cfuncs_prems, presburger)  
  show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
  proof -
    have "((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c u
        = ((eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)) ∘⇩c left_coproj X Y ∘⇩c x"
      using u_is_left_coproj by auto
    also have "... =  (eq_pred X ∘⇩c ⟨id X, x ∘⇩c β⇘X⇙⟩) ∘⇩c x "
      by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
    also have "... = eq_pred X ∘⇩c ⟨x, x⟩"
      by (typecheck_cfuncs, metis cart_prod_extract_left cfunc_type_def comp_associative)
    also have "... = 𝗍"
      using eq_pred_iff_eq by (typecheck_cfuncs, blast)
    ultimately show ?thesis
      by (simp add: case1)
  qed
next
  assume "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ ≠ 𝗍"
  then have case2: "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = 𝖿"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have u_not_left_coproj_x: "u  ≠ left_coproj X Y ∘⇩c x"
    using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)
  show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
  proof (cases "∃ g. g : 𝟭 → X ∧ u = left_coproj X Y ∘⇩c g")  
    assume "∃g. g ∈⇩c X ∧ u = left_coproj X Y ∘⇩c g"
    then obtain g where g_type[type_rule]: "g ∈⇩c X" and g_def: "u = left_coproj X Y ∘⇩c g"
      by auto
    then have x_not_g: "x ≠ g"
      using u_not_left_coproj_x by auto
    show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"
    proof -
      have "(eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c left_coproj X Y ∘⇩c g
          = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ∘⇩c g"
        using comp_associative2 left_coproj_cfunc_coprod by (typecheck_cfuncs, force)
      also have "... = eq_pred X ∘⇩c ⟨g,x⟩"
        by (typecheck_cfuncs, simp add: cart_prod_extract_left comp_associative2)
      also have "... = 𝖿"
        using eq_pred_iff_eq_conv x_not_g by (typecheck_cfuncs, blast)
      ultimately show ?thesis
        using case2 g_def by argo
    qed
  next
    assume "∄g. g ∈⇩c X ∧ u = left_coproj X Y ∘⇩c g"
    then obtain g where g_type[type_rule]: "g ∈⇩c Y" and g_def: "u = right_coproj X Y ∘⇩c g"
      by (meson coprojs_jointly_surj u_type)

    show "eq_pred (X ∐ Y) ∘⇩c ⟨u,left_coproj X Y ∘⇩c x⟩ = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u"  
    proof -
      have "(eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c u
          = (eq_pred X ∘⇩c ⟨id⇩c X,x ∘⇩c β⇘X⇙⟩) ⨿ (𝖿 ∘⇩c β⇘Y⇙)  ∘⇩c right_coproj X Y ∘⇩c g"
        using g_def by auto
      also have "... = (𝖿 ∘⇩c β⇘Y⇙) ∘⇩c g"
        by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
      also have "... = 𝖿"
        by (typecheck_cfuncs, smt (z3) comp_associative2 id_right_unit2 id_type terminal_func_comp terminal_func_unique)
      ultimately show ?thesis
        using case2 by argo
    qed
  qed
qed

lemma eq_pred_right_coproj:
  assumes u_type[type_rule]: "u ∈⇩c X ∐ Y" and y_type[type_rule]: "y ∈⇩c Y"
  shows "eq_pred (X ∐ Y) ∘⇩c ⟨u, right_coproj X Y ∘⇩c y⟩ = ((𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id Y, y ∘⇩c β⇘Y⇙⟩)) ∘⇩c u"
proof (cases "eq_pred (X ∐ Y) ∘⇩c ⟨u, right_coproj X Y ∘⇩c y⟩ = 𝗍")
  assume case1: "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = 𝗍"
  then have u_is_right_coproj: "u = right_coproj X Y ∘⇩c y"
    using eq_pred_iff_eq by (typecheck_cfuncs_prems, presburger)
  show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
  proof -
    have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u
        = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c right_coproj X Y ∘⇩c y"
      using u_is_right_coproj by auto
    also have "... = (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c y"
      by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
    also have "... = eq_pred Y ∘⇩c ⟨y,y⟩"
      by (typecheck_cfuncs, smt cart_prod_extract_left comp_associative2)
    also have "... = 𝗍"
      using eq_pred_iff_eq y_type by auto
    ultimately show ?thesis
      using case1 by argo
  qed
next
  assume "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ ≠ 𝗍"
  then have eq_pred_false: "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = 𝖿"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have u_not_right_coproj_y: "u  ≠ right_coproj X Y ∘⇩c y"
    using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)

  show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
  proof (cases "∃ g. g : 𝟭 → Y ∧ u = right_coproj X Y ∘⇩c g")
    assume "∃g. g ∈⇩c Y ∧ u = right_coproj X Y ∘⇩c g"
    then obtain g where g_type[type_rule]: "g ∈⇩c Y" and g_def: "u = right_coproj X Y ∘⇩c g"
      by auto
    then have y_not_g: "y ≠ g"
      using u_not_right_coproj_y by auto

    show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
    proof -
      have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c right_coproj X Y ∘⇩c g
          = (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c g"
        by (typecheck_cfuncs, simp add: comp_associative2 right_coproj_cfunc_coprod)
      also have "... = eq_pred Y ∘⇩c ⟨g,y⟩"
        using cart_prod_extract_left comp_associative2 by (typecheck_cfuncs, auto)
      also have "... = 𝖿"
        using eq_pred_iff_eq_conv y_not_g y_type g_type by blast
      ultimately show ?thesis
        using eq_pred_false g_def by argo
    qed
  next
    assume "∄g. g ∈⇩c Y ∧ u = right_coproj X Y ∘⇩c g"
    then obtain g where g_type[type_rule]: "g ∈⇩c X" and g_def: "u = left_coproj X Y ∘⇩c g"
      by (meson coprojs_jointly_surj u_type)
    show "eq_pred (X ∐ Y) ∘⇩c ⟨u,right_coproj X Y ∘⇩c y⟩ = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u"
    proof -
      have "(𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c u
          = (𝖿 ∘⇩c β⇘X⇙) ⨿ (eq_pred Y ∘⇩c ⟨id⇩c Y,y ∘⇩c β⇘Y⇙⟩) ∘⇩c left_coproj X Y ∘⇩c g"
        using g_def by auto
      also have "... = (𝖿 ∘⇩c β⇘X⇙) ∘⇩c g"
        by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
      also have "... = 𝖿"
        by (typecheck_cfuncs, smt (z3) comp_associative2 id_right_unit2 id_type terminal_func_comp terminal_func_unique)
      ultimately show ?thesis
        using eq_pred_false by auto
    qed
  qed
qed

subsection  ‹Bowtie Product›

definition cfunc_bowtie_prod :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "⨝⇩f" 55) where
  "f ⨝⇩f g = ((left_coproj (codomain f) (codomain g)) ∘⇩c f) ⨿ ((right_coproj (codomain f) (codomain g)) ∘⇩c g)"

lemma cfunc_bowtie_prod_def2: 
  assumes "f : X → Y" "g : V→ W"
  shows "f ⨝⇩f g = (left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)"
  using assms cfunc_bowtie_prod_def cfunc_type_def by auto

lemma cfunc_bowtie_prod_type[type_rule]:
  "f : X → Y ⟹ g : V → W ⟹ f ⨝⇩f g : X ∐ V → Y ∐ W"
  unfolding cfunc_bowtie_prod_def
  using cfunc_coprod_type cfunc_type_def comp_type left_proj_type right_proj_type by auto

lemma left_coproj_cfunc_bowtie_prod:
  "f : X → Y ⟹ g : V → W ⟹ (f ⨝⇩f g) ∘⇩c left_coproj X V = left_coproj Y W ∘⇩c f"
  unfolding cfunc_bowtie_prod_def2
  by (meson comp_type left_coproj_cfunc_coprod left_proj_type right_proj_type)

 lemma right_coproj_cfunc_bowtie_prod:
  "f : X → Y ⟹ g : V → W ⟹ (f ⨝⇩f g) ∘⇩c right_coproj X V = right_coproj Y W ∘⇩c g"
  unfolding cfunc_bowtie_prod_def2
  by (meson comp_type right_coproj_cfunc_coprod right_proj_type left_proj_type)

lemma cfunc_bowtie_prod_unique: "f : X → Y ⟹ g : V → W ⟹ h : X ∐ V → Y ∐ W ⟹
    h ∘⇩c left_coproj X V   = left_coproj Y W ∘⇩c f ⟹
    h ∘⇩c right_coproj X V = right_coproj Y W ∘⇩c g ⟹ h = f ⨝⇩f g"
  unfolding cfunc_bowtie_prod_def
  using cfunc_coprod_unique cfunc_type_def codomain_comp domain_comp left_proj_type right_proj_type by auto

text ‹The lemma below is dual to Proposition 2.1.11 in Halvorson.›
lemma identity_distributes_across_composition_dual:
  assumes f_type: "f : A → B" and g_type: "g : B → C"
  shows "(g  ∘⇩c f) ⨝⇩f id X = (g ⨝⇩f id X) ∘⇩c (f ⨝⇩f id X)"
proof - 
  from cfunc_bowtie_prod_unique
  have uniqueness: "∀h. h : A ∐  X → C ∐ X ∧
    h ∘⇩c left_coproj A X  = left_coproj C X ∘⇩c (g ∘⇩c f) ∧
    h ∘⇩c right_coproj A X = right_coproj C X ∘⇩c  id(X) ⟶
    h =  (g ∘⇩c f) ⨝⇩f  id⇩c X"
    using assms by (typecheck_cfuncs, simp add: cfunc_bowtie_prod_unique)

  have left_eq: " ((g ⨝⇩f id⇩c X) ∘⇩c (f ⨝⇩f id⇩c X)) ∘⇩c left_coproj A X = left_coproj C X ∘⇩c (g  ∘⇩c f)"
    by (typecheck_cfuncs, smt comp_associative2 left_coproj_cfunc_bowtie_prod left_proj_type assms)
  have right_eq: " ((g ⨝⇩f id⇩c X) ∘⇩c (f ⨝⇩f id⇩c X)) ∘⇩c right_coproj A X = right_coproj C X ∘⇩c id X"
    by(typecheck_cfuncs, smt comp_associative2 id_right_unit2 right_coproj_cfunc_bowtie_prod right_proj_type assms)

  show ?thesis
    using assms left_eq right_eq uniqueness by (typecheck_cfuncs, auto)
qed

lemma coproduct_of_beta:
  "β⇘X⇙ ⨿ β⇘Y⇙ = β⇘X∐Y⇙"
  by (metis (full_types) cfunc_coprod_unique left_proj_type right_proj_type terminal_func_comp terminal_func_type)

lemma cfunc_bowtieprod_comp_cfunc_coprod:
  assumes a_type: "a : Y → Z" and b_type: "b : W → Z"
  assumes f_type: "f : X → Y" and g_type: "g : V → W"
  shows "(a ⨿ b) ∘⇩c (f ⨝⇩f g) = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
proof - 
  from cfunc_bowtie_prod_unique have uniqueness:
    "∀h. h : X ∐ V → Z ∧ h ∘⇩c left_coproj X V   = a ∘⇩c f ∧ h ∘⇩c right_coproj X V  = b ∘⇩c g ⟶ 
      h = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
    using assms comp_type by (metis (full_types) cfunc_coprod_unique) 

  have left_eq: "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ∘⇩c f)"
  proof - 
    have "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ⨿ b) ∘⇩c (f ⨝⇩f g)  ∘⇩c left_coproj X V"
      using assms by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = (a ⨿ b)  ∘⇩c left_coproj Y W ∘⇩c f"
      using f_type g_type left_coproj_cfunc_bowtie_prod by auto
    also have "... = ((a ⨿ b)  ∘⇩c left_coproj Y W) ∘⇩c f"
      using a_type assms(2) cfunc_type_def comp_associative f_type by (typecheck_cfuncs, auto)
    also have "... = (a ∘⇩c f)"
      using a_type b_type left_coproj_cfunc_coprod by presburger
    finally show  "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c left_coproj X V = (a ∘⇩c f)".
  qed

  have right_eq: "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (b ∘⇩c g)"
  proof - 
    have "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (a ⨿ b) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
      using assms by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = (a ⨿ b) ∘⇩c right_coproj Y W ∘⇩c g"
      using f_type g_type right_coproj_cfunc_bowtie_prod by auto
    also have "... = ((a ⨿ b) ∘⇩c right_coproj Y W) ∘⇩c g"
      using a_type assms(2) cfunc_type_def comp_associative g_type by (typecheck_cfuncs, auto)
    also have "... = (b ∘⇩c g)"
      using a_type b_type right_coproj_cfunc_coprod by auto
    finally show "(a ⨿ b ∘⇩c f ⨝⇩f g) ∘⇩c right_coproj X V = (b ∘⇩c g)".
  qed

  show "(a ⨿ b) ∘⇩c (f ⨝⇩f g) = (a ∘⇩c f) ⨿ (b ∘⇩c g)"
    using uniqueness left_eq right_eq assms
    by (typecheck_cfuncs, auto)
qed

lemma id_bowtie_prod: "id(X) ⨝⇩f id(Y) = id(X ∐ Y)"
  by (metis cfunc_bowtie_prod_def id_codomain id_coprod id_right_unit2 left_proj_type right_proj_type)

lemma cfunc_bowtie_prod_comp_cfunc_bowtie_prod:
  assumes "f : X → Y" "g : V → W" "x : Y → S" "y : W → T"
  shows "(x ⨝⇩f y) ∘⇩c (f ⨝⇩f g) = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
proof- 
  have "(x ⨝⇩f y) ∘⇩c ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g))
      = ((x ⨝⇩f y) ∘⇩c left_coproj Y W ∘⇩c f) ⨿ ((x ⨝⇩f y) ∘⇩c right_coproj Y W ∘⇩c g)"
    using assms by (typecheck_cfuncs, simp add: cfunc_coprod_comp)
  also have "... = (((x ⨝⇩f y) ∘⇩c left_coproj Y W) ∘⇩c f) ⨿ (((x ⨝⇩f y) ∘⇩c right_coproj Y W) ∘⇩c g)"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = ((left_coproj S T ∘⇩c x) ∘⇩c f) ⨿ ((right_coproj S T ∘⇩c y) ∘⇩c g)"
    using assms(3,4) left_coproj_cfunc_bowtie_prod right_coproj_cfunc_bowtie_prod by auto
  also have "... = (left_coproj S T ∘⇩c x ∘⇩c f) ⨿ (right_coproj S T ∘⇩c y ∘⇩c g)"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
    using assms cfunc_bowtie_prod_def cfunc_type_def codomain_comp by auto
  ultimately show "(x ⨝⇩f y) ∘⇩c (f ⨝⇩f g) = (x ∘⇩c f) ⨝⇩f (y ∘⇩c g)"
    using assms(1,2) cfunc_bowtie_prod_def2 by auto
qed

lemma cfunc_bowtieprod_epi:
  assumes f_type[type_rule]: "f : X → Y" and g_type[type_rule]: "g : V → W"
  assumes f_epi: "epimorphism f" and g_epi: "epimorphism g"
  shows "epimorphism (f ⨝⇩f g)"
proof (typecheck_cfuncs, unfold epimorphism_def3, clarify)
  fix x y A
  assume x_type: "x: Y ∐ W → A"
  assume y_type: "y: Y ∐ W → A"
  assume eqs: "x ∘⇩c f ⨝⇩f g = y ∘⇩c f ⨝⇩f g"

  obtain x1 x2 where x_expand: "x = x1 ⨿ x2" and x1_x2_type: "x1 : Y → A" "x2 : W → A"
    using coprod_decomp x_type by blast
  obtain y1 y2 where y_expand: "y = y1 ⨿ y2" and y1_y2_type: "y1 : Y → A" "y2 : W → A"
    using coprod_decomp y_type by blast

  have "(x1 = y1) ∧ (x2 = y2)"
  proof
    have "x1 ∘⇩c f = ((x1 ⨿ x2) ∘⇩c left_coproj Y W) ∘⇩c f"
      using x1_x2_type left_coproj_cfunc_coprod by auto 
    also have "... = (x1 ⨿ x2) ∘⇩c left_coproj Y W ∘⇩c f"
      using assms comp_associative2 x_expand x_type by (typecheck_cfuncs, auto)
    also have "... = (x1 ⨿ x2) ∘⇩c (f ⨝⇩f g) ∘⇩c left_coproj X V"
      using left_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
    also have "... = (y1 ⨿ y2) ∘⇩c (f ⨝⇩f g) ∘⇩c left_coproj X V"
      using assms cfunc_type_def comp_associative eqs x_expand x_type y_expand y_type by (typecheck_cfuncs, auto)
    also have "... = (y1 ⨿ y2) ∘⇩c left_coproj Y W ∘⇩c f"
      using assms by (typecheck_cfuncs, simp add: left_coproj_cfunc_bowtie_prod)
    also have "... = ((y1 ⨿ y2) ∘⇩c left_coproj Y W) ∘⇩c f"
      using assms comp_associative2 y_expand y_type by (typecheck_cfuncs, blast)
    also have "... = y1 ∘⇩c f"
      using y1_y2_type left_coproj_cfunc_coprod by auto 
    ultimately show "x1 = y1"
      using epimorphism_def3 f_epi f_type x1_x2_type(1) y1_y2_type(1) by fastforce
  next
    have "x2 ∘⇩c g = ((x1 ⨿ x2) ∘⇩c right_coproj Y W) ∘⇩c g"
      using x1_x2_type right_coproj_cfunc_coprod by auto 
    also have "... = (x1 ⨿ x2) ∘⇩c right_coproj Y W ∘⇩c g"
      using assms comp_associative2 x_expand x_type by (typecheck_cfuncs, auto)
    also have "... = (x1 ⨿ x2) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
      using right_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
    also have "... = (y1 ⨿ y2) ∘⇩c (f ⨝⇩f g) ∘⇩c right_coproj X V"
      using assms cfunc_type_def comp_associative eqs x_expand x_type y_expand y_type by (typecheck_cfuncs, auto)
    also have "... = (y1 ⨿ y2) ∘⇩c right_coproj Y W ∘⇩c g"
      using assms by (typecheck_cfuncs, simp add: right_coproj_cfunc_bowtie_prod)
    also have "... = ((y1 ⨿ y2) ∘⇩c right_coproj Y W) ∘⇩c g"
      using assms comp_associative2 y_expand y_type by (typecheck_cfuncs, blast)
    also have "... = y2 ∘⇩c g"
      using right_coproj_cfunc_coprod y1_y2_type(1) y1_y2_type(2) by auto
    ultimately show "x2 = y2"
      using epimorphism_def3 g_epi g_type x1_x2_type(2) y1_y2_type(2) by fastforce
  qed
  then show "x = y"
    by (simp add: x_expand y_expand)
qed

lemma cfunc_bowtieprod_inj:
  assumes type_assms: "f : X → Y" "g : V → W"
  assumes f_epi: "injective f" and g_epi: "injective g"
  shows "injective (f ⨝⇩f g)"
  unfolding injective_def
proof(clarify)
  fix z1 z2 
  assume x_type: "z1 ∈⇩c domain (f ⨝⇩f g)"
  assume y_type: "z2 ∈⇩c domain (f ⨝⇩f g)"
  assume eqs: "(f ⨝⇩f g) ∘⇩c z1 = (f ⨝⇩f g) ∘⇩c z2"

  have f_bowtie_g_type: "(f ⨝⇩f g) : X ∐ V → Y ∐ W"
    by (simp add: cfunc_bowtie_prod_type type_assms(1) type_assms(2))

  have x_type2: "z1 ∈⇩c X ∐ V"
    using cfunc_type_def f_bowtie_g_type x_type by auto
  have y_type2: "z2 ∈⇩c X ∐ V"
    using cfunc_type_def f_bowtie_g_type y_type by auto

  have z1_decomp: "(∃ x1. (x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1))
      ∨  (∃ y1. (y1 ∈⇩c V ∧ z1 = right_coproj X V ∘⇩c y1))"
    by (simp add: coprojs_jointly_surj x_type2)

  have z2_decomp: "(∃ x2. (x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2))
      ∨  (∃ y2. (y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2))"
    by (simp add: coprojs_jointly_surj y_type2)

  show "z1 = z2"
  proof(cases "∃ x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1")
    assume case1: "∃x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
    obtain x1 where x1_def: "x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
          using case1 by blast
    show "z1 = z2"
    proof(cases "∃ x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2")
      assume caseA: "∃x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
      show "z1 = z2"
      proof - 
        obtain x2 where x2_def: "x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
          using caseA by blast
        have "x1 = x2"
        proof - 
          have "left_coproj Y W ∘⇩c f  ∘⇩c x1  = (left_coproj Y W ∘⇩c f) ∘⇩c x1"
            using cfunc_type_def comp_associative left_proj_type type_assms(1) x1_def by auto            
          also have "... = 
                (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x1"
            using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
          also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x1"
            using comp_associative2 type_assms x1_def by (typecheck_cfuncs, fastforce)
          also have "... = (f ⨝⇩f g) ∘⇩c z1"
            using cfunc_bowtie_prod_def2 type_assms x1_def by auto
          also have "... = (f ⨝⇩f g) ∘⇩c z2"
            by (meson eqs)
          also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x2"
            using cfunc_bowtie_prod_def2 type_assms(1) type_assms(2) x2_def by auto
          also have "... = ((((left_coproj Y W) ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x2"
            by (typecheck_cfuncs, meson comp_associative2 type_assms(1) type_assms(2) x2_def)
          also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x2"
            using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
          also have "... = left_coproj Y W ∘⇩c f  ∘⇩c x2"
            by (metis comp_associative2 left_proj_type type_assms(1) x2_def)
          ultimately have "f  ∘⇩c x1 = f  ∘⇩c x2"
            using cfunc_type_def left_coproj_are_monomorphisms
            left_proj_type monomorphism_def type_assms(1) x1_def x2_def by (typecheck_cfuncs,auto)
          then show "x1 = x2"
            by (metis cfunc_type_def f_epi injective_def type_assms(1) x1_def x2_def)
        qed
        then show "z1 = z2"
          by (simp add: x1_def x2_def)
      qed
    next 
      assume caseB: "∄x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
      then obtain y2 where y2_def: "(y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2)"
        using z2_decomp by blast
      have "left_coproj Y W ∘⇩c f  ∘⇩c x1  = (left_coproj Y W ∘⇩c f) ∘⇩c x1"
            using cfunc_type_def comp_associative left_proj_type type_assms(1) x1_def by auto            
      also have "... = 
            (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x1"
        using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
      also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x1"
        using comp_associative2 type_assms(1,2) x1_def by (typecheck_cfuncs, fastforce)
      also have "... = (f ⨝⇩f g) ∘⇩c z1"
        using cfunc_bowtie_prod_def2 type_assms x1_def by auto
      also have "... = (f ⨝⇩f g) ∘⇩c z2"
        by (meson eqs)
      also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y2"
        using cfunc_bowtie_prod_def2 type_assms y2_def by auto
      also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y2"
        by (typecheck_cfuncs, meson comp_associative2 type_assms y2_def)
      also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y2"
        using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
      also have "... = right_coproj Y W ∘⇩c g  ∘⇩c y2"
        using comp_associative2 type_assms(2) y2_def by (typecheck_cfuncs, auto)
      ultimately have False
        using comp_type coproducts_disjoint type_assms x1_def y2_def by auto
      then show "z1 = z2"
        by simp
    qed
  next
    assume case2: "∄x1. x1 ∈⇩c X ∧ z1 = left_coproj X V ∘⇩c x1"
    then obtain y1 where y1_def: "y1 ∈⇩c V ∧ z1 = right_coproj X V ∘⇩c y1"
      using z1_decomp by blast
    show "z1 = z2"
    proof(cases "∃ x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2")
      assume caseA: "∃x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
      show "z1 = z2"
      proof - 
        obtain x2 where x2_def: "x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
          using caseA by blast
        have "left_coproj Y W ∘⇩c f  ∘⇩c x2  = (left_coproj Y W ∘⇩c f) ∘⇩c x2"
          using comp_associative2 type_assms(1) x2_def by (typecheck_cfuncs, auto)
        also have "... =
              (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V) ∘⇩c x2"
          using cfunc_bowtie_prod_def2 left_coproj_cfunc_bowtie_prod type_assms by auto
        also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c left_coproj X V ∘⇩c x2"
          using comp_associative2 type_assms x2_def by (typecheck_cfuncs, fastforce)
        also have "... = (f ⨝⇩f g) ∘⇩c z2"
          using cfunc_bowtie_prod_def2 type_assms x2_def by auto
        also have "... = (f ⨝⇩f g) ∘⇩c z1"
          by (simp add: eqs)
        also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y1"
          using cfunc_bowtie_prod_def2 type_assms y1_def by auto
        also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y1"
          by (typecheck_cfuncs, meson comp_associative2 type_assms y1_def)
        also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y1"
          using right_coproj_cfunc_coprod type_assms  by (typecheck_cfuncs, fastforce)
        also have "... = right_coproj Y W ∘⇩c g  ∘⇩c y1"
          using comp_associative2 type_assms(2) y1_def by (typecheck_cfuncs, auto)
        ultimately have False
          using comp_type coproducts_disjoint type_assms x2_def y1_def by auto
        then show "z1 = z2"
          by simp
      qed
    next
      assume caseB: "∄x2. x2 ∈⇩c X ∧ z2 = left_coproj X V ∘⇩c x2"
      then obtain y2 where y2_def: "(y2 ∈⇩c V ∧ z2 = right_coproj X V ∘⇩c y2)"
        using z2_decomp by blast
        have "y1 = y2"
        proof - 
          have "right_coproj Y W ∘⇩c g  ∘⇩c y1  = (right_coproj Y W ∘⇩c g) ∘⇩c y1"
            using comp_associative2 type_assms(2) y1_def by (typecheck_cfuncs, auto)
          also have "... =
                (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y1"
            using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
          also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y1"
            using comp_associative2 type_assms  y1_def by (typecheck_cfuncs, fastforce)
          also have "... = (f ⨝⇩f g) ∘⇩c z1"
            using cfunc_bowtie_prod_def2 type_assms y1_def by auto
          also have "... = (f ⨝⇩f g) ∘⇩c z2"
            by (meson eqs)
          also have "... = ((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V ∘⇩c y2"
            using cfunc_bowtie_prod_def2 type_assms y2_def by auto
          also have "... = (((left_coproj Y W ∘⇩c f) ⨿ (right_coproj Y W ∘⇩c g)) ∘⇩c right_coproj X V) ∘⇩c y2"
            by (typecheck_cfuncs, meson comp_associative2 type_assms  y2_def)
          also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y2"
            using right_coproj_cfunc_coprod type_assms by (typecheck_cfuncs, fastforce)
          also have "... = right_coproj Y W ∘⇩c g  ∘⇩c y2"
            using comp_associative2 type_assms(2) y2_def by (typecheck_cfuncs, auto)
          ultimately have "g  ∘⇩c y1 = g  ∘⇩c y2"
            using  cfunc_type_def right_coproj_are_monomorphisms
            right_proj_type monomorphism_def type_assms(2) y1_def y2_def by (typecheck_cfuncs,auto)
          then show "y1 = y2"
            by (metis cfunc_type_def g_epi injective_def type_assms(2) y1_def y2_def)
        qed
        then show "z1 = z2"
          by (simp add: y1_def y2_def)
      qed
   qed
 qed

lemma cfunc_bowtieprod_inj_converse:
  assumes type_assms: "f : X → Y" "g : Z → W"
  assumes inj_f_bowtie_g: "injective (f ⨝⇩f g)"
  shows "injective f ∧ injective g"
  unfolding injective_def
proof(safe)
  fix x y 
  assume x_type: "x ∈⇩c domain f" 
  assume y_type: "y ∈⇩c domain f"
  assume eqs:    "f ∘⇩c x = f ∘⇩c y"

  have x_type2: "x ∈⇩c X"
    using cfunc_type_def type_assms(1) x_type by auto
  have y_type2: "y ∈⇩c X"
    using cfunc_type_def type_assms(1) y_type by auto
  have fg_bowtie_tyepe: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
    using assms by typecheck_cfuncs
  have lift: "(f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c y"
  proof - 
    have "(f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
      using x_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
    also have  "... =  (left_coproj Y W ∘⇩c f) ∘⇩c x"
      using left_coproj_cfunc_bowtie_prod type_assms by auto
    also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
      using x_type2 comp_associative2 type_assms(1) by (typecheck_cfuncs, auto)
    also have "... = left_coproj Y W ∘⇩c f ∘⇩c y"
      by (simp add: eqs)
    also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c y"
      using y_type2 comp_associative2 type_assms(1) by (typecheck_cfuncs, auto)
    also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c y"
      using left_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
    also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c y"
      using y_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
    finally show ?thesis.
  qed
  then have "monomorphism (f ⨝⇩f g)"
    using inj_f_bowtie_g injective_imp_monomorphism by auto
  then have "left_coproj X Z  ∘⇩c x = left_coproj X Z ∘⇩c y"
    by (typecheck_cfuncs, metis cfunc_type_def fg_bowtie_tyepe inj_f_bowtie_g injective_def lift x_type2 y_type2)
  then show "x = y"
    using x_type2 y_type2 cfunc_type_def left_coproj_are_monomorphisms left_proj_type monomorphism_def by auto
next
  fix x y 
  assume x_type: "x ∈⇩c domain g" 
  assume y_type: "y ∈⇩c domain g"
  assume eqs:    "g ∘⇩c x = g ∘⇩c y"

  have x_type2: "x ∈⇩c Z"
    using cfunc_type_def type_assms(2) x_type by auto
  have y_type2: "y ∈⇩c Z"
    using cfunc_type_def type_assms(2) y_type by auto
  have fg_bowtie_tyepe: "f ⨝⇩f g : X ∐ Z → Y ∐ W"
    using assms by typecheck_cfuncs
  have lift: "(f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c x = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c y"
  proof - 
    have "(f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c x = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c x"
      using x_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
    also have  "... =  (right_coproj Y W ∘⇩c g) ∘⇩c x"
      using right_coproj_cfunc_bowtie_prod type_assms by auto
    also have "... = right_coproj Y W ∘⇩c g ∘⇩c x"
      using x_type2 comp_associative2 type_assms(2) by (typecheck_cfuncs, auto)
    also have "... = right_coproj Y W ∘⇩c g ∘⇩c y"
      by (simp add: eqs)
    also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c y"
      using y_type2 comp_associative2 type_assms(2) by (typecheck_cfuncs, auto)
    also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c y"
      using right_coproj_cfunc_bowtie_prod type_assms(1) type_assms(2) by auto
    also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c y"
      using y_type2 comp_associative2 fg_bowtie_tyepe by (typecheck_cfuncs, auto)
    finally show ?thesis.
  qed
  then have "monomorphism (f ⨝⇩f g)"
    using inj_f_bowtie_g injective_imp_monomorphism by auto
  then have "right_coproj X Z ∘⇩c x = right_coproj X Z ∘⇩c y"
    by (typecheck_cfuncs, metis cfunc_type_def fg_bowtie_tyepe inj_f_bowtie_g injective_def lift x_type2 y_type2)
  then show "x = y"
    using x_type2 y_type2 cfunc_type_def right_coproj_are_monomorphisms right_proj_type monomorphism_def by auto
qed

lemma cfunc_bowtieprod_iso:
  assumes type_assms: "f : X → Y" "g : V → W"
  assumes f_iso: "isomorphism f" and g_iso: "isomorphism g"
  shows "isomorphism (f ⨝⇩f g)"
  by (typecheck_cfuncs, meson cfunc_bowtieprod_epi cfunc_bowtieprod_inj epi_mon_is_iso f_iso g_iso injective_imp_monomorphism iso_imp_epi_and_monic monomorphism_imp_injective singletonI assms)

lemma cfunc_bowtieprod_surj_converse:
  assumes type_assms: "f : X → Y" "g : Z → W"
  assumes inj_f_bowtie_g: "surjective (f ⨝⇩f g)"
  shows "surjective f ∧ surjective g"
  unfolding surjective_def
proof(safe)
  fix y 
  assume y_type: "y ∈⇩c codomain f" 
  then have y_type2: "y ∈⇩c Y"
    using cfunc_type_def type_assms(1) by auto
  then have coproj_y_type: "left_coproj Y W ∘⇩c y ∈⇩c Y ∐ W" 
    by typecheck_cfuncs
  have fg_type: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
    using assms by typecheck_cfuncs
  obtain xz where xz_def: "xz ∈⇩c X ∐ Z ∧ (f ⨝⇩f g) ∘⇩c xz =  left_coproj Y W ∘⇩c y"
    using fg_type y_type2 cfunc_type_def inj_f_bowtie_g surjective_def by (typecheck_cfuncs, auto)
  then have xz_form: "(∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz) ∨  
                      (∃ z. z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz)"
    using coprojs_jointly_surj xz_def by (typecheck_cfuncs, blast)
  show "∃ x. x ∈⇩c domain f ∧ f ∘⇩c x = y"
  proof(cases "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz")
    assume "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
    then obtain x where x_def: "x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
      by blast
    have "f ∘⇩c x = y"
    proof - 
      have "left_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
        by (simp add: xz_def)
      also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x"
        by (simp add: x_def)
      also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
        using  comp_associative2 fg_type x_def by (typecheck_cfuncs, auto)
      also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x"
        using left_coproj_cfunc_bowtie_prod type_assms by auto
      also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
        using comp_associative2 type_assms(1) x_def by (typecheck_cfuncs, auto)
      ultimately show "f ∘⇩c x = y"
        using type_assms(1) x_def y_type2  
        by (typecheck_cfuncs, metis cfunc_type_def left_coproj_are_monomorphisms left_proj_type monomorphism_def x_def)
    qed
    then show ?thesis
      using cfunc_type_def type_assms(1) x_def by auto
 next
   assume "∄x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
   then obtain z where z_def: "z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz"
     using xz_form by blast
   have False
    proof - 
      have "left_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
        by (simp add: xz_def)         
      also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c z"
        by (simp add: z_def)
      also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c z"
        using comp_associative2 fg_type z_def by (typecheck_cfuncs, auto)
      also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c z"
        using right_coproj_cfunc_bowtie_prod type_assms by auto
      also have "... = right_coproj Y W ∘⇩c g ∘⇩c z"
        using comp_associative2 type_assms(2) z_def by (typecheck_cfuncs, auto)
      ultimately show False
        using comp_type coproducts_disjoint type_assms(2) y_type2 z_def by auto
   qed
   then show ?thesis
     by simp
 qed
next
  fix y
  assume y_type: "y ∈⇩c codomain g"
  then have y_type2: "y ∈⇩c W"
    using cfunc_type_def type_assms(2) by auto 
  then have coproj_y_type: "(right_coproj Y W) ∘⇩c y ∈⇩c (Y ∐ W)" 
    using cfunc_type_def comp_type right_proj_type type_assms(2) by auto
  have fg_type: "(f ⨝⇩f g) : X ∐ Z → Y ∐ W"
    by (simp add: cfunc_bowtie_prod_type type_assms)
  obtain xz where xz_def: "xz ∈⇩c X ∐ Z ∧ (f ⨝⇩f g) ∘⇩c xz = right_coproj Y W ∘⇩c y"
    using fg_type y_type2 cfunc_type_def inj_f_bowtie_g surjective_def by (typecheck_cfuncs, auto)
  then have xz_form: "(∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz) ∨  
                      (∃ z. z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz)"
    using coprojs_jointly_surj xz_def by (typecheck_cfuncs, blast)
  show "∃x. x ∈⇩c domain g ∧ g ∘⇩c x = y"
  proof(cases "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz")
    assume "∃ x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
    then obtain x where x_def: "x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
      by blast
    have False
    proof - 
      have "right_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
        by (simp add: xz_def)
      also have "... = (f ⨝⇩f g) ∘⇩c left_coproj X Z ∘⇩c x"
        by (simp add: x_def)
      also have "... = ((f ⨝⇩f g) ∘⇩c left_coproj X Z) ∘⇩c x"
        using  comp_associative2 fg_type x_def by (typecheck_cfuncs, auto)
      also have "... = (left_coproj Y W ∘⇩c f) ∘⇩c x"
        using left_coproj_cfunc_bowtie_prod type_assms by auto
      also have "... = left_coproj Y W ∘⇩c f ∘⇩c x"
        using comp_associative2 type_assms(1) x_def by (typecheck_cfuncs, auto)
      ultimately show False
        by (metis comp_type coproducts_disjoint type_assms(1) x_def y_type2)
    qed
    then show ?thesis
      by simp
next
  assume "∄x. x ∈⇩c X ∧ left_coproj X Z ∘⇩c x = xz"
  then obtain z where z_def: "z ∈⇩c Z ∧ right_coproj X Z ∘⇩c z = xz"
    using xz_form by blast
  have "g ∘⇩c z = y"
    proof - 
      have "right_coproj Y W ∘⇩c y = (f ⨝⇩f g) ∘⇩c xz"
        by (simp add: xz_def)         
      also have "... = (f ⨝⇩f g) ∘⇩c right_coproj X Z ∘⇩c z"
        by (simp add: z_def)
      also have "... = ((f ⨝⇩f g) ∘⇩c right_coproj X Z) ∘⇩c z"
        using comp_associative2 fg_type z_def by (typecheck_cfuncs, auto)
      also have "... = (right_coproj Y W ∘⇩c g) ∘⇩c z"
        using right_coproj_cfunc_bowtie_prod type_assms by auto
      also have "... = right_coproj Y W ∘⇩c g ∘⇩c z"
        using comp_associative2 type_assms(2) z_def by (typecheck_cfuncs, auto)
      ultimately show ?thesis
        by (metis cfunc_type_def codomain_comp monomorphism_def 
           right_coproj_are_monomorphisms right_proj_type type_assms(2) y_type2 z_def)
    qed
    then show ?thesis
      using cfunc_type_def type_assms(2) z_def by auto
 qed
qed

subsection ‹Boolean Cases›

definition case_bool :: "cfunc" where
  "case_bool = (THE f. f : Ω → (𝟭 ∐ 𝟭) ∧  
    (𝗍 ⨿ 𝖿) ∘⇩c f = id Ω ∧ f ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭))"

lemma case_bool_def2:
  "case_bool : Ω → (𝟭 ∐ 𝟭) ∧  
    (𝗍 ⨿ 𝖿) ∘⇩c case_bool = id Ω ∧ case_bool ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭)"
  unfolding case_bool_def
proof (rule theI', safe)
  show "∃x. x : Ω → 𝟭 ∐ 𝟭 ∧ 𝗍 ⨿ 𝖿 ∘⇩c x = id⇩c Ω ∧ x ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)"
    unfolding isomorphism_def
    using isomorphism_def3 truth_value_set_iso_1u1 by (typecheck_cfuncs, blast)
next
  fix x y
  assume x_type[type_rule]: "x : Ω → 𝟭 ∐ 𝟭" and y_type[type_rule]: "y : Ω → 𝟭 ∐ 𝟭"
  assume x_left_inv: "𝗍 ⨿ 𝖿 ∘⇩c x = id⇩c Ω"
  assume "x ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)" "y ∘⇩c 𝗍 ⨿ 𝖿 = id⇩c (𝟭 ∐ 𝟭)"
  then have "x ∘⇩c 𝗍 ⨿ 𝖿 = y ∘⇩c 𝗍 ⨿ 𝖿"
    by auto
  then have "x ∘⇩c 𝗍 ⨿ 𝖿 ∘⇩c x = y ∘⇩c 𝗍 ⨿ 𝖿 ∘⇩c x"
    by (typecheck_cfuncs, auto simp add: comp_associative2)
  then show "x = y"
    using id_right_unit2 x_left_inv by (typecheck_cfuncs_prems, auto)
qed

lemma case_bool_type[type_rule]: 
  "case_bool : Ω → 𝟭 ∐ 𝟭"
  using case_bool_def2 by auto

lemma case_bool_true_coprod_false:
  "case_bool ∘⇩c (𝗍 ⨿ 𝖿) = id (𝟭 ∐ 𝟭)"
  using case_bool_def2 by auto

lemma true_coprod_false_case_bool:
  "(𝗍 ⨿ 𝖿) ∘⇩c case_bool = id Ω"
  using case_bool_def2 by auto

lemma case_bool_iso:
  "isomorphism case_bool"
  using case_bool_def2 unfolding isomorphism_def
  by (intro exI[where x="𝗍 ⨿ 𝖿"], typecheck_cfuncs, auto simp add: cfunc_type_def)

lemma case_bool_true_and_false:
  "(case_bool ∘⇩c 𝗍 = left_coproj 𝟭 𝟭) ∧ (case_bool ∘⇩c 𝖿 = right_coproj 𝟭 𝟭)"
proof -
  have "(left_coproj 𝟭 𝟭) ⨿  (right_coproj 𝟭 𝟭) = id(𝟭 ∐ 𝟭)"
    by (simp add: id_coprod)
  also have "... = case_bool ∘⇩c (𝗍 ⨿ 𝖿)"
    by (simp add: case_bool_def2)
  also have "...  = (case_bool ∘⇩c 𝗍) ⨿ (case_bool ∘⇩c 𝖿)"
    using case_bool_def2 cfunc_coprod_comp false_func_type true_func_type by auto
  ultimately show ?thesis 
    using coprod_eq2 by (typecheck_cfuncs, auto)
qed

lemma case_bool_true:
  "case_bool ∘⇩c 𝗍 = left_coproj 𝟭 𝟭"
  by (simp add: case_bool_true_and_false)

lemma case_bool_false:
  "case_bool ∘⇩c 𝖿 = right_coproj 𝟭 𝟭"
  by (simp add: case_bool_true_and_false)

lemma coprod_case_bool_true:
  assumes "x1 ∈⇩c X"
  assumes "x2 ∈⇩c X"
  shows   "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝗍 = x1"
proof - 
  have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝗍 = (x1 ⨿ x2) ∘⇩c case_bool ∘⇩c 𝗍"
    using assms by (typecheck_cfuncs , simp add: comp_associative2)
  also have "... = (x1 ⨿ x2) ∘⇩c  left_coproj 𝟭 𝟭"
    using assms case_bool_true by presburger
  also have "... = x1"
    using assms left_coproj_cfunc_coprod by force
  finally show ?thesis.
qed

lemma coprod_case_bool_false:
  assumes "x1 ∈⇩c X"
  assumes "x2 ∈⇩c X"
  shows   "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝖿 = x2"
proof - 
  have "(x1 ⨿ x2 ∘⇩c case_bool) ∘⇩c 𝖿 = (x1 ⨿ x2) ∘⇩c case_bool ∘⇩c 𝖿"
    using assms by (typecheck_cfuncs , simp add: comp_associative2)
  also have "... = (x1 ⨿ x2) ∘⇩c  right_coproj 𝟭 𝟭"
    using assms case_bool_false by presburger
  also have "... = x2"
    using assms right_coproj_cfunc_coprod by force
  finally show ?thesis.
qed

subsection ‹Distribution of Products over Coproducts›

subsubsection ‹Factor Product over Coproduct on Left›

definition factor_prod_coprod_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "factor_prod_coprod_left A B C = (id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)"

lemma factor_prod_coprod_left_type[type_rule]:
  "factor_prod_coprod_left A B C : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
  unfolding factor_prod_coprod_left_def by typecheck_cfuncs

lemma factor_prod_coprod_left_ap_left:
  assumes "a ∈⇩c A" "b ∈⇩c B"
  shows "factor_prod_coprod_left A B C ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, b⟩ = ⟨a, left_coproj B C ∘⇩c b⟩"
  unfolding factor_prod_coprod_left_def using assms 
  by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 left_coproj_cfunc_coprod)

lemma factor_prod_coprod_left_ap_right:
  assumes "a ∈⇩c A" "c ∈⇩c C"
  shows "factor_prod_coprod_left A B C ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, c⟩ = ⟨a, right_coproj B C ∘⇩c c⟩"
  unfolding factor_prod_coprod_left_def using assms 
  by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 right_coproj_cfunc_coprod)

lemma factor_prod_coprod_left_mono:
  "monomorphism (factor_prod_coprod_left A B C)"
proof -
  obtain φ where φ_def: "φ = (id A  ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)" and
                 φ_type[type_rule]: "φ : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
    by (typecheck_cfuncs, simp)

  have injective: "injective(φ)"
    unfolding injective_def
  proof(clarify) 
    fix x y
    assume x_type: "x ∈⇩c domain φ"
    assume y_type: "y ∈⇩c domain φ"
    assume equal: "φ ∘⇩c x = φ ∘⇩c y"

    have x_type[type_rule]: "x ∈⇩c (A ×⇩c B) ∐ (A ×⇩c C)"
      using cfunc_type_def φ_type x_type by auto
    then have x_form: "(∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')
      ∨  (∃ x'. x' ∈⇩c A ×⇩c C ∧ x = (right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')"
      by (simp add: coprojs_jointly_surj)
    have y_type[type_rule]: "y ∈⇩c (A ×⇩c B) ∐ (A ×⇩c C)"
      using cfunc_type_def φ_type y_type by auto
    then have y_form: "(∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y')
      ∨  (∃ y'. y' ∈⇩c A ×⇩c C ∧ y = (right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y')"
      by (simp add: coprojs_jointly_surj)
    
    show "x = y" 
    proof(cases "(∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x')")
      assume "∃ x'. x' ∈⇩c A ×⇩c B ∧ x = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c x'"
      then obtain x' where x'_def[type_rule]: "x' ∈⇩c A ×⇩c B" "x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
        by blast
      then have ab_exists: "∃ a b. a ∈⇩c A ∧ b ∈⇩c B ∧ x' =⟨a,b⟩"
        using cart_prod_decomp by blast
      then obtain a b where ab_def[type_rule]: "a ∈⇩c A" "b ∈⇩c B"  "x' =⟨a,b⟩"
        by blast
      show "x = y"  
      proof(cases "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y'")
        assume "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = (left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c y'"
        then obtain y' where y'_def: "y' ∈⇩c A ×⇩c B" "y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
          by blast
        then have ab_exists: "∃ a' b'. a' ∈⇩c A ∧ b' ∈⇩c B ∧ y' =⟨a',b'⟩"
          using cart_prod_decomp by blast
        then obtain a' b' where a'b'_def[type_rule]: "a' ∈⇩c A" "b' ∈⇩c B" "y' =⟨a',b'⟩"
          by blast
        have equal_pair: "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩"
        proof - 
          have "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨id A ∘⇩c a, left_coproj B C ∘⇩c b⟩"
            using ab_def id_left_unit2 by force
          also have "... = (id A ×⇩f left_coproj B C)  ∘⇩c ⟨a, b⟩"
            by (smt ab_def cfunc_cross_prod_comp_cfunc_prod id_type left_proj_type)
          also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
            unfolding φ_def using  left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = φ ∘⇩c x"
            using ab_def comp_associative2 x'_def by (typecheck_cfuncs, fastforce)
          also have "... = φ ∘⇩c y"
            by (simp add: local.equal)
          also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', b'⟩"
            using a'b'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
          also have "... = (id A ×⇩f left_coproj B C)  ∘⇩c ⟨ a',  b'⟩"
            unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = ⟨id A ∘⇩c a', left_coproj B C ∘⇩c b'⟩"
            using a'b'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, auto)
          also have "... =  ⟨a', left_coproj B C ∘⇩c b'⟩"
            using a'b'_def id_left_unit2 by force
          finally show "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩".
        qed
        then have a_equal: "a = a' ∧ left_coproj B C ∘⇩c b = left_coproj B C ∘⇩c b'"
          using a'b'_def ab_def cart_prod_eq2 equal_pair by (typecheck_cfuncs, blast)
        then have b_equal: "b = b'"
          using a'b'_def a_equal ab_def left_coproj_are_monomorphisms left_proj_type monomorphism_def3 by blast
        then show "x = y"
          by (simp add: a'b'_def a_equal ab_def x'_def y'_def)
    next 
      assume "∄y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
      then obtain y' where y'_def: "y' ∈⇩c A ×⇩c C" "y = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
        using  y_form by blast
      then obtain a' c' where a'c'_def: "a' ∈⇩c A" "c' ∈⇩c C" "y' =⟨a',c'⟩"
        by (meson cart_prod_decomp)
      have equal_pair: "⟨a, (left_coproj B C) ∘⇩c b⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩"
      proof - 
        have "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨id A ∘⇩c a, left_coproj B C ∘⇩c b⟩"
          using ab_def id_left_unit2 by force
        also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨a, b⟩"
          by (smt ab_def cfunc_cross_prod_comp_cfunc_prod id_type left_proj_type)
        also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
          unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
        also have "... = φ ∘⇩c x"
          using ab_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
        also have "... = φ ∘⇩c y"
          by (simp add: local.equal)
        also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', c'⟩"
          using a'c'_def comp_associative2 y'_def by (typecheck_cfuncs, blast)
          also have "... = (id A ×⇩f right_coproj B C) ∘⇩c ⟨a', c'⟩"
          unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
        also have "... = ⟨id A ∘⇩c a', right_coproj B C ∘⇩c c'⟩"
          using a'c'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
        also have "... =  ⟨a', right_coproj B C ∘⇩c c'⟩"
          using a'c'_def id_left_unit2 by force
        finally show "⟨a, left_coproj B C ∘⇩c b⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩".
      qed        
      then have impossible: "left_coproj B C ∘⇩c b = right_coproj B C ∘⇩c c'"
        using a'c'_def ab_def element_pair_eq equal_pair by (typecheck_cfuncs, blast)
      then show "x = y"
        using a'c'_def ab_def coproducts_disjoint  by blast
    qed
  next
    assume "∄x'. x' ∈⇩c A ×⇩c B ∧ x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
    then obtain x' where x'_def: "x' ∈⇩c A ×⇩c C" "x = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c x'"
      using  x_form by blast
    then have ac_exists: "∃ a c. a ∈⇩c A ∧ c ∈⇩c C ∧ x' =⟨a,c⟩"
      using cart_prod_decomp by blast
    then obtain a c where ac_def: "a ∈⇩c A" "c ∈⇩c C" "x' =⟨a,c⟩"
      by blast
    show "x = y"  
    proof(cases "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'")
      assume "∃ y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
      then obtain y' where y'_def: "y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
        by blast
      then obtain a' b' where a'b'_def: "a' ∈⇩c A ∧ b' ∈⇩c B ∧ y' =⟨a',b'⟩"
        using cart_prod_decomp y'_def by blast
      have equal_pair: "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩"
      proof - 
        have "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨id(A) ∘⇩c a, right_coproj B C ∘⇩c c⟩"
          using ac_def id_left_unit2 by force
        also have "... = (id A ×⇩f right_coproj B C)  ∘⇩c ⟨a, c⟩"
          by (smt ac_def cfunc_cross_prod_comp_cfunc_prod id_type right_proj_type)
        also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
          unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
        also have "... = φ ∘⇩c x"
          using ac_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
        also have "... = φ ∘⇩c y"
          by (simp add: local.equal)
        also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', b'⟩"
          using a'b'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
          also have "... = (id A ×⇩f left_coproj B C) ∘⇩c ⟨a', b'⟩"
          unfolding φ_def using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
        also have "... = ⟨id A ∘⇩c a', left_coproj B C ∘⇩c b'⟩"
          using a'b'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
        also have "... =  ⟨a', left_coproj B C ∘⇩c b'⟩"
          using a'b'_def id_left_unit2 by force
        finally show "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', left_coproj B C ∘⇩c b'⟩".
      qed        
      then have impossible:  "right_coproj B C ∘⇩c c = left_coproj B C ∘⇩c b'"
          using a'b'_def ac_def cart_prod_eq2 equal_pair by (typecheck_cfuncs, blast)
        then show "x = y"
          using a'b'_def ac_def coproducts_disjoint by force
      next 
        assume "∄y'. y' ∈⇩c A ×⇩c B ∧ y = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
        then obtain y' where y'_def: "y' ∈⇩c (A ×⇩c C) ∧ y = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c y'"
          using  y_form by blast
        then obtain a' c' where a'c'_def: "a' ∈⇩c A" "c' ∈⇩c C" "y' =⟨a',c'⟩"
          using cart_prod_decomp by blast
        have equal_pair: "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩"
        proof - 
          have "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨id A ∘⇩c a, right_coproj B C ∘⇩c c⟩"
            using ac_def id_left_unit2 by force
          also have "... = (id A ×⇩f right_coproj B C)  ∘⇩c ⟨a,  c⟩"
            by (smt ac_def cfunc_cross_prod_comp_cfunc_prod id_type right_proj_type)
          also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
            unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = φ ∘⇩c x"
            using ac_def comp_associative2 φ_type x'_def by (typecheck_cfuncs, fastforce)
          also have "... = φ ∘⇩c y"
            by (simp add: local.equal)
          also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a', c'⟩"
            using a'c'_def comp_associative2 φ_type y'_def by (typecheck_cfuncs, blast)
          also have "... = (id A ×⇩f right_coproj B C)  ∘⇩c ⟨a',  c'⟩"
            unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = ⟨id A ∘⇩c a', right_coproj B C ∘⇩c c'⟩"
            using a'c'_def cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs,auto)
          also have "... =  ⟨a', right_coproj B C ∘⇩c c'⟩"
            using a'c'_def id_left_unit2 by force
          finally show "⟨a, right_coproj B C ∘⇩c c⟩ = ⟨a', right_coproj B C ∘⇩c c'⟩".            
        qed     
        then have a_equal: "a = a' ∧ right_coproj B C ∘⇩c c = right_coproj B C ∘⇩c c'"
          using a'c'_def ac_def element_pair_eq equal_pair by (typecheck_cfuncs, blast)
        then have c_equal: "c = c'" 
          using a'c'_def a_equal ac_def right_coproj_are_monomorphisms right_proj_type monomorphism_def3 by blast
        then show "x = y"
          by (simp add: a'c'_def a_equal ac_def x'_def y'_def)
      qed
    qed
  qed
  then show "monomorphism (factor_prod_coprod_left A B C)"
    using φ_def factor_prod_coprod_left_def injective_imp_monomorphism by fastforce
qed

lemma factor_prod_coprod_left_epi:
  "epimorphism (factor_prod_coprod_left A B C)"
proof -
  obtain φ where φ_def: "φ = (id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C)" and
                 φ_type[type_rule]: "φ : (A ×⇩c B) ∐ (A ×⇩c C) → A ×⇩c (B ∐ C)"
    by (typecheck_cfuncs, simp)
  have surjective: "surjective((id A ×⇩f left_coproj B C) ⨿ (id A ×⇩f right_coproj B C))"
    unfolding surjective_def
  proof(clarify)
    fix y 
    assume y_type: "y ∈⇩c codomain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
    then have y_type2: "y ∈⇩c A ×⇩c (B ∐ C)"
      using φ_def φ_type cfunc_type_def by auto
    then obtain a where a_def: "∃ bc. a ∈⇩c A ∧ bc ∈⇩c B ∐ C ∧ y = ⟨a,bc⟩"
      by (meson cart_prod_decomp)
    then obtain bc where bc_def: "bc ∈⇩c (B ∐ C) ∧ y = ⟨a,bc⟩"
      by blast
    have bc_form: "(∃ b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b) ∨ (∃ c. c ∈⇩c C ∧ bc = right_coproj B C ∘⇩c c)"
      by (simp add: bc_def coprojs_jointly_surj)
    have domain_is: "(A ×⇩c B) ∐ (A ×⇩c C) = domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
      by (typecheck_cfuncs, simp add: cfunc_type_def)
    show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
             (id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
    proof(cases "∃ b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b")
      assume case1: "∃b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
      then obtain b where b_def: "b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
        by blast
      then have ab_type: "⟨a, b⟩ ∈⇩c (A ×⇩c B)"
        using a_def b_def by (typecheck_cfuncs, blast)
      obtain x where x_def: "x = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, b⟩"
        by simp
      have x_type: "x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
        using ab_type cfunc_type_def codomain_comp domain_comp domain_is left_proj_type x_def by auto
      have y_def2: "y = ⟨a,left_coproj B C ∘⇩c b⟩"
        by (simp add: b_def bc_def)
      have "y = (id(A) ×⇩f left_coproj B C) ∘⇩c ⟨a,b⟩"
        using a_def b_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 y_def2 by (typecheck_cfuncs, auto)
      also have "... = (φ ∘⇩c left_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, b⟩"
        unfolding φ_def by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
      also have "... = φ ∘⇩c x"
        using φ_type x_def ab_type comp_associative2 by (typecheck_cfuncs, auto)
      ultimately show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
        (id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
        using φ_def x_type by auto
    next
      assume "∄b. b ∈⇩c B ∧ bc = left_coproj B C ∘⇩c b"
      then have case2: "∃ c. c ∈⇩c C ∧ bc = (right_coproj B C  ∘⇩c c)"
        using bc_form by blast
      then obtain c where c_def: "c ∈⇩c C ∧ bc = right_coproj B C  ∘⇩c c"
        by blast
      then have ac_type: "⟨a, c⟩ ∈⇩c (A ×⇩c C)"
        using a_def c_def by (typecheck_cfuncs, blast)
      obtain x where x_def: "x = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a, c⟩"
        by simp
      have x_type: "x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C))"
        using ac_type cfunc_type_def codomain_comp domain_comp domain_is right_proj_type x_def by auto
      have y_def2: "y = ⟨a,right_coproj B C ∘⇩c c⟩"
        by (simp add: c_def bc_def)
      have "y = (id(A) ×⇩f right_coproj B C) ∘⇩c ⟨a,c⟩"
        using a_def c_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 y_def2 by (typecheck_cfuncs, auto)
      also have "... = (φ ∘⇩c right_coproj (A ×⇩c B) (A ×⇩c C)) ∘⇩c ⟨a, c⟩"
        unfolding φ_def using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
      also have "... = φ ∘⇩c x"
        using φ_type x_def ac_type comp_associative2 by (typecheck_cfuncs, auto)
      ultimately show "∃x. x ∈⇩c domain ((id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C)) ∧
        (id⇩c A ×⇩f left_coproj B C) ⨿ (id⇩c A ×⇩f right_coproj B C) ∘⇩c x = y"
        using φ_def x_type by auto
    qed
  qed
  then show "epimorphism (factor_prod_coprod_left A B C)"
    by (simp add: factor_prod_coprod_left_def surjective_is_epimorphism)
qed

lemma dist_prod_coprod_iso:
  "isomorphism(factor_prod_coprod_left A B C)"
  by (simp add: factor_prod_coprod_left_epi factor_prod_coprod_left_mono epi_mon_is_iso)

text ‹The lemma below corresponds to Proposition 2.5.10 in Halvorson.›
lemma prod_distribute_coprod:
  "A ×⇩c (X ∐ Y) ≅ (A ×⇩c X) ∐ (A ×⇩c Y)"
  using dist_prod_coprod_iso factor_prod_coprod_left_type is_isomorphic_def isomorphic_is_symmetric by blast

subsubsection  ‹Distribute Product over Coproduct on Left›

definition dist_prod_coprod_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "dist_prod_coprod_left A B C = (THE f. f : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)
    ∧ f ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))
    ∧ factor_prod_coprod_left A B C ∘⇩c f = id (A ×⇩c (B ∐ C)))"

lemma dist_prod_coprod_left_def2:
  shows "dist_prod_coprod_left A B C : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)
    ∧ dist_prod_coprod_left A B C ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))
    ∧ factor_prod_coprod_left A B C ∘⇩c dist_prod_coprod_left A B C = id (A ×⇩c (B ∐ C))"
  unfolding dist_prod_coprod_left_def
proof (rule theI', safe)
  show "∃x. x : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C ∧
        x ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C) ∧
        factor_prod_coprod_left A B C ∘⇩c x = id⇩c (A ×⇩c B ∐ C)"
    using dist_prod_coprod_iso[where A=A, where B=B, where C=C] unfolding isomorphism_def
    by (typecheck_cfuncs, auto simp add: cfunc_type_def)
  then obtain inv where inv_type: "inv : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C" and
        inv_left: "inv ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)" and
        inv_right: "factor_prod_coprod_left A B C ∘⇩c inv = id⇩c (A ×⇩c B ∐ C)"
    by auto

  fix x y
  assume x_type: "x : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C"
  assume y_type: "y : A ×⇩c B ∐ C → (A ×⇩c B) ∐ A ×⇩c C"

  assume "x ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)"
    and "y ∘⇩c factor_prod_coprod_left A B C = id⇩c ((A ×⇩c B) ∐ A ×⇩c C)"
  then have "x ∘⇩c factor_prod_coprod_left A B C = y ∘⇩c factor_prod_coprod_left A B C"
    by auto
  then have "(x ∘⇩c factor_prod_coprod_left A B C) ∘⇩c inv = (y ∘⇩c factor_prod_coprod_left A B C) ∘⇩c inv"
    by auto
  then have "x ∘⇩c factor_prod_coprod_left A B C ∘⇩c inv = y ∘⇩c factor_prod_coprod_left A B C ∘⇩c inv"
    using inv_type x_type y_type by (typecheck_cfuncs, auto simp add: comp_associative2)
  then have "x ∘⇩c id⇩c (A ×⇩c B ∐ C) = y ∘⇩c id⇩c (A ×⇩c B ∐ C)"
    by (simp add: inv_right)
  then show "x = y"
    using id_right_unit2 x_type y_type by auto
qed

lemma dist_prod_coprod_left_type[type_rule]:
  "dist_prod_coprod_left A B C : A ×⇩c (B ∐ C) → (A ×⇩c B) ∐ (A ×⇩c C)"
  by (simp add: dist_prod_coprod_left_def2)

lemma dist_factor_prod_coprod_left:
  "dist_prod_coprod_left A B C ∘⇩c factor_prod_coprod_left A B C = id ((A ×⇩c B) ∐ (A ×⇩c C))"
  by (simp add: dist_prod_coprod_left_def2)

lemma factor_dist_prod_coprod_left:
  "factor_prod_coprod_left A B C ∘⇩c dist_prod_coprod_left A B C = id (A ×⇩c (B ∐ C))"
  by (simp add: dist_prod_coprod_left_def2)

lemma dist_prod_coprod_left_iso:
  "isomorphism(dist_prod_coprod_left A B C)"
  by (metis factor_dist_prod_coprod_left dist_prod_coprod_left_type dist_prod_coprod_iso factor_prod_coprod_left_type id_isomorphism id_right_unit2 id_type isomorphism_sandwich)

lemma dist_prod_coprod_left_ap_left:
  assumes "a ∈⇩c A" "b ∈⇩c B"
  shows "dist_prod_coprod_left A B C ∘⇩c ⟨a,left_coproj B C ∘⇩c b⟩ = left_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a,b⟩"
  using assms by (typecheck_cfuncs, smt comp_associative2 dist_prod_coprod_left_def2 factor_prod_coprod_left_ap_left factor_prod_coprod_left_type id_left_unit2)

lemma dist_prod_coprod_left_ap_right:
  assumes "a ∈⇩c A" "c ∈⇩c C"
  shows "dist_prod_coprod_left A B C ∘⇩c ⟨a,right_coproj B C ∘⇩c c⟩ = right_coproj (A ×⇩c B) (A ×⇩c C) ∘⇩c ⟨a,c⟩"
  using assms by (typecheck_cfuncs, smt comp_associative2 dist_prod_coprod_left_def2 factor_prod_coprod_left_ap_right factor_prod_coprod_left_type id_left_unit2)

subsubsection  ‹Factor Product over Coproduct on Right›

definition factor_prod_coprod_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "factor_prod_coprod_right A B C = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)"

lemma factor_prod_coprod_right_type[type_rule]:
  "factor_prod_coprod_right A B C : (A ×⇩c C) ∐ (B ×⇩c C) → (A ∐ B) ×⇩c C"
  unfolding factor_prod_coprod_right_def by typecheck_cfuncs

lemma factor_prod_coprod_right_ap_left:
  assumes "a ∈⇩c A" "c ∈⇩c C"
  shows "factor_prod_coprod_right A B C ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩) = ⟨left_coproj A B ∘⇩c a, c⟩"
proof -
  have "factor_prod_coprod_right A B C ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩)
    = (swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)) ∘⇩c (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩)"
    unfolding factor_prod_coprod_right_def by auto
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c ((swap A C ⨝⇩f swap B C) ∘⇩c left_coproj (A ×⇩c C) (B ×⇩c C)) ∘⇩c ⟨a, c⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap A C) ∘⇩c ⟨a, c⟩"
    using assms by (typecheck_cfuncs, auto simp add: left_coproj_cfunc_bowtie_prod)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap A C ∘⇩c ⟨a, c⟩"
    using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, a⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  also have "... = swap C (A ∐ B) ∘⇩c ⟨c, left_coproj A B ∘⇩c a⟩"
    using assms by (typecheck_cfuncs, simp add: factor_prod_coprod_left_ap_left)
  also have "... = ⟨left_coproj A B ∘⇩c a, c⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  finally show ?thesis.
qed

lemma factor_prod_coprod_right_ap_right:
  assumes "b ∈⇩c B" "c ∈⇩c C"
  shows "factor_prod_coprod_right A B C ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩ = ⟨right_coproj A B ∘⇩c b, c⟩"
proof -
  have "factor_prod_coprod_right A B C ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩
    = (swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (swap A C ⨝⇩f swap B C)) ∘⇩c (right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩)"
    unfolding factor_prod_coprod_right_def by auto
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c ((swap A C ⨝⇩f swap B C) ∘⇩c right_coproj (A ×⇩c C) (B ×⇩c C)) ∘⇩c ⟨b, c⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c (right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap B C) ∘⇩c ⟨b, c⟩"
    using assms by (typecheck_cfuncs, auto simp add: right_coproj_cfunc_bowtie_prod)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c swap B C ∘⇩c ⟨b, c⟩"
    using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = swap C (A ∐ B) ∘⇩c factor_prod_coprod_left C A B ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, b⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  also have "... = swap C (A ∐ B) ∘⇩c ⟨c, right_coproj A B ∘⇩c b⟩"
    using assms by (typecheck_cfuncs, simp add: factor_prod_coprod_left_ap_right)
  also have "... = ⟨right_coproj A B ∘⇩c b, c⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  finally show ?thesis.
qed

subsubsection  ‹Distribute Product over Coproduct on Right›

definition dist_prod_coprod_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "dist_prod_coprod_right A B C = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C"

lemma dist_prod_coprod_right_type[type_rule]:
  "dist_prod_coprod_right A B C : (A ∐ B) ×⇩c C → (A ×⇩c C) ∐ (B ×⇩c C)"
  unfolding dist_prod_coprod_right_def by typecheck_cfuncs

lemma dist_prod_coprod_right_ap_left:
  assumes "a ∈⇩c A" "c ∈⇩c C"
  shows "dist_prod_coprod_right A B C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩ = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩"
proof -
  have "dist_prod_coprod_right A B C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩
    = ((swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C) ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩"
    unfolding dist_prod_coprod_right_def by auto
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C ∘⇩c ⟨left_coproj A B ∘⇩c a, c⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c ⟨c, left_coproj A B ∘⇩c a⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, a⟩"
    using assms by (typecheck_cfuncs, simp add: dist_prod_coprod_left_ap_left)
  also have "... = ((swap C A ⨝⇩f swap C B) ∘⇩c left_coproj (C ×⇩c A) (C ×⇩c B)) ∘⇩c ⟨c, a⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = (left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C A) ∘⇩c ⟨c, a⟩"
    using assms left_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, auto)
  also have "... = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C A ∘⇩c ⟨c, a⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = left_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨a, c⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  finally show ?thesis.
qed

lemma dist_prod_coprod_right_ap_right:
  assumes "b ∈⇩c B" "c ∈⇩c C"
  shows "dist_prod_coprod_right A B C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩ = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩"
proof -
  have "dist_prod_coprod_right A B C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩
    = ((swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C) ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩"
    unfolding dist_prod_coprod_right_def by auto
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c swap (A ∐ B) C ∘⇩c ⟨right_coproj A B ∘⇩c b, c⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2)
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c dist_prod_coprod_left C A B ∘⇩c ⟨c, right_coproj A B ∘⇩c b⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  also have "... = (swap C A ⨝⇩f swap C B) ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B) ∘⇩c ⟨c, b⟩"
    using assms by (typecheck_cfuncs, simp add: dist_prod_coprod_left_ap_right)
  also have "... = ((swap C A ⨝⇩f swap C B) ∘⇩c right_coproj (C ×⇩c A) (C ×⇩c B)) ∘⇩c ⟨c, b⟩"
    using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = (right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C B) ∘⇩c ⟨c, b⟩"
    using assms by (typecheck_cfuncs, auto simp add: right_coproj_cfunc_bowtie_prod)
  also have "... = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c swap C B ∘⇩c ⟨c, b⟩"
    using assms by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = right_coproj (A ×⇩c C) (B ×⇩c C) ∘⇩c ⟨b, c⟩"
    using assms swap_ap by (typecheck_cfuncs, auto)
  finally show ?thesis.
qed

lemma dist_prod_coprod_right_left_coproj:
  "dist_prod_coprod_right X Y H ∘⇩c (left_coproj X Y ×⇩f id H) = left_coproj (X ×⇩c H) (Y ×⇩c H)"
  by (typecheck_cfuncs, smt (z3) one_separator cart_prod_decomp cfunc_cross_prod_comp_cfunc_prod comp_associative2 dist_prod_coprod_right_ap_left id_left_unit2)

lemma dist_prod_coprod_right_right_coproj:
  "dist_prod_coprod_right X Y H ∘⇩c (right_coproj X Y ×⇩f id H) = right_coproj (X ×⇩c H) (Y ×⇩c H)"
  by (typecheck_cfuncs, smt (z3) one_separator cart_prod_decomp cfunc_cross_prod_comp_cfunc_prod comp_associative2 dist_prod_coprod_right_ap_right id_left_unit2)

lemma factor_dist_prod_coprod_right:
"factor_prod_coprod_right A B C ∘⇩c dist_prod_coprod_right A B C = id ((A ∐ B) ×⇩c C)"
  unfolding factor_prod_coprod_right_def dist_prod_coprod_right_def
  by (typecheck_cfuncs, smt (verit, best) cfunc_bowtie_prod_comp_cfunc_bowtie_prod comp_associative2 factor_dist_prod_coprod_left id_bowtie_prod id_left_unit2 swap_idempotent)
   
lemma dist_factor_prod_coprod_right:
"dist_prod_coprod_right A B C ∘⇩c factor_prod_coprod_right A B C = id ((A ×⇩c C) ∐ (B ×⇩c C))"
  unfolding factor_prod_coprod_right_def dist_prod_coprod_right_def
  by (typecheck_cfuncs, smt (verit, best) cfunc_bowtie_prod_comp_cfunc_bowtie_prod comp_associative2 dist_factor_prod_coprod_left id_bowtie_prod id_left_unit2 swap_idempotent)
   
lemma factor_prod_coprod_right_iso:
  "isomorphism(factor_prod_coprod_right A B C)"
  by (metis cfunc_type_def dist_factor_prod_coprod_right factor_prod_coprod_right_type factor_dist_prod_coprod_right dist_prod_coprod_right_type isomorphism_def)

subsection ‹Casting between Sets›

subsubsection  ‹Going from a Set or its Complement to the Superset›

text ‹This subsection corresponds to Proposition 2.4.5 in Halvorson.›
definition into_super :: "cfunc ⇒ cfunc" where
  "into_super m = m ⨿ m⇧c"

lemma into_super_type[type_rule]:
  "monomorphism m ⟹ m : X → Y ⟹ into_super m : X ∐ (Y ∖ (X,m)) → Y"
  unfolding into_super_def by typecheck_cfuncs

lemma into_super_mono:
  assumes "monomorphism m" "m : X → Y"
  shows "monomorphism (into_super m)"
proof (rule injective_imp_monomorphism, unfold injective_def, clarify)
  fix x y
  assume "x ∈⇩c domain (into_super m)"  then have x_type: "x ∈⇩c X ∐ (Y ∖ (X,m))"
    using assms cfunc_type_def into_super_type by auto
  
  assume "y ∈⇩c domain (into_super m)"  then have y_type: "y ∈⇩c X ∐ (Y ∖ (X,m))"
    using assms cfunc_type_def into_super_type by auto

  assume into_super_eq: "into_super m ∘⇩c x = into_super m ∘⇩c y"

  have x_cases: "(∃ x'. x' ∈⇩c X ∧ x = left_coproj X (Y ∖ (X,m)) ∘⇩c x')
    ∨  (∃ x'. x' ∈⇩c Y ∖ (X,m) ∧ x = right_coproj X (Y ∖ (X,m)) ∘⇩c x')"
    by (simp add: coprojs_jointly_surj x_type)

  have y_cases: "(∃ y'. y' ∈⇩c X ∧ y = left_coproj X (Y ∖ (X,m)) ∘⇩c y')
    ∨  (∃ y'. y' ∈⇩c Y ∖ (X,m) ∧ y = right_coproj X (Y ∖ (X,m)) ∘⇩c y')"
    by (simp add: coprojs_jointly_surj y_type)

  show "x = y"
    using x_cases y_cases
  proof safe
    fix x' y'
    assume x'_type: "x' ∈⇩c X" and x_def: "x = left_coproj X (Y ∖ (X, m)) ∘⇩c x'"
    assume y'_type: "y' ∈⇩c X" and y_def: "y = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"

    have "into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      using into_super_eq unfolding x_def y_def by auto
    then have "(into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c y'"
      using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
    then have "m ∘⇩c x' = m ∘⇩c y'"
      using assms unfolding into_super_def
      by (simp add: complement_morphism_type left_coproj_cfunc_coprod)
    then have "x' = y'"
      using assms cfunc_type_def monomorphism_def x'_type y'_type by auto
    then show "left_coproj X (Y ∖ (X, m)) ∘⇩c x' = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      by simp
  next
    fix x' y'
    assume x'_type: "x' ∈⇩c X" and x_def: "x = left_coproj X (Y ∖ (X, m)) ∘⇩c x'"
    assume y'_type: "y' ∈⇩c Y ∖ (X, m)" and y_def: "y = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"

    have "into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      using into_super_eq unfolding x_def y_def by auto
    then have "(into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c y'"
      using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
    then have "m ∘⇩c x' = m⇧c ∘⇩c y'"
      using assms unfolding into_super_def
      by (simp add: complement_morphism_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
    then have False
      using assms complement_disjoint x'_type y'_type by blast
    then show "left_coproj X (Y ∖ (X, m)) ∘⇩c x' = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      by auto
  next
    fix x' y'
    assume x'_type: "x' ∈⇩c Y ∖ (X, m)" and x_def: "x = right_coproj X (Y ∖ (X, m)) ∘⇩c x'"
    assume y'_type: "y' ∈⇩c X" and y_def: "y = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"

    have "into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      using into_super_eq unfolding x_def y_def by auto
    then have "(into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c left_coproj X (Y ∖ (X, m))) ∘⇩c y'"
      using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
    then have "m⇧c ∘⇩c x' = m ∘⇩c y'"
      using assms unfolding into_super_def
      by (simp add: complement_morphism_type left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
    then have False
      using assms complement_disjoint x'_type y'_type by fastforce
    then show "right_coproj X (Y ∖ (X, m)) ∘⇩c x' = left_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      by auto
  next
    fix x' y'
    assume x'_type: "x' ∈⇩c Y ∖ (X, m)" and x_def: "x = right_coproj X (Y ∖ (X, m)) ∘⇩c x'"
    assume y'_type: "y' ∈⇩c Y ∖ (X, m)" and y_def: "y = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"

    have "into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c x' = into_super m ∘⇩c right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      using into_super_eq unfolding x_def y_def by auto
    then have "(into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c x' = (into_super m ∘⇩c right_coproj X (Y ∖ (X, m))) ∘⇩c y'"
      using assms x'_type y'_type comp_associative2 by (typecheck_cfuncs, auto)
    then have "m⇧c ∘⇩c x' = m⇧c ∘⇩c y'"
      using assms unfolding into_super_def
      by (simp add: complement_morphism_type right_coproj_cfunc_coprod)
    then have "x' = y'"
      using assms complement_morphism_mono complement_morphism_type monomorphism_def2 x'_type y'_type by blast
    then show "right_coproj X (Y ∖ (X, m)) ∘⇩c x' = right_coproj X (Y ∖ (X, m)) ∘⇩c y'"
      by simp
  qed
qed

lemma into_super_epi:
  assumes "monomorphism m" "m : X → Y"
  shows "epimorphism (into_super m)"
proof (rule surjective_is_epimorphism, unfold surjective_def, clarify)
  fix y
  assume "y ∈⇩c codomain (into_super m)"
  then have y_type: "y ∈⇩c Y"
    using assms cfunc_type_def into_super_type by auto

  have y_cases: "(characteristic_func m ∘⇩c y = 𝗍) ∨ (characteristic_func m ∘⇩c y = 𝖿)"
    using y_type assms true_false_only_truth_values by (typecheck_cfuncs, blast)
  then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
  proof safe
    assume "characteristic_func m ∘⇩c y = 𝗍"
    then have "y ∈⇘Y⇙ (X, m)"
      by (simp add: assms characteristic_func_true_relative_member y_type)
    then obtain x where x_type: "x ∈⇩c X" and x_def: "y = m ∘⇩c x"
      unfolding relative_member_def2 by (auto, unfold factors_through_def2, auto)
    then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
      unfolding into_super_def using assms cfunc_type_def comp_associative left_coproj_cfunc_coprod
      by (intro exI[where x="left_coproj X (Y ∖ (X, m)) ∘⇩c x"], typecheck_cfuncs, metis)
  next
    assume "characteristic_func m ∘⇩c y = 𝖿"
    then have "¬ y ∈⇘Y⇙ (X, m)"
      by (simp add: assms characteristic_func_false_not_relative_member y_type)
    then have "y ∈⇘Y⇙ (Y ∖ (X, m), m⇧c)"
      by (simp add: assms not_in_subset_in_complement y_type)
    then obtain x' where x'_type: "x' ∈⇩c Y ∖ (X, m)" and x'_def: "y = m⇧c ∘⇩c x'"
      unfolding relative_member_def2 by (auto, unfold factors_through_def2, auto)
    then show "∃x. x ∈⇩c domain (into_super m) ∧ into_super m ∘⇩c x = y"
      unfolding into_super_def using assms cfunc_type_def comp_associative right_coproj_cfunc_coprod
      by (intro exI[where x="right_coproj X (Y ∖ (X, m)) ∘⇩c x'"], typecheck_cfuncs, metis)
  qed
qed

lemma into_super_iso:
  assumes "monomorphism m" "m : X → Y"
  shows "isomorphism (into_super m)"
  using assms epi_mon_is_iso into_super_epi into_super_mono by auto

subsubsection ‹Going from a Set to a Subset or its Complement›

definition try_cast :: "cfunc ⇒ cfunc" where
  "try_cast m = (THE m'. m' : codomain m → domain m ∐ ((codomain m) ∖ ((domain m),m))
    ∧ m' ∘⇩c into_super m = id (domain m ∐ (codomain m ∖ ((domain m),m)))
    ∧ into_super m ∘⇩c m' = id (codomain m))"

lemma try_cast_def2:
  assumes "monomorphism m" "m : X → Y"
  shows "try_cast m : codomain m → (domain m) ∐ ((codomain m) ∖ ((domain m),m))
    ∧ try_cast m ∘⇩c into_super m = id ((domain m) ∐ ((codomain m) ∖ ((domain m),m)))
    ∧ into_super m ∘⇩c try_cast m = id (codomain m)"
  unfolding try_cast_def
proof (rule theI', safe)
  show "∃x. x : codomain m → domain m ∐ (codomain m ∖ (domain m, m)) ∧
        x ∘⇩c into_super m = id⇩c (domain m ∐ (codomain m ∖ (domain m, m))) ∧
        into_super m ∘⇩c x = id⇩c (codomain m)"
    using assms into_super_iso cfunc_type_def into_super_type unfolding isomorphism_def by fastforce
next
  fix x y
  assume x_type: "x : codomain m → domain m ∐ (codomain m ∖ (domain m, m))"
  assume y_type: "y : codomain m → domain m ∐ (codomain m ∖ (domain m, m))"
  assume "into_super m ∘⇩c x = id⇩c (codomain m)" and "into_super m ∘⇩c y = id⇩c (codomain m)"
  then have "into_super m ∘⇩c x = into_super m ∘⇩c y"
    by auto
  then show "x = y"
    using into_super_mono unfolding monomorphism_def
    by (metis assms(1) cfunc_type_def into_super_type monomorphism_def x_type y_type)
qed

lemma try_cast_type[type_rule]:
  assumes "monomorphism m" "m : X → Y"
  shows "try_cast m : Y → X ∐ (Y ∖ (X,m))"
  using assms cfunc_type_def try_cast_def2 by auto 

lemma try_cast_into_super:
  assumes "monomorphism m" "m : X → Y"
  shows "try_cast m ∘⇩c into_super m = id (X ∐ (Y ∖ (X,m)))"
  using assms cfunc_type_def try_cast_def2 by auto

lemma into_super_try_cast:
  assumes "monomorphism m" "m : X → Y"
  shows "into_super m ∘⇩c  try_cast m = id Y"
  using assms cfunc_type_def try_cast_def2 by auto

lemma try_cast_in_X:
  assumes m_type: "monomorphism m" "m : X → Y"
  assumes y_in_X: "y ∈⇘Y⇙ (X, m)"
  shows "∃ x. x ∈⇩c X ∧ try_cast m ∘⇩c y = left_coproj X (Y ∖ (X,m)) ∘⇩c x"
proof -
  have y_type: "y ∈⇩c Y"
    using y_in_X unfolding relative_member_def2 by auto
  obtain x where x_type: "x ∈⇩c X" and x_def: "y = m ∘⇩c x"
    using y_in_X unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
  then have "y = (into_super m ∘⇩c left_coproj X (Y ∖ (X,m))) ∘⇩c x"
    unfolding into_super_def using complement_morphism_type left_coproj_cfunc_coprod m_type by auto
  then have "y = into_super m ∘⇩c left_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using x_type m_type by (typecheck_cfuncs, simp add:  comp_associative2)
  then have "try_cast m ∘⇩c y = (try_cast m ∘⇩c into_super m) ∘⇩c left_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using x_type m_type by (typecheck_cfuncs, smt comp_associative2)
  then have "try_cast m ∘⇩c y = left_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using m_type x_type by (typecheck_cfuncs, simp add: id_left_unit2 try_cast_into_super)
  then show ?thesis
    using x_type by blast
qed

lemma try_cast_not_in_X:
  assumes m_type: "monomorphism m" "m : X → Y"
  assumes y_in_X: "¬ y ∈⇘Y⇙ (X, m)" and y_type: "y ∈⇩c Y"  
  shows "∃ x. x ∈⇩c Y ∖ (X,m) ∧ try_cast m ∘⇩c y = right_coproj X (Y ∖ (X,m)) ∘⇩c x"
proof -
  have y_in_complement: "y ∈⇘Y⇙ (Y ∖ (X,m), m⇧c)"
    by (simp add: assms not_in_subset_in_complement)
  then obtain x where x_type: "x ∈⇩c Y ∖ (X,m)" and x_def: "y = m⇧c ∘⇩c x"
    unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
  then have "y = (into_super m ∘⇩c right_coproj X (Y ∖ (X,m))) ∘⇩c x"
    unfolding into_super_def using complement_morphism_type m_type right_coproj_cfunc_coprod by auto 
  then have "y = into_super m ∘⇩c right_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using x_type m_type by (typecheck_cfuncs, simp add:  comp_associative2)
  then have "try_cast m ∘⇩c y = (try_cast m ∘⇩c into_super m) ∘⇩c right_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using x_type m_type by (typecheck_cfuncs, smt comp_associative2)
  then have "try_cast m ∘⇩c y = right_coproj X (Y ∖ (X,m)) ∘⇩c x"
    using m_type x_type by (typecheck_cfuncs, simp add: id_left_unit2 try_cast_into_super)
  then show ?thesis
    using x_type by blast
qed

lemma try_cast_m_m:
  assumes m_type: "monomorphism m" "m : X → Y"
  shows "(try_cast m) ∘⇩c m = left_coproj X (Y ∖ (X,m))"
  by (smt comp_associative2 complement_morphism_type id_left_unit2 into_super_def into_super_type left_coproj_cfunc_coprod left_proj_type m_type try_cast_into_super try_cast_type)

lemma try_cast_m_m':
  assumes m_type: "monomorphism m" "m : X → Y"
  shows "(try_cast m) ∘⇩c m⇧c = right_coproj X (Y ∖ (X,m))"
  by (smt comp_associative2 complement_morphism_type id_left_unit2 into_super_def into_super_type m_type(1) m_type(2) right_coproj_cfunc_coprod right_proj_type try_cast_into_super try_cast_type)

lemma try_cast_mono:
  assumes m_type: "monomorphism m" "m : X → Y"
  shows "monomorphism(try_cast m)"
  by (smt cfunc_type_def comp_monic_imp_monic' id_isomorphism into_super_type iso_imp_epi_and_monic try_cast_def2 assms)  

subsection ‹Cases›

definition cases :: "cfunc ⇒ cfunc" where
"cases(f) = ((right_cart_proj 𝟭 (domain f)) ⨝⇩f (right_cart_proj 𝟭 (domain f))) ∘⇩c (dist_prod_coprod_right 𝟭 𝟭 (domain f)) ∘⇩c ⟨case_bool ∘⇩c f, id(domain(f))⟩"

lemma cases_def2: 
  assumes "f : X → Ω"
  shows "cases(f) = ((right_cart_proj 𝟭 X) ⨝⇩f (right_cart_proj 𝟭 X)) ∘⇩c (dist_prod_coprod_right 𝟭 𝟭 X) ∘⇩c ⟨case_bool ∘⇩c f, id X⟩"
  unfolding cases_def
  using assms cfunc_type_def by auto 

lemma cases_type[type_rule]:
  assumes "f : X → Ω"
  shows "cases(f) : X  → X ∐ X"
  using assms by(etcs_subst cases_def2,
  meson case_bool_def2 cfunc_bowtie_prod_type cfunc_prod_type comp_type
  dist_prod_coprod_right_type id_type right_cart_proj_type)
  
lemma true_case:
  assumes x_type[type_rule]: "x ∈⇩c X"
  assumes f_type[type_rule]: "f : X → Ω"
  assumes true_case: "f ∘⇩c x = 𝗍"
  shows "cases f ∘⇩c x = left_coproj X X ∘⇩c x"
proof (etcs_subst cases_def2)  
  have "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c
     dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x 
  = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c  dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f ∘⇩c x, x⟩"
     using cfunc_prod_comp comp_associative2 id_left_unit2  by (etcs_assocr, typecheck_cfuncs, force)
  also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨left_coproj 𝟭 𝟭, x⟩"
    using true_case case_bool_true by argo
  also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c left_coproj (𝟭 ×⇩c X) (𝟭 ×⇩c X) ∘⇩c ⟨id 𝟭 , x⟩"
    by (typecheck_cfuncs, metis dist_prod_coprod_right_ap_left id_right_unit2)
  also have "... = left_coproj X X ∘⇩c right_cart_proj 𝟭 X  ∘⇩c ⟨id 𝟭, x⟩"
    by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_bowtie_prod)
  also have "... = left_coproj X X ∘⇩c x"
    using right_cart_proj_cfunc_prod by (typecheck_cfuncs, presburger)
  finally show "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x = left_coproj X X ∘⇩c x".
qed

lemma false_case:
  assumes x_type[type_rule]: "x ∈⇩c X"
  assumes f_type[type_rule]: "f : X → Ω"
  assumes false_case: "f ∘⇩c x = 𝖿"
  shows "cases f ∘⇩c x = right_coproj X X ∘⇩c x"
proof (etcs_subst cases_def2)  
  have "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c
     dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x 
  = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c  dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f ∘⇩c x, x⟩"
     using cfunc_prod_comp comp_associative2 id_left_unit2  by (etcs_assocr, typecheck_cfuncs, force)
  also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨right_coproj 𝟭 𝟭, x⟩"
    using false_case case_bool_false by argo
  also have "... = (right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c right_coproj (𝟭 ×⇩c X) (𝟭 ×⇩c X) ∘⇩c ⟨id 𝟭 , x⟩"
    by (typecheck_cfuncs, metis dist_prod_coprod_right_ap_right id_right_unit2)
  also have "... = right_coproj X X ∘⇩c right_cart_proj 𝟭 X  ∘⇩c ⟨id 𝟭, x⟩"
    using comp_associative2 right_coproj_cfunc_bowtie_prod by (typecheck_cfuncs, force)
  also have "... = right_coproj X X ∘⇩c x"
    using right_cart_proj_cfunc_prod by (typecheck_cfuncs, presburger)
  finally show "((right_cart_proj 𝟭 X ⨝⇩f right_cart_proj 𝟭 X) ∘⇩c dist_prod_coprod_right 𝟭 𝟭 X ∘⇩c ⟨case_bool ∘⇩c f,id⇩c X⟩) ∘⇩c x = right_coproj X X ∘⇩c x".
qed

subsection  ‹Coproduct Set Properities›

lemma coproduct_commutes:
  "A ∐ B ≅ B ∐ A"
proof -
  have id_AB: "((right_coproj A B)  ⨿ (left_coproj A B)) ∘⇩c ((right_coproj B A) ⨿ (left_coproj B A)) = id(A ∐ B)"
    by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp id_coprod left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
  have id_BA: " ((right_coproj B A) ⨿ (left_coproj B A)) ∘⇩c ((right_coproj A B)  ⨿ (left_coproj A B)) = id(B ∐ A)"
    by (typecheck_cfuncs, smt (z3) cfunc_coprod_comp id_coprod right_coproj_cfunc_coprod left_coproj_cfunc_coprod)
  show "A ∐ B ≅ B ∐ A"
    by (smt (verit, ccfv_threshold) cfunc_coprod_type cfunc_type_def id_AB id_BA is_isomorphic_def isomorphism_def left_proj_type right_proj_type)
qed

lemma coproduct_associates:
  "A ∐ (B ∐ C)  ≅ (A ∐ B) ∐ C"
proof -
  obtain q where q_def: "q = (left_coproj (A ∐ B) C ) ∘⇩c (right_coproj A B)" and q_type[type_rule]: "q: B → (A ∐ B) ∐ C"
    by (typecheck_cfuncs, simp)  
  obtain f where f_def: "f = q ⨿ (right_coproj (A ∐ B) C)" and f_type[type_rule]: "(f: (B ∐ C) → ((A ∐ B) ∐ C))"
    by (typecheck_cfuncs, simp)
  have f_prop: "(f ∘⇩c left_coproj B C = q) ∧ (f ∘⇩c right_coproj B C = right_coproj (A ∐ B) C)"
    by (typecheck_cfuncs, simp add: f_def left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
  then have f_unique: "(∃!f. (f: (B ∐ C) → ((A ∐ B) ∐ C)) ∧ (f ∘⇩c left_coproj B C = q) ∧ (f ∘⇩c right_coproj B C = right_coproj (A ∐ B) C))"
    by (typecheck_cfuncs, metis cfunc_coprod_unique f_prop f_type)

  obtain m where m_def: "m = (left_coproj (A ∐ B) C ) ∘⇩c (left_coproj A B)" and m_type[type_rule]: "m : A → (A ∐ B) ∐ C"
    by (typecheck_cfuncs, simp)
  obtain g where g_def: "g = m ⨿ f" and g_type[type_rule]: "g: A ∐ (B ∐ C)  → (A ∐ B) ∐ C"
    by (typecheck_cfuncs, simp)
  have g_prop: "(g ∘⇩c (left_coproj A (B ∐ C)) = m) ∧ (g ∘⇩c (right_coproj A (B ∐ C)) = f)"
    by (typecheck_cfuncs, simp add: g_def left_coproj_cfunc_coprod right_coproj_cfunc_coprod) 
  have g_unique: "∃! g. ((g: A ∐ (B ∐ C)  → (A ∐ B) ∐ C) ∧ (g ∘⇩c (left_coproj A (B ∐ C)) = m) ∧ (g ∘⇩c (right_coproj A (B ∐ C)) = f))"
    by (typecheck_cfuncs, metis cfunc_coprod_unique g_prop g_type)

  obtain p where p_def: "p = (right_coproj A (B ∐ C)) ∘⇩c  (left_coproj B C)" and p_type[type_rule]: "p: B → A ∐ (B ∐ C)"
    by (typecheck_cfuncs, simp)
  obtain h where h_def: "h = (left_coproj A (B ∐ C)) ⨿ p" and h_type[type_rule]: "h: (A ∐ B) → A ∐ (B ∐ C)"
    by (typecheck_cfuncs, simp)
  have h_prop1: "h ∘⇩c (left_coproj A B)  = (left_coproj A (B ∐ C))"
    by (typecheck_cfuncs, simp add: h_def left_coproj_cfunc_coprod p_type)
  have h_prop2: "h ∘⇩c (right_coproj A B) = p"
    using h_def left_proj_type right_coproj_cfunc_coprod by (typecheck_cfuncs, blast)
  have h_unique: "∃! h. ((h: (A ∐ B) → A ∐ (B ∐ C)) ∧ (h ∘⇩c (left_coproj A B)  = (left_coproj A (B ∐ C))) ∧ (h ∘⇩c (right_coproj A B) =p))"
    by (typecheck_cfuncs, metis cfunc_coprod_unique h_prop1 h_prop2 h_type)

  obtain j where j_def: "j = (right_coproj A (B ∐ C)) ∘⇩c  (right_coproj B C)" and j_type[type_rule]: "j : C → A ∐ (B ∐ C)"
    by (typecheck_cfuncs, simp)
  obtain k where k_def: "k = h ⨿ j" and k_type[type_rule]: "k: (A ∐ B) ∐ C → A ∐ (B ∐ C)"
    by (typecheck_cfuncs, simp)

  have fact1: "(k ∘⇩c g) ∘⇩c (left_coproj A (B ∐ C)) = (left_coproj A (B ∐ C))"
    by (typecheck_cfuncs, smt (z3) comp_associative2 g_prop h_prop1 h_type j_type k_def left_coproj_cfunc_coprod left_proj_type m_def)
  have fact2: "(g ∘⇩c k) ∘⇩c (left_coproj (A ∐ B) C) = (left_coproj (A ∐ B) C)"
    by (typecheck_cfuncs, smt (verit) cfunc_coprod_comp cfunc_coprod_unique comp_associative2 comp_type f_prop g_prop g_type h_def h_type j_def k_def k_type left_coproj_cfunc_coprod left_proj_type m_def p_def p_type q_def right_proj_type)
  have fact3: "(g ∘⇩c k) ∘⇩c (right_coproj (A ∐ B) C) = (right_coproj (A ∐ B) C)"
    by (smt comp_associative2 comp_type f_def g_prop g_type h_type j_def k_def k_type q_type right_coproj_cfunc_coprod right_proj_type)
  have fact4: "(k ∘⇩c g) ∘⇩c (right_coproj A (B ∐ C)) = (right_coproj A (B ∐ C))"
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) cfunc_coprod_unique cfunc_type_def comp_associative comp_type f_prop g_prop h_prop2 h_type j_def k_def left_coproj_cfunc_coprod left_proj_type p_def q_def right_coproj_cfunc_coprod right_proj_type)
  have fact5: "(k ∘⇩c g) = id( A ∐ (B ∐ C))"
    by (typecheck_cfuncs, metis cfunc_coprod_unique fact1 fact4 id_coprod left_proj_type right_proj_type)
  have fact6: "(g ∘⇩c k) = id((A ∐ B) ∐ C)"
    by (typecheck_cfuncs, metis cfunc_coprod_unique fact2 fact3 id_coprod left_proj_type right_proj_type)
  show ?thesis
    by (metis cfunc_type_def fact5 fact6 g_type is_isomorphic_def isomorphism_def k_type)
qed

text ‹The lemma below corresponds to Proposition 2.5.10.›
lemma product_distribute_over_coproduct_left:
  "A ×⇩c (X ∐ Y) ≅ (A ×⇩c X) ∐ (A ×⇩c Y)"
  using factor_prod_coprod_left_type dist_prod_coprod_iso is_isomorphic_def isomorphic_is_symmetric by blast

lemma prod_pres_iso:
  assumes "A ≅  C"  "B ≅ D"
  shows "A ×⇩c B ≅  C ×⇩c D"
proof - 
  obtain f where f_def: "f: A → C ∧ isomorphism(f)"
    using assms(1) is_isomorphic_def by blast
  obtain g where g_def: "g: B → D ∧ isomorphism(g)"
    using assms(2) is_isomorphic_def by blast
  have "isomorphism(f×⇩fg)"
    by (meson cfunc_cross_prod_mono cfunc_cross_prod_surj epi_is_surj epi_mon_is_iso f_def g_def iso_imp_epi_and_monic surjective_is_epimorphism)
  then show "A ×⇩c B ≅  C ×⇩c D"
    by (meson cfunc_cross_prod_type f_def g_def is_isomorphic_def)
qed

lemma coprod_pres_iso:
  assumes "A ≅  C"  "B ≅ D"
  shows "A ∐ B ≅  C ∐ D"
proof- 
  obtain f where f_def: "f: A → C" "isomorphism(f)"
    using assms(1) is_isomorphic_def by blast
  obtain g where g_def: "g: B → D" "isomorphism(g)"
    using assms(2) is_isomorphic_def by blast

  have surj_f: "surjective(f)"
    using epi_is_surj f_def iso_imp_epi_and_monic by blast
  have surj_g: "surjective(g)"
    using epi_is_surj g_def iso_imp_epi_and_monic by blast

  have coproj_f_inject: "injective(((left_coproj C D) ∘⇩c f))"
    using cfunc_type_def composition_of_monic_pair_is_monic f_def iso_imp_epi_and_monic left_coproj_are_monomorphisms left_proj_type monomorphism_imp_injective by auto
    
  have coproj_g_inject: "injective(((right_coproj C D) ∘⇩c g))"
    using cfunc_type_def composition_of_monic_pair_is_monic g_def iso_imp_epi_and_monic right_coproj_are_monomorphisms right_proj_type monomorphism_imp_injective by auto

  obtain φ where φ_def: "φ = (left_coproj C D ∘⇩c f)  ⨿ (right_coproj C D ∘⇩c g)"
    by simp
  then have φ_type: "φ: A ∐ B →  C ∐ D"
    using cfunc_coprod_type cfunc_type_def codomain_comp domain_comp f_def g_def left_proj_type right_proj_type by auto

  have "surjective(φ)"
    unfolding surjective_def
  proof(clarify) 
    fix y 
    assume y_type: "y ∈⇩c codomain φ"
    then have y_type2: "y ∈⇩c C ∐ D"
      using φ_type cfunc_type_def by auto
    then have y_form: "(∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c)
      ∨  (∃ d. d ∈⇩c D ∧ y = right_coproj C D ∘⇩c d)"
      using coprojs_jointly_surj by auto
    show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
    proof(cases "∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c")
      assume "∃ c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
      then obtain c where c_def: "c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
        by blast
      then have "∃ a. a ∈⇩c A ∧ f ∘⇩c a = c"
        using cfunc_type_def f_def surj_f surjective_def by auto
      then obtain a where a_def: "a ∈⇩c A ∧ f ∘⇩c a = c"
        by blast
      obtain x where x_def: "x = left_coproj A B ∘⇩c a"
        by blast
      have x_type: "x ∈⇩c A ∐ B"
        using a_def comp_type left_proj_type x_def by blast
      have "φ ∘⇩c x = y"
        using φ_def φ_type a_def c_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_def by (smt (verit))
      then show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
        using φ_type cfunc_type_def x_type by auto
    next
      assume "∄c. c ∈⇩c C ∧ y = left_coproj C D ∘⇩c c"
      then have y_def2: "∃ d. d ∈⇩c D ∧ y = right_coproj C D ∘⇩c d"
        using y_form by blast
      then obtain d where d_def: "d ∈⇩c D" "y = right_coproj C D ∘⇩c d"
        by blast
      then have "∃ b. b ∈⇩c B ∧ g ∘⇩c b = d"
        using cfunc_type_def g_def surj_g surjective_def by auto
      then obtain b where b_def: "b ∈⇩c B" "g ∘⇩c b = d"
        by blast
      obtain x where x_def: "x = right_coproj A B ∘⇩c b"
        by blast
      have x_type: "x ∈⇩c A ∐ B"
        using b_def comp_type right_proj_type x_def by blast
      have "φ ∘⇩c x = y"
        using φ_def φ_type b_def cfunc_type_def comp_associative comp_type d_def f_def g_def left_proj_type right_coproj_cfunc_coprod right_proj_type x_def by (smt (verit))
      then show "∃x. x ∈⇩c domain φ ∧ φ ∘⇩c x = y"
        using φ_type cfunc_type_def x_type by auto
    qed
  qed

  have "injective(φ)"
    unfolding injective_def
  proof(clarify)
    fix x y   
    assume x_type: "x ∈⇩c domain φ"
    assume y_type: "y ∈⇩c domain φ"
    assume equals: "φ ∘⇩c x = φ ∘⇩c y"
    have x_type2: "x ∈⇩c A ∐ B"
      using φ_type cfunc_type_def x_type by auto
    have y_type2: "y ∈⇩c A ∐ B"
      using φ_type cfunc_type_def y_type by auto

    have phix_type: "φ ∘⇩c x ∈⇩c C ∐ D"
      using φ_type comp_type x_type2 by blast
    have phiy_type: "φ ∘⇩c y ∈⇩c C ∐ D"
      using equals phix_type by auto

    have x_form: "(∃ a. a ∈⇩c A  ∧ x = left_coproj A B ∘⇩c a)
      ∨  (∃ b. b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b)"
      using cfunc_type_def coprojs_jointly_surj x_type x_type2 y_type by auto
    
    have y_form: "(∃ a. a ∈⇩c A  ∧ y = left_coproj A B ∘⇩c a)
      ∨  (∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b)"
      using cfunc_type_def coprojs_jointly_surj x_type x_type2 y_type by auto

    show "x=y"
    proof(cases "∃ a. a ∈⇩c A  ∧ x = left_coproj A B ∘⇩c a")
      assume "∃ a. a ∈⇩c A  ∧ x = left_coproj A B ∘⇩c a"
      then obtain a where a_def: "a ∈⇩c A" "x = left_coproj A B ∘⇩c a"
        by blast
      show "x = y"
      proof(cases "∃ a. a ∈⇩c A  ∧ y = left_coproj A B ∘⇩c a")
        assume "∃ a. a ∈⇩c A  ∧ y = left_coproj A B ∘⇩c a"
        then obtain a' where a'_def: "a' ∈⇩c A" "y = left_coproj A B ∘⇩c a'"
          by blast
        then have "a = a'"
        proof - 
          have "(left_coproj C D ∘⇩c f) ∘⇩c a = φ ∘⇩c x"
            using φ_def a_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_type by (smt (verit))
          also have "... = φ ∘⇩c y"
            by (meson equals)
          also have "... = (φ ∘⇩c left_coproj A B) ∘⇩c a'"
            using φ_type a'_def comp_associative2 by (typecheck_cfuncs, blast)
          also have "... = (left_coproj C D ∘⇩c f) ∘⇩c a'"
            unfolding φ_def using f_def g_def a'_def left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          ultimately show "a = a'"
            by (smt a'_def a_def cfunc_type_def coproj_f_inject domain_comp f_def injective_def left_proj_type)
        qed
        then show "x=y"
          by (simp add:  a'_def(2) a_def(2))
      next
        assume "∄a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
        then have "∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b"
          using y_form by blast
        then obtain b' where b'_def: "b' ∈⇩c B" "y = right_coproj A B ∘⇩c b'"
          by blast
        show "x = y"
        proof - 
          have "left_coproj C D ∘⇩c (f ∘⇩c a) = (left_coproj C D ∘⇩c f) ∘⇩c a"
            using a_def cfunc_type_def comp_associative f_def left_proj_type by auto
          also have "...  = φ ∘⇩c x"
              using φ_def a_def cfunc_type_def comp_associative comp_type f_def g_def left_coproj_cfunc_coprod left_proj_type right_proj_type x_type by (smt (verit))
          also have "... = φ ∘⇩c y"
            by (meson equals)
          also have "... = (φ ∘⇩c right_coproj A B) ∘⇩c b'"
            using φ_type b'_def comp_associative2 by (typecheck_cfuncs, blast)
          also have "... = (right_coproj C D ∘⇩c g) ∘⇩c b' "
            unfolding φ_def using f_def g_def b'_def right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = right_coproj C D ∘⇩c (g ∘⇩c b')"
              using g_def b'_def by (typecheck_cfuncs, simp add: comp_associative2)
          ultimately show "x = y"
             using  a_def(1) b'_def(1) comp_type coproducts_disjoint f_def(1) g_def(1) by auto
         qed
       qed
    next
      assume "∄a. a ∈⇩c A ∧ x = left_coproj A B ∘⇩c a"
      then have "∃ b. b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b"
        using x_form by blast
      then obtain b where b_def: "b ∈⇩c B ∧ x = right_coproj A B ∘⇩c b"
        by blast
      show "x = y"
      proof(cases "∃ a. a ∈⇩c A  ∧ y = left_coproj A B ∘⇩c a")
        assume "∃ a. a ∈⇩c A  ∧ y = left_coproj A B ∘⇩c a"
        then obtain a' where a'_def: "a' ∈⇩c A" "y = left_coproj A B ∘⇩c a'"
          by blast
        show "x = y"
        proof - 
          have "right_coproj C D ∘⇩c (g ∘⇩c b) = (right_coproj C D ∘⇩c g) ∘⇩c b"
            using b_def cfunc_type_def comp_associative g_def right_proj_type by auto
          also have "...  = φ ∘⇩c x"
            by (smt φ_def φ_type b_def comp_associative2 comp_type f_def(1) g_def(1) left_proj_type right_coproj_cfunc_coprod right_proj_type)
          also have "... = φ ∘⇩c y"
            by (meson equals)
          also have "... = (φ ∘⇩c left_coproj A B) ∘⇩c a'"
            using φ_type a'_def comp_associative2 by (typecheck_cfuncs, blast)
          also have "... = (left_coproj C D ∘⇩c f) ∘⇩c a' "
            unfolding φ_def using f_def g_def a'_def left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          also have "... = left_coproj C D ∘⇩c (f ∘⇩c a')"
            using f_def a'_def by (typecheck_cfuncs, simp add: comp_associative2)
          ultimately show "x = y"
            by (metis a'_def(1) b_def comp_type coproducts_disjoint f_def(1) g_def(1))
        qed
      next
        assume "∄a. a ∈⇩c A ∧ y = left_coproj A B ∘⇩c a"
        then have "∃ b. b ∈⇩c B ∧ y = right_coproj A B ∘⇩c b"
          using y_form by blast
        then obtain b' where b'_def: "b' ∈⇩c B" "y = right_coproj A B ∘⇩c b'"
          by blast
        then have "b = b'"
        proof - 
          have "(right_coproj C D ∘⇩c g) ∘⇩c b = φ ∘⇩c x"
            by (smt φ_def φ_type b_def comp_associative2 comp_type f_def(1) g_def(1) left_proj_type right_coproj_cfunc_coprod right_proj_type)
          also have "... = φ ∘⇩c y"
            by (meson equals)
          also have "... = (φ ∘⇩c right_coproj A B) ∘⇩c b'"
            using φ_type b'_def comp_associative2 by (typecheck_cfuncs, blast)
          also have "... = (right_coproj C D ∘⇩c g) ∘⇩c b'"
            unfolding φ_def using f_def g_def b'_def right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
          ultimately show "b = b'"
            by (smt b'_def b_def cfunc_type_def coproj_g_inject domain_comp g_def injective_def right_proj_type)
        qed
        then show "x = y"
          by (simp add: b'_def(2) b_def)
        qed
      qed
    qed

    have "monomorphism φ"
      using ‹injective φ› injective_imp_monomorphism by blast
    have "epimorphism φ"
      by (simp add: ‹surjective φ› surjective_is_epimorphism)
    have "isomorphism φ"
      using ‹epimorphism φ› ‹monomorphism φ› epi_mon_is_iso by blast
    then show ?thesis
      using φ_type is_isomorphic_def by blast
qed 

lemma product_distribute_over_coproduct_right:
  "(A ∐ B) ×⇩c C  ≅ (A ×⇩c C) ∐ (B ×⇩c C)"
  by (meson coprod_pres_iso isomorphic_is_transitive product_commutes product_distribute_over_coproduct_left)

lemma coproduct_with_self_iso:
  "X ∐ X ≅ X ×⇩c Ω"
proof - 
  obtain ρ where ρ_def: "ρ = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ⨿ ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩" and ρ_type[type_rule]: "ρ : X ∐ X → X ×⇩c Ω"
    by (typecheck_cfuncs, simp)
  have ρ_inj: "injective ρ"
    unfolding injective_def
  proof(clarify)
    fix x y 
    assume "x ∈⇩c domain ρ" then have x_type[type_rule]: "x ∈⇩c X ∐ X"
      using ρ_type cfunc_type_def by auto
    assume "y ∈⇩c domain ρ" then have y_type[type_rule]: "y ∈⇩c X ∐ X"
      using ρ_type cfunc_type_def by auto
    assume equals: "ρ ∘⇩c x = ρ ∘⇩c y"
    show "x = y"
    proof(cases "∃ lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X")
      assume "∃lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
      then obtain lx where lx_def: "x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
        by blast
      have ρx: "ρ ∘⇩c x = ⟨lx, 𝗍⟩"
      proof - 
        have "ρ ∘⇩c x = (ρ ∘⇩c left_coproj X X) ∘⇩c lx"
          using comp_associative2 lx_def by (typecheck_cfuncs, blast)
        also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩  ∘⇩c lx"
          unfolding ρ_def  using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨lx, 𝗍⟩"
          by (typecheck_cfuncs, metis cart_prod_extract_left lx_def)
        finally show ?thesis.
      qed
      show "x = y"
      proof(cases "∃ ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X")
        assume "∃ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
        then obtain ly where ly_def: "y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
          by blast
        have "ρ ∘⇩c y = ⟨ly, 𝗍⟩"
        proof - 
          have "ρ ∘⇩c y = (ρ ∘⇩c left_coproj X X) ∘⇩c ly"
            using comp_associative2 ly_def by (typecheck_cfuncs, blast)
          also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩  ∘⇩c ly"
            unfolding ρ_def  using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
          also have "... = ⟨ly, 𝗍⟩"
            by (typecheck_cfuncs, metis cart_prod_extract_left ly_def)
          finally show ?thesis.
        qed
        then show "x = y"
          using ρx cart_prod_eq2 equals lx_def ly_def true_func_type by auto
      next
        assume "∄ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
        then obtain ry where ry_def: "y = right_coproj X X ∘⇩c ry" and ry_type[type_rule]: "ry ∈⇩c X"
          by (meson y_type coprojs_jointly_surj)
        have ρy: "ρ ∘⇩c y = ⟨ry, 𝖿⟩"
        proof - 
          have "ρ ∘⇩c y = (ρ ∘⇩c right_coproj X X) ∘⇩c ry"
            using comp_associative2 ry_def by (typecheck_cfuncs, blast)
          also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩  ∘⇩c ry"
            unfolding ρ_def  using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
          also have "... = ⟨ry, 𝖿⟩"
            by (typecheck_cfuncs, metis cart_prod_extract_left)
          finally show ?thesis.
        qed
        then show ?thesis
          using ρx ρy cart_prod_eq2 equals false_func_type lx_def ry_type true_false_distinct true_func_type by force
      qed
    next
      assume "∄lx. x = left_coproj X X ∘⇩c lx ∧ lx ∈⇩c X"
      then obtain rx where rx_def: "x = right_coproj X X ∘⇩c rx ∧ rx ∈⇩c X"
        by (typecheck_cfuncs, meson coprojs_jointly_surj)
      have ρx: "ρ ∘⇩c x = ⟨rx, 𝖿⟩"
      proof - 
        have "ρ ∘⇩c x = (ρ ∘⇩c right_coproj X X) ∘⇩c rx"
          using comp_associative2 rx_def by (typecheck_cfuncs, blast)
        also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩  ∘⇩c rx"
          unfolding ρ_def  using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨rx, 𝖿⟩"
          by (typecheck_cfuncs, metis cart_prod_extract_left rx_def)
        finally show ?thesis.
      qed
      show "x = y"
      proof(cases "∃ ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X")
        assume "∃ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
        then obtain ly where ly_def: "y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
          by blast
        have "ρ ∘⇩c y = ⟨ly, 𝗍⟩"
        proof - 
          have "ρ ∘⇩c y = (ρ ∘⇩c left_coproj X X) ∘⇩c ly"
            using comp_associative2 ly_def by (typecheck_cfuncs, blast)
          also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩ ∘⇩c ly"
            unfolding ρ_def  using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
          also have "... = ⟨ly, 𝗍⟩"
            by (typecheck_cfuncs, metis cart_prod_extract_left ly_def)
          finally show ?thesis.
        qed
        then show "x = y"
          using ρx cart_prod_eq2 equals false_func_type ly_def rx_def true_false_distinct true_func_type by force
      next
        assume "∄ly. y = left_coproj X X ∘⇩c ly ∧ ly ∈⇩c X"
        then obtain ry where ry_def: "y = right_coproj X X ∘⇩c ry ∧ ry ∈⇩c X"
          using  coprojs_jointly_surj by (typecheck_cfuncs, blast)
        have ρy: "ρ ∘⇩c y = ⟨ry, 𝖿⟩"
        proof - 
          have "ρ ∘⇩c y = (ρ ∘⇩c right_coproj X X) ∘⇩c ry"
            using comp_associative2 ry_def by (typecheck_cfuncs, blast)
          also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩  ∘⇩c ry"
            unfolding ρ_def  using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
          also have "... = ⟨ry, 𝖿⟩"
            by (typecheck_cfuncs, metis cart_prod_extract_left ry_def)
          finally show ?thesis.
        qed
        show "x = y"
          using ρx ρy cart_prod_eq2 equals false_func_type rx_def ry_def by auto
      qed
    qed
  qed
  have "surjective ρ"
    unfolding surjective_def
  proof(clarify)
    fix y
    assume "y ∈⇩c codomain ρ" then have y_type[type_rule]: "y ∈⇩c X ×⇩c Ω"
      using ρ_type cfunc_type_def by fastforce
    then obtain x w where y_def: "y = ⟨x,w⟩ ∧ x ∈⇩c X ∧ w ∈⇩c Ω"
      using cart_prod_decomp by fastforce
    show "∃x. x ∈⇩c domain ρ ∧ ρ ∘⇩c x = y"
    proof(cases "w = 𝗍")
      assume "w = 𝗍"
      obtain z where z_def: "z = left_coproj X X ∘⇩c x"
        by simp
      have "ρ ∘⇩c z = y"
      proof - 
        have "ρ ∘⇩c z = (ρ ∘⇩c left_coproj X X) ∘⇩c x"
          using comp_associative2 y_def z_def by (typecheck_cfuncs, blast)
        also have "... = ⟨id X, 𝗍 ∘⇩c β⇘X⇙⟩  ∘⇩c x"
          unfolding ρ_def  using left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)        
        also have "... = y"
          using ‹w = 𝗍› cart_prod_extract_left y_def by auto
        finally show ?thesis.
      qed
      then show ?thesis
        by (metis ρ_type cfunc_type_def codomain_comp domain_comp left_proj_type y_def z_def)
    next
      assume "w ≠ 𝗍" then have "w = 𝖿"  
        by (typecheck_cfuncs, meson true_false_only_truth_values y_def)
      obtain z where z_def: "z = right_coproj X X ∘⇩c x"
        by simp
      have "ρ ∘⇩c z = y"
      proof - 
        have "ρ ∘⇩c z = (ρ ∘⇩c right_coproj X X) ∘⇩c x"
          using comp_associative2 y_def z_def by (typecheck_cfuncs, blast)
        also have "... = ⟨id X, 𝖿 ∘⇩c β⇘X⇙⟩  ∘⇩c x"
          unfolding ρ_def  using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)        
        also have "... = y"
          using ‹w = 𝖿› cart_prod_extract_left y_def by auto
        finally show ?thesis.
      qed
      then show ?thesis
        by (metis ρ_type cfunc_type_def codomain_comp domain_comp right_proj_type y_def z_def)
    qed
  qed
  then show ?thesis
    by (metis ρ_inj ρ_type epi_mon_is_iso injective_imp_monomorphism is_isomorphic_def surjective_is_epimorphism)
qed

lemma oneUone_iso_Ω:
  "Ω ≅ 𝟭 ∐ 𝟭"
  using case_bool_def2 case_bool_iso is_isomorphic_def by auto

text ‹The lemma below is dual to Proposition 2.2.2 in Halvorson.›
lemma "card {x. x ∈⇩c Ω ∐ Ω} = 4"
proof -
  (*Distinctness*)
  have f1: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝗍"
    by (typecheck_cfuncs, simp add: coproducts_disjoint)
  have f2: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (left_coproj Ω Ω) ∘⇩c 𝖿"
    by (typecheck_cfuncs, metis cfunc_type_def left_coproj_are_monomorphisms monomorphism_def true_false_distinct)
  have f3: "(left_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
    by (typecheck_cfuncs, simp add: coproducts_disjoint)
  have f4: "(right_coproj Ω Ω) ∘⇩c 𝗍 ≠ (left_coproj Ω Ω) ∘⇩c 𝖿"
    by (typecheck_cfuncs, metis (no_types) coproducts_disjoint)
  have f5: "(right_coproj Ω Ω) ∘⇩c 𝗍 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
    by (typecheck_cfuncs, metis cfunc_type_def monomorphism_def right_coproj_are_monomorphisms true_false_distinct)
  have f6: "(left_coproj Ω Ω) ∘⇩c 𝖿 ≠ (right_coproj Ω Ω) ∘⇩c 𝖿"
    by (typecheck_cfuncs, simp add: coproducts_disjoint)
  (*Upper limit*)
  have "{x. x ∈⇩c Ω ∐ Ω} = {(left_coproj Ω Ω) ∘⇩c 𝗍 , (right_coproj Ω Ω) ∘⇩c 𝗍, (left_coproj Ω Ω) ∘⇩c 𝖿, (right_coproj Ω Ω) ∘⇩c 𝖿}"
    using coprojs_jointly_surj true_false_only_truth_values 
    by (typecheck_cfuncs, auto) 
  then show "card {x. x ∈⇩c Ω ∐ Ω} = 4"
    by (simp add: f1 f2 f3 f4 f5 f6)
qed

end