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  XY" and
  right_proj_type[type_rule]: "right_coproj X Y : Y  XY" and
  cfunc_coprod_type[type_rule]: "f : X  Z  g : Y  Z  f⨿g :  XY  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 i0 i1 X Y  
    (i0 : X  W  i1 : Y  W 
    ( f g Z. (f : X  Z  g : Y  Z)  
      ( h. h :  W  Z  h c i0 = f  h c i1 = g 
        ( h2. (h2 : W  Z  h2 c i0 = f  h2 c i1 = g)  h2 = h))))"

lemma is_coprod_def2:
  assumes "i0 : X  W" "i1 : Y  W"
  shows "is_coprod W i0 i1 X Y  
    ( f g Z. (f : X  Z  g : Y  Z)  
      ( h. h :  W  Z  h c i0 = f  h c i1 = g 
        ( h2. (h2 : W  Z  h2 c i0 = f  h2 c i1 = 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, i0, i1) X Y"
  assumes W'_coprod: "is_coprod_triple (W', i'0, i'1) X Y"
  shows " g. g : W  W'  isomorphism g  g c i0  = i'0  g c i1 = i'1"
proof -
  obtain f where f_def: "f : W'  W  f c i'0  = i0  f c i'1 = i1"
    using W_coprod W'_coprod unfolding is_coprod_def
    by (metis split_pairs)

  obtain g where g_def: "g : W  W'  g c i0  = i'0  g c i1 = i'1"
    using W_coprod W'_coprod unfolding is_coprod_def
    by (metis split_pairs)

  have fg0: "(f c g) c  i0   = i0"
    by (metis W_coprod comp_associative2 f_def g_def is_coprod_def split_pairs)
  have fg1: "(f c g) c  i1   = i1"
    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 i0  = i0  h2 c i1 = i1)  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 i0 = i0  h2 c i1 = i1  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 i0  = i'0  g c i1 = 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:
  " xc 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]: "xc 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,idc (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,idc (X  Y)) c left_coproj X Y) c x = 
              eq_pred (X  Y) c z c β⇘X  Y,idc (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,idc (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,idc (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,idc (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,idc (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,idc (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:  "xc (𝟭  𝟭)"
  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 idc 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 idc 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 idc X,x c β⇘X) ⨿ (𝖿 c β⇘Y) c u"
    proof -
      have "(eq_pred X c idc X,x c β⇘X) ⨿ (𝖿 c β⇘Y) c left_coproj X Y c g
          = (eq_pred X c idc 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 idc X,x c β⇘X) ⨿ (𝖿 c β⇘Y) c u"  
    proof -
      have "(eq_pred X c idc X,x c β⇘X) ⨿ (𝖿 c β⇘Y) c u
          = (eq_pred X c idc 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 idc Y,y c β⇘Y) c u"
  proof -
    have "(𝖿 c β⇘X) ⨿ (eq_pred Y c idc Y,y c β⇘Y) c u
        = (𝖿 c β⇘X) ⨿ (eq_pred Y c idc Y,y c β⇘Y) c right_coproj X Y c y"
      using u_is_right_coproj by auto
    also have "... = (eq_pred Y c idc 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 idc 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 idc Y,y c β⇘Y) c u"
    proof -
      have "(𝖿 c β⇘X) ⨿ (eq_pred Y c idc Y,y c β⇘Y) c right_coproj X Y c g
          = (eq_pred Y c idc 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 idc Y,y c β⇘Y) c u"
    proof -
      have "(𝖿 c β⇘X) ⨿ (eq_pred Y c idc Y,y c β⇘Y) c u
          = (𝖿 c β⇘X) ⨿ (eq_pred Y c idc 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  idc X"
    using assms by (typecheck_cfuncs, simp add: cfunc_bowtie_prod_unique)

  have left_eq: " ((g f idc X) c (f f idc 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 idc X) c (f f idc 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= β⇘XY⇙"
  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 = idc Ω  x c 𝗍 ⨿ 𝖿 = idc (𝟭  𝟭)"
    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 = idc Ω"
  assume "x c 𝗍 ⨿ 𝖿 = idc (𝟭  𝟭)" "y c 𝗍 ⨿ 𝖿 = idc (𝟭  𝟭)"
  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 ((idc A ×f left_coproj B C) ⨿ (idc 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 ((idc A ×f left_coproj B C) ⨿ (idc A ×f right_coproj B C))"
      by (typecheck_cfuncs, simp add: cfunc_type_def)
    show "x. x c domain ((idc A ×f left_coproj B C) ⨿ (idc A ×f right_coproj B C)) 
             (idc A ×f left_coproj B C) ⨿ (idc 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 ((idc A ×f left_coproj B C) ⨿ (idc 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 ((idc A ×f left_coproj B C) ⨿ (idc A ×f right_coproj B C)) 
        (idc A ×f left_coproj B C) ⨿ (idc 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 ((idc A ×f left_coproj B C) ⨿ (idc 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 ((idc A ×f left_coproj B C) ⨿ (idc A ×f right_coproj B C)) 
        (idc A ×f left_coproj B C) ⨿ (idc 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 = idc ((A ×c B)  A ×c C) 
        factor_prod_coprod_left A B C c x = idc (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 = idc ((A ×c B)  A ×c C)" and
        inv_right: "factor_prod_coprod_left A B C c inv = idc (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 = idc ((A ×c B)  A ×c C)"
    and "y c factor_prod_coprod_left A B C = idc ((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 idc (A ×c B  C) = y c idc (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 ⨿ mc"

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' = mc 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 "mc 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 "mc c x' = mc 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), mc)"
      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 = mc 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 = idc (domain m  (codomain m  (domain m, m))) 
        into_super m c x = idc (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 = idc (codomain m)" and "into_super m c y = idc (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), mc)"
    by (simp add: assms not_in_subset_in_complement)
  then obtain x where x_type: "x c Y  (X,m)" and x_def: "y = mc 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 mc = 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,idc 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,idc 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,idc 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,idc 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