Theory Pred_Logic

section ‹Predicate Logic Functions›

theory Pred_Logic
  imports Coproduct
begin

subsection ‹NOT›

definition NOT :: "cfunc" where
  "NOT = (THE χ. is_pullback 𝟭 𝟭 Ω Ω (β⇘𝟭⇙) 𝗍 𝖿 χ)"

lemma NOT_is_pullback:
  "is_pullback 𝟭 𝟭 Ω Ω (β⇘𝟭⇙) 𝗍 𝖿 NOT"
  unfolding NOT_def
  using characteristic_function_exists false_func_type element_monomorphism
  by (subst the1I2, auto)

lemma NOT_type[type_rule]:
  "NOT : Ω → Ω"
  using NOT_is_pullback unfolding is_pullback_def  by auto

lemma NOT_false_is_true:
  "NOT ∘c 𝖿 = 𝗍"
  using NOT_is_pullback unfolding is_pullback_def 
  by (metis cfunc_type_def id_right_unit id_type one_unique_element)

lemma NOT_true_is_false:
  "NOT ∘c 𝗍 = 𝖿"
proof(rule ccontr)
  assume "NOT ∘c 𝗍 ≠ 𝖿"
  then have "NOT ∘c 𝗍 = 𝗍"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have "𝗍 ∘c idc 𝟭 = NOT ∘c 𝗍"
    using id_right_unit2 true_func_type by auto
  then obtain j where j_type: "j ∈c 𝟭" and j_id: "β⇘𝟭⇙ ∘c j = idc 𝟭" and f_j_eq_t: "𝖿 ∘c j = 𝗍"
    using NOT_is_pullback unfolding is_pullback_def by (typecheck_cfuncs, blast)
  then have "j = idc 𝟭"
    using id_type one_unique_element by blast
  then have "𝖿 = 𝗍"
    using f_j_eq_t false_func_type id_right_unit2 by auto
  then show False
    using true_false_distinct by auto
qed
  
lemma NOT_is_true_implies_false:
  assumes "p ∈c Ω"
  shows "NOT ∘c p = 𝗍 ⟹ p = 𝖿"
  using NOT_true_is_false assms true_false_only_truth_values by fastforce

lemma NOT_is_false_implies_true:
  assumes "p ∈c Ω"
  shows "NOT ∘c p = 𝖿 ⟹ p = 𝗍"
  using NOT_false_is_true assms true_false_only_truth_values by fastforce

lemma double_negation:
  "NOT ∘c NOT =  id Ω"
  by (typecheck_cfuncs, smt (verit, del_insts) 
  NOT_false_is_true NOT_true_is_false cfunc_type_def comp_associative id_left_unit2 one_separator
  true_false_only_truth_values)

subsection ‹AND›

definition AND :: "cfunc" where
  "AND = (THE χ. is_pullback 𝟭 𝟭 (Ω ×c Ω) Ω (β⇘𝟭⇙) 𝗍 ⟨𝗍,𝗍⟩ χ)"

lemma AND_is_pullback:
  "is_pullback 𝟭 𝟭 (Ω ×c Ω) Ω (β⇘𝟭⇙) 𝗍 ⟨𝗍,𝗍⟩ AND"
  unfolding AND_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, subst the1I2, auto)

lemma AND_type[type_rule]:
  "AND : Ω ×c Ω → Ω"
  using AND_is_pullback unfolding is_pullback_def by auto

lemma AND_true_true_is_true:
  "AND ∘c ⟨𝗍,𝗍⟩ = 𝗍"
  using AND_is_pullback unfolding is_pullback_def
  by (metis cfunc_type_def id_right_unit id_type one_unique_element)

lemma AND_false_left_is_false:
  assumes "p ∈c Ω"
  shows "AND ∘c ⟨𝖿,p⟩ = 𝖿"
proof (rule ccontr)
  assume "AND ∘c ⟨𝖿,p⟩ ≠ 𝖿"
  then have "AND ∘c ⟨𝖿,p⟩ = 𝗍"
    using assms true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have "𝗍 ∘c id 𝟭 = AND ∘c ⟨𝖿,p⟩"
    using assms by (typecheck_cfuncs, simp add: id_right_unit2)
  then obtain j where j_type: "j ∈c 𝟭" and j_id: "β⇘𝟭⇙ ∘c j = idc 𝟭" and tt_j_eq_fp: "⟨𝗍,𝗍⟩ ∘c j = ⟨𝖿,p⟩"
    using AND_is_pullback assms unfolding is_pullback_def by (typecheck_cfuncs, blast)
  then have "j = idc 𝟭"
    using id_type one_unique_element by auto
  then have "⟨𝗍,𝗍⟩ = ⟨𝖿,p⟩"
    by (typecheck_cfuncs, metis tt_j_eq_fp id_right_unit2)
  then have "𝗍 = 𝖿"
    using assms cart_prod_eq2 by (typecheck_cfuncs, auto)
  then show False
    using true_false_distinct by auto
qed

lemma AND_false_right_is_false:
  assumes "p ∈c Ω"
  shows "AND ∘c ⟨p,𝖿⟩ = 𝖿"
proof(rule ccontr)
  assume "AND ∘c ⟨p,𝖿⟩ ≠ 𝖿"
  then have "AND ∘c ⟨p,𝖿⟩ = 𝗍"
    using assms true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have "𝗍 ∘c id 𝟭 = AND ∘c ⟨p,𝖿⟩"
    using assms by (typecheck_cfuncs, simp add: id_right_unit2)
  then obtain j where j_type: "j ∈c 𝟭" and j_id: "β⇘𝟭⇙ ∘c j = idc 𝟭" and tt_j_eq_fp: "⟨𝗍,𝗍⟩ ∘c j = ⟨p,𝖿⟩"
    using AND_is_pullback assms unfolding is_pullback_def by (typecheck_cfuncs, blast)
  then have "j = idc 𝟭"
    using id_type one_unique_element by auto
  then have "⟨𝗍,𝗍⟩ = ⟨p,𝖿⟩"
    by (typecheck_cfuncs, metis tt_j_eq_fp id_right_unit2)
  then have "𝗍 = 𝖿"
    using assms cart_prod_eq2 by (typecheck_cfuncs, auto)
  then show "False"
    using true_false_distinct by auto
qed

lemma AND_commutative:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "AND ∘c ⟨p,q⟩ = AND ∘c ⟨q,p⟩"
  by (metis AND_false_left_is_false AND_false_right_is_false assms true_false_only_truth_values)

lemma AND_idempotent:
  assumes "p ∈c Ω"
  shows "AND ∘c ⟨p,p⟩ = p"
  using AND_false_right_is_false AND_true_true_is_true assms true_false_only_truth_values by blast

lemma AND_associative:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  assumes "r ∈c Ω"
  shows "AND ∘c ⟨AND ∘c ⟨p,q⟩, r⟩ = AND ∘c ⟨p, AND ∘c ⟨q,r⟩⟩"
  by (metis AND_commutative AND_false_left_is_false AND_true_true_is_true assms true_false_only_truth_values)

lemma AND_complementary:
  assumes "p ∈c Ω"
  shows "AND ∘c ⟨p, NOT ∘c p⟩ =  𝖿"
  by (metis AND_false_left_is_false AND_false_right_is_false NOT_false_is_true NOT_true_is_false assms true_false_only_truth_values true_func_type)

subsection ‹NOR›

definition NOR :: "cfunc" where
  "NOR = (THE χ. is_pullback  𝟭 𝟭 (Ω ×c Ω) Ω (β⇘𝟭⇙) 𝗍 ⟨𝖿, 𝖿⟩ χ)"

lemma NOR_is_pullback:
  "is_pullback  𝟭 𝟭 (Ω ×c Ω) Ω (β⇘𝟭⇙) 𝗍 ⟨𝖿, 𝖿⟩ NOR"
  unfolding NOR_def
  using characteristic_function_exists element_monomorphism
  by (typecheck_cfuncs, simp add: the1I2)

lemma NOR_type[type_rule]:
  "NOR : Ω ×c Ω → Ω"
  using NOR_is_pullback unfolding is_pullback_def by auto

lemma NOR_false_false_is_true:
  "NOR ∘c ⟨𝖿,𝖿⟩ = 𝗍"
  using NOR_is_pullback unfolding is_pullback_def 
  by (auto, metis cfunc_type_def id_right_unit id_type one_unique_element)

lemma NOR_left_true_is_false:
  assumes "p ∈c Ω"
  shows "NOR ∘c ⟨𝗍,p⟩ = 𝖿"
proof (rule ccontr)
  assume "NOR ∘c ⟨𝗍,p⟩ ≠ 𝖿"
  then have "NOR ∘c ⟨𝗍,p⟩ = 𝗍"
    using assms true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have "NOR ∘c ⟨𝗍,p⟩ = 𝗍 ∘c id 𝟭"
    using id_right_unit2 true_func_type by auto
  then obtain j where j_type: "j ∈c 𝟭" and j_id: "β⇘𝟭⇙ ∘c j = id 𝟭" and ff_j_eq_tp: "⟨𝖿,𝖿⟩ ∘c j = ⟨𝗍,p⟩"
    using NOR_is_pullback assms unfolding is_pullback_def by (typecheck_cfuncs, metis)
  then have "j = id 𝟭"
    using id_type one_unique_element by blast
  then have "⟨𝖿,𝖿⟩ = ⟨𝗍,p⟩"
    using cfunc_prod_comp false_func_type ff_j_eq_tp id_right_unit2 j_type by auto
  then have "𝖿 = 𝗍"
    using assms cart_prod_eq2 false_func_type true_func_type by auto
  then show False
    using true_false_distinct by auto
qed

lemma NOR_right_true_is_false:
  assumes "p ∈c Ω"
  shows "NOR ∘c ⟨p,𝗍⟩ = 𝖿"
proof (rule ccontr)
  assume "NOR ∘c ⟨p,𝗍⟩ ≠ 𝖿"
  then have "NOR ∘c ⟨p,𝗍⟩ = 𝗍"
    using assms true_false_only_truth_values by (typecheck_cfuncs, blast)
  then have "NOR ∘c ⟨p,𝗍⟩ = 𝗍 ∘c id 𝟭"
    using id_right_unit2 true_func_type by auto
  then obtain j where j_type: "j ∈c 𝟭" and j_id: "β⇘𝟭⇙ ∘c j = id 𝟭" and ff_j_eq_tp: "⟨𝖿,𝖿⟩ ∘c j = ⟨p,𝗍⟩"
    using NOR_is_pullback assms unfolding is_pullback_def by (typecheck_cfuncs, metis)
  then have "j = id 𝟭"
    using id_type one_unique_element by blast
  then have "⟨𝖿,𝖿⟩ = ⟨p,𝗍⟩"
    using cfunc_prod_comp false_func_type ff_j_eq_tp id_right_unit2 j_type by auto
  then have "𝖿 = 𝗍"
    using assms cart_prod_eq2 false_func_type true_func_type by auto
  then show False
    using true_false_distinct by auto
qed

lemma NOR_true_implies_both_false:
  assumes X_nonempty: "nonempty X" and Y_nonempty: "nonempty Y"
  assumes P_Q_types[type_rule]: "P : X → Ω" "Q : Y → Ω"
  assumes NOR_true: "NOR ∘c (P ×f Q) = 𝗍 ∘c β⇘X ×c Y⇙"
  shows "P = 𝖿 ∘c β⇘X⇙ ∧ Q = 𝖿 ∘c β⇘Y⇙"
proof -
  obtain z where z_type[type_rule]: "z : X ×c Y → 𝟭" and "P ×f Q = ⟨𝖿,𝖿⟩ ∘c z"
    using NOR_is_pullback NOR_true unfolding is_pullback_def
    by (metis P_Q_types cfunc_cross_prod_type terminal_func_type) 
  then have "P ×f Q = ⟨𝖿,𝖿⟩ ∘c β⇘X ×c Y⇙"
    using terminal_func_unique by auto
  then have "P ×f Q = ⟨𝖿 ∘c β⇘X ×c Y⇙, 𝖿 ∘c β⇘X ×c Y⇙⟩"
    by (typecheck_cfuncs, simp add: cfunc_prod_comp)
  then have "P ×f Q = ⟨𝖿 ∘c β⇘X⇙ ∘c left_cart_proj X Y, 𝖿 ∘c β⇘Y⇙ ∘c right_cart_proj X Y⟩"
    by (typecheck_cfuncs_prems, metis left_cart_proj_type right_cart_proj_type terminal_func_comp)
  then have "⟨P ∘c left_cart_proj X Y, Q ∘c right_cart_proj X Y⟩
      = ⟨𝖿 ∘c β⇘X⇙ ∘c left_cart_proj X Y, 𝖿 ∘c β⇘Y⇙ ∘c right_cart_proj X Y⟩"
    by (typecheck_cfuncs, unfold cfunc_cross_prod_def2, auto)
  then have "P ∘c left_cart_proj X Y = (𝖿 ∘c β⇘X⇙) ∘c left_cart_proj X Y
      ∧ Q ∘c right_cart_proj X Y = (𝖿 ∘c β⇘Y⇙) ∘c right_cart_proj X Y"
    using  cart_prod_eq2 by (typecheck_cfuncs, auto simp add: comp_associative2)
  then have eqs: "P = 𝖿 ∘c β⇘X⇙ ∧ Q = 𝖿 ∘c β⇘Y⇙"
    using assms epimorphism_def3 nonempty_left_imp_right_proj_epimorphism nonempty_right_imp_left_proj_epimorphism
    by (typecheck_cfuncs_prems, blast)
  then have "P ≠ 𝗍 ∘c β⇘X⇙ ∧ Q ≠ 𝗍 ∘c β⇘Y⇙"
  proof safe
    show "𝖿 ∘c β⇘X⇙ = 𝗍 ∘c β⇘X⇙ ⟹ False"
      by (typecheck_cfuncs_prems, smt X_nonempty comp_associative2 nonempty_def one_separator_contrapos terminal_func_comp terminal_func_unique true_false_distinct)
    show "𝖿 ∘c β⇘Y⇙ = 𝗍 ∘c β⇘Y⇙ ⟹ False"
      by (typecheck_cfuncs_prems, smt Y_nonempty comp_associative2 nonempty_def one_separator_contrapos terminal_func_comp terminal_func_unique true_false_distinct)
  qed
  then show ?thesis
    using eqs by linarith
qed

lemma NOR_true_implies_neither_true:
  assumes X_nonempty: "nonempty X" and Y_nonempty: "nonempty Y"
  assumes P_Q_types[type_rule]: "P : X → Ω" "Q : Y → Ω"
  assumes NOR_true: "NOR ∘c (P ×f Q) = 𝗍 ∘c β⇘X ×c Y⇙"
  shows "¬ (P = 𝗍 ∘c β⇘X⇙ ∨ Q = 𝗍 ∘c β⇘Y⇙)"
  by (smt (verit, ccfv_SIG) NOR_true NOT_false_is_true NOT_true_is_false NOT_type X_nonempty Y_nonempty assms(3,4) comp_associative2 comp_type nonempty_def terminal_func_type true_false_distinct true_false_only_truth_values NOR_true_implies_both_false)

subsection ‹OR›

definition OR :: "cfunc" where
  "OR = (THE χ. is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) χ)"

lemma pre_OR_type[type_rule]: 
  "⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) : 𝟭∐(𝟭∐𝟭) → Ω ×c Ω"
  by typecheck_cfuncs

lemma set_three: 
  "{x. x ∈c (𝟭∐(𝟭∐𝟭))} = {
 (left_coproj 𝟭 (𝟭∐𝟭)) , 
 (right_coproj 𝟭 (𝟭∐𝟭) ∘c left_coproj 𝟭 𝟭), 
  right_coproj 𝟭 (𝟭∐𝟭) ∘c(right_coproj 𝟭 𝟭)}"
  by(typecheck_cfuncs, safe, typecheck_cfuncs, smt (z3) comp_associative2 coprojs_jointly_surj one_unique_element)

lemma set_three_card: 
 "card {x. x ∈c (𝟭∐(𝟭∐𝟭))} = 3"
proof - 
  have f1: "left_coproj 𝟭 (𝟭 ∐ 𝟭) ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
    by (typecheck_cfuncs, metis cfunc_type_def coproducts_disjoint id_right_unit id_type)
  have f2: "left_coproj 𝟭 (𝟭 ∐ 𝟭) ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c right_coproj 𝟭 𝟭"
    by (typecheck_cfuncs, metis cfunc_type_def coproducts_disjoint id_right_unit id_type)
  have f3: "right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭 ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c right_coproj 𝟭 𝟭"
    by (typecheck_cfuncs, metis cfunc_type_def coproducts_disjoint monomorphism_def one_unique_element right_coproj_are_monomorphisms)
  show ?thesis
    by (simp add: f1 f2 f3 set_three)
qed

lemma pre_OR_injective:
  "injective(⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩))"
  unfolding injective_def
proof(clarify)
  fix x y 
  assume "x ∈c domain (⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have x_type: "x ∈c (𝟭∐(𝟭∐𝟭))"  
    using cfunc_type_def pre_OR_type by force
  then have x_form: "(∃ w. (w ∈c 𝟭 ∧ x = (left_coproj 𝟭 (𝟭∐𝟭)) ∘c w))
      ∨  (∃ w. (w ∈c (𝟭∐𝟭) ∧ x = (right_coproj 𝟭 (𝟭∐𝟭)) ∘c w))"
    using coprojs_jointly_surj by auto

  assume "y ∈c domain (⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have y_type: "y ∈c (𝟭∐(𝟭∐𝟭))"  
    using cfunc_type_def pre_OR_type by force
  then have y_form: "(∃ w. (w ∈c 𝟭 ∧ y = (left_coproj 𝟭 (𝟭∐𝟭)) ∘c w))
      ∨  (∃ w. (w ∈c (𝟭∐𝟭) ∧ y = (right_coproj 𝟭 (𝟭∐𝟭)) ∘c w))"
    using coprojs_jointly_surj by auto

  assume mx_eqs_my: "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c x = ⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c y"

  have f1: "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 (𝟭 ∐ 𝟭) = ⟨𝗍,𝗍⟩"
    by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
  have f2: "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭) = ⟨𝗍,𝖿⟩"
  proof- 
    have "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭) = 
          (⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭) )∘c left_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝗍,𝖿⟩"
      by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
    finally show ?thesis.
  qed
  have f3: "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭) = ⟨𝖿,𝗍⟩"
  proof- 
    have "⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭) = 
          (⟨𝗍,𝗍⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭) )∘c right_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝖿,𝗍⟩"
      by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
    finally show ?thesis.
  qed
  show "x = y"
  proof(cases "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)")
    assume case1: "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then show "x = y"
      by (typecheck_cfuncs, smt (z3) mx_eqs_my element_pair_eq f1 f2 f3 false_func_type maps_into_1u1 terminal_func_unique true_false_distinct true_func_type x_form y_form)
  next
    assume not_case1: "x ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "x = (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭)∨ 
               x = right_coproj 𝟭 (𝟭∐𝟭) ∘c(right_coproj 𝟭 𝟭)"
      by (metis id_right_unit2 id_type left_proj_type maps_into_1u1 terminal_func_unique x_form)
    show "x = y"
    proof(cases "x = (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭)")
      assume case2: "x = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then show "x = y"
        by (typecheck_cfuncs, smt (z3) cart_prod_eq2 case2 f1 f2 f3 false_func_type id_right_unit2 left_proj_type maps_into_1u1 mx_eqs_my terminal_func_comp terminal_func_comp_elem terminal_func_unique true_false_distinct true_func_type y_form)        
    next
      assume not_case2: "x ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "x = right_coproj 𝟭 (𝟭∐𝟭) ∘c(right_coproj 𝟭 𝟭)"
        using case2_or_3 by blast
      then show "x = y"
        by (smt (verit, best) f1 f2 f3  NOR_false_false_is_true NOR_is_pullback case3 cfunc_prod_comp comp_associative2 element_pair_eq false_func_type is_pullback_def left_proj_type maps_into_1u1 mx_eqs_my pre_OR_type terminal_func_unique true_false_distinct true_func_type y_form)
    qed
  qed
qed

lemma OR_is_pullback:
  "is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) OR"
  unfolding OR_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, simp add: the1I2 injective_imp_monomorphism pre_OR_injective)
      
lemma OR_type[type_rule]:
  "OR : Ω ×c Ω → Ω"
  unfolding OR_def
  by (metis OR_def OR_is_pullback is_pullback_def) 

lemma OR_true_left_is_true:
  assumes "p ∈c Ω"
  shows "OR ∘c ⟨𝗍,p⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝗍,p⟩"
    by (typecheck_cfuncs, smt (z3) assms comp_associative2 comp_type left_coproj_cfunc_coprod
        left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (typecheck_cfuncs, smt (verit, ccfv_SIG)  NOT_false_is_true NOT_is_pullback OR_is_pullback
        comp_associative2 is_pullback_def terminal_func_comp)
qed

lemma OR_true_right_is_true:
  assumes "p ∈c Ω"
  shows "OR ∘c ⟨p,𝗍⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ⟨p,𝗍⟩"
    by (typecheck_cfuncs, smt (z3) assms comp_associative2 comp_type left_coproj_cfunc_coprod
        left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) NOT_false_is_true NOT_is_pullback OR_is_pullback
        comp_associative2 is_pullback_def  terminal_func_comp)
qed

lemma OR_false_false_is_false:
  "OR ∘c ⟨𝖿,𝖿⟩ = 𝖿"
proof(rule ccontr)
  assume "OR ∘c ⟨𝖿,𝖿⟩ ≠ 𝖿"
  then have "OR ∘c ⟨𝖿,𝖿⟩ = 𝗍"
    using  true_false_only_truth_values by (typecheck_cfuncs, blast)
  then obtain j where  j_type[type_rule]: "j ∈c 𝟭∐(𝟭∐𝟭)" and j_def: "(⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝖿,𝖿⟩"
    using  OR_is_pullback unfolding is_pullback_def 
    by (typecheck_cfuncs, metis id_right_unit2 id_type)
  have trichotomy: "(⟨𝗍, 𝗍⟩ = ⟨𝖿,𝖿⟩) ∨ ((⟨𝗍, 𝖿⟩ = ⟨𝖿,𝖿⟩) ∨ (⟨𝖿, 𝗍⟩ = ⟨𝖿,𝖿⟩))"
  proof(cases "j = left_coproj 𝟭 (𝟭 ∐ 𝟭)")
    assume case1: "j = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then show ?thesis
      using case1 cfunc_coprod_type j_def left_coproj_cfunc_coprod by (typecheck_cfuncs, force)
  next
    assume not_case1: "j ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "j = right_coproj 𝟭 (𝟭∐𝟭) ∘c left_coproj 𝟭 𝟭   ∨ 
                           j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
      using not_case1 set_three by (typecheck_cfuncs, auto)
    show ?thesis
    proof(cases "j = (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭)")
      assume case2: "j = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      have "⟨𝗍, 𝖿⟩ = ⟨𝖿,𝖿⟩"
      proof - 
        have "(⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ((⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭)) ∘c left_coproj 𝟭 𝟭"
          by (typecheck_cfuncs, simp add: case2 comp_associative2)
        also have "... = (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c left_coproj 𝟭 𝟭"
          using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨𝗍, 𝖿⟩"
          by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
        finally show ?thesis
          using j_def by simp
      qed
      then show ?thesis
        by blast
    next
      assume not_case2: "j ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
        using case2_or_3 by blast
      have "⟨𝖿, 𝗍⟩ = ⟨𝖿,𝖿⟩"
      proof - 
        have "(⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ((⟨𝗍, 𝗍⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭)) ∘c right_coproj 𝟭 𝟭"
          by (typecheck_cfuncs, simp add: case3 comp_associative2)
        also have "... = (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c right_coproj 𝟭 𝟭"
          using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨𝖿, 𝗍⟩"
          by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
        finally show ?thesis
          using j_def by simp
      qed
      then show ?thesis
        by blast
    qed
  qed
    then have "𝗍 = 𝖿"
      using trichotomy cart_prod_eq2 by (typecheck_cfuncs, force)
    then show False
      using true_false_distinct by smt
qed

lemma OR_true_implies_one_is_true:
  assumes "p ∈c Ω" 
  assumes "q ∈c Ω"
  assumes "OR ∘c ⟨p,q⟩ = 𝗍"
  shows "(p = 𝗍) ∨ (q = 𝗍)"
  by (metis OR_false_false_is_false assms true_false_only_truth_values)

lemma NOT_NOR_is_OR:
 "OR = NOT ∘c NOR"
proof(etcs_rule one_separator)
  fix x 
  assume x_type[type_rule]: "x ∈c Ω ×c Ω"
  then obtain p q where p_type[type_rule]: "p ∈c Ω" and q_type[type_rule]:  "q ∈c Ω" and x_def: "x = ⟨p,q⟩"
    by (meson cart_prod_decomp)
  show "OR ∘c x = (NOT ∘c NOR) ∘c x"
  proof(cases "p = 𝗍")
    show "p = 𝗍 ⟹ OR ∘c x = (NOT ∘c NOR) ∘c x"
      by (typecheck_cfuncs, metis NOR_left_true_is_false NOT_false_is_true OR_true_left_is_true comp_associative2 q_type x_def)
  next
    assume "p ≠ 𝗍"
    then have "p = 𝖿"
      using p_type true_false_only_truth_values by blast
    show "OR ∘c x = (NOT ∘c NOR) ∘c x"
    proof(cases "q = 𝗍")
      show "q = 𝗍 ⟹ OR ∘c x = (NOT ∘c NOR) ∘c x"
        by (typecheck_cfuncs, metis NOR_right_true_is_false NOT_false_is_true OR_true_right_is_true 
            cfunc_type_def comp_associative p_type x_def)
    next
      assume "q ≠ 𝗍"
      then show ?thesis
        by (typecheck_cfuncs,metis NOR_false_false_is_true NOT_is_true_implies_false OR_false_false_is_false
            ‹p = 𝖿›  comp_associative2 q_type true_false_only_truth_values x_def)
    qed
  qed
qed

lemma OR_commutative:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "OR ∘c ⟨p,q⟩ = OR ∘c ⟨q,p⟩"
  by (metis OR_true_left_is_true OR_true_right_is_true assms true_false_only_truth_values)

lemma OR_idempotent:
  assumes "p ∈c Ω"
  shows "OR ∘c ⟨p,p⟩ = p"
  using OR_false_false_is_false OR_true_left_is_true assms true_false_only_truth_values by blast

lemma OR_associative:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  assumes "r ∈c Ω"
  shows "OR ∘c ⟨OR ∘c ⟨p,q⟩, r⟩ = OR ∘c ⟨p, OR ∘c ⟨q,r⟩⟩"
  by (metis OR_commutative OR_false_false_is_false OR_true_right_is_true assms true_false_only_truth_values)

lemma OR_complementary:
  assumes "p ∈c Ω"
  shows "OR ∘c ⟨p, NOT ∘c p⟩ =  𝗍"
  by (metis NOT_false_is_true NOT_true_is_false OR_true_left_is_true OR_true_right_is_true assms false_func_type true_false_only_truth_values)

subsection ‹XOR›

definition XOR :: "cfunc" where
  "XOR = (THE χ. is_pullback (𝟭∐𝟭) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐𝟭)⇙) 𝗍 (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) χ)"

lemma pre_XOR_type[type_rule]: 
  "⟨𝗍, 𝖿⟩ ⨿ ⟨𝖿, 𝗍⟩ : 𝟭∐𝟭 → Ω ×c Ω"
  by typecheck_cfuncs

lemma pre_XOR_injective:
 "injective(⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)"
 unfolding injective_def
proof(clarify)
  fix x y 
  assume "x ∈c domain (⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have x_type: "x ∈c 𝟭∐𝟭"  
    using cfunc_type_def pre_XOR_type by force
  then have x_form: "(∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w)
                  ∨  (∃ w. w ∈c 𝟭 ∧ x = right_coproj 𝟭 𝟭 ∘c w)"
    using coprojs_jointly_surj by auto

  assume "y ∈c domain (⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have y_type: "y ∈c 𝟭∐𝟭"  
    using cfunc_type_def pre_XOR_type by force
  then have y_form: "(∃ w. w ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c w)
                 ∨  (∃ w. w ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c w)"
    using coprojs_jointly_surj by auto

  assume eqs: "⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c x = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c y"

  show "x = y"
  proof(cases "∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w")
    assume a1: "∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
    then obtain w where x_def: "w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
      by blast
    then have w_is: "w = id(𝟭)"
      by (typecheck_cfuncs, metis terminal_func_unique x_def)
    have "∃ v. v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
    proof(rule ccontr)
      assume a2: "∄v. v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
      then obtain v where y_def:  "v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
        using y_form by (typecheck_cfuncs, blast)
      then have v_is: "v = id(𝟭)"
        by (typecheck_cfuncs, metis terminal_func_unique y_def)
      then have "⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 𝟭 = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 𝟭"
        using w_is eqs id_right_unit2 x_def y_def by (typecheck_cfuncs, force)
      then have "⟨𝗍,𝖿⟩ = ⟨𝖿,𝗍⟩"
        by (typecheck_cfuncs, smt (z3) cfunc_coprod_unique coprod_eq2 pre_XOR_type right_coproj_cfunc_coprod)      
      then have "𝗍 = 𝖿 ∧ 𝖿 = 𝗍"
        using cart_prod_eq2 false_func_type true_func_type by blast
      then show False
        using true_false_distinct by blast
    qed
    then obtain v where y_def: "v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
      by blast
    then have "v = id(𝟭)"
      by (typecheck_cfuncs, metis terminal_func_unique)
    then show ?thesis
      by (simp add: w_is x_def y_def)
  next
    assume "∄w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
    then obtain w where x_def: "w ∈c 𝟭 ∧ x = right_coproj 𝟭 𝟭 ∘c w"
      using x_form by force
    then have w_is: "w = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique x_def)
    have "∃ v. v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
    proof(rule ccontr)
      assume a2: "∄v. v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
      then obtain v where y_def:  "v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
        using y_form by (typecheck_cfuncs, blast)
      then have "v = id 𝟭"
        by (typecheck_cfuncs, metis terminal_func_unique y_def)
      then have "⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 𝟭 = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 𝟭"
        using w_is eqs id_right_unit2 x_def y_def by (typecheck_cfuncs, force)
      then have "⟨𝗍,𝖿⟩ = ⟨𝖿,𝗍⟩"
        by (typecheck_cfuncs, smt (z3)  cfunc_coprod_unique coprod_eq2 pre_XOR_type right_coproj_cfunc_coprod)      
      then have "𝗍 = 𝖿 ∧ 𝖿 = 𝗍"
        using cart_prod_eq2 false_func_type true_func_type by blast
      then show False
        using true_false_distinct by blast
    qed
    then obtain v where y_def: "v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
      by blast
    then have "v = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique)
    then show ?thesis
      by (simp add: w_is x_def y_def)
  qed
qed

lemma XOR_is_pullback:
  "is_pullback (𝟭∐𝟭) 𝟭 (Ω ×c Ω) Ω (β⇘(𝟭∐𝟭)⇙) 𝗍 (⟨𝗍, 𝖿⟩ ⨿ ⟨𝖿, 𝗍⟩) XOR"
  unfolding XOR_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, simp add: the1I2 injective_imp_monomorphism pre_XOR_injective)
      
lemma XOR_type[type_rule]:
  "XOR : Ω ×c Ω → Ω"
  unfolding XOR_def
  by (metis XOR_def XOR_is_pullback is_pullback_def)

lemma XOR_only_true_left_is_true:
  "XOR ∘c  ⟨𝗍,𝖿⟩ = 𝗍"
proof -   
  have "∃ j. j ∈c 𝟭∐𝟭 ∧ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝗍,𝖿⟩"
    by (typecheck_cfuncs, meson left_coproj_cfunc_coprod left_proj_type)
  then show ?thesis
    by (smt (verit, best) XOR_is_pullback comp_associative2 id_right_unit2 is_pullback_def terminal_func_comp_elem)
qed

lemma XOR_only_true_right_is_true:
  "XOR ∘c  ⟨𝖿,𝗍⟩ = 𝗍"
proof -   
  have "∃ j. j ∈c 𝟭∐𝟭 ∧ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝖿,𝗍⟩"
    by (typecheck_cfuncs, meson right_coproj_cfunc_coprod right_proj_type)
  then show ?thesis
    by (smt (verit, best) XOR_is_pullback  comp_associative2 id_right_unit2 is_pullback_def terminal_func_comp_elem)
qed

lemma XOR_false_false_is_false:
   "XOR ∘c  ⟨𝖿,𝖿⟩ = 𝖿"
proof(rule ccontr)
  assume "XOR ∘c ⟨𝖿,𝖿⟩ ≠ 𝖿"
  then have "XOR ∘c ⟨𝖿,𝖿⟩  = 𝗍"
    by (metis NOR_is_pullback XOR_type comp_type is_pullback_def  true_false_only_truth_values)
  then obtain j where j_def: "j ∈c 𝟭∐𝟭 ∧ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝖿,𝖿⟩"
    by (typecheck_cfuncs, auto, smt (verit, ccfv_threshold) XOR_is_pullback id_right_unit2 id_type is_pullback_def)
  show False
  proof(cases "j = left_coproj 𝟭 𝟭")
    assume "j = left_coproj 𝟭 𝟭"
    then have "(⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝗍, 𝖿⟩"
      using  left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝗍, 𝖿⟩ = ⟨𝖿,𝖿⟩"
      using j_def by auto
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  next
    assume "j ≠ left_coproj 𝟭 𝟭"
    then have "j = right_coproj 𝟭 𝟭"
      by (meson j_def maps_into_1u1)
    then have "(⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝖿, 𝗍⟩"
      using  right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝖿, 𝗍⟩ = ⟨𝖿,𝖿⟩"
      using j_def by auto
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  qed
qed

lemma XOR_true_true_is_false:
   "XOR ∘c  ⟨𝗍,𝗍⟩ = 𝖿"
proof(rule ccontr)
  assume "XOR ∘c ⟨𝗍,𝗍⟩ ≠ 𝖿"
  then have "XOR ∘c ⟨𝗍,𝗍⟩  = 𝗍"
    by (metis XOR_type comp_type diag_on_elements diagonal_type true_false_only_truth_values true_func_type)
  then obtain j where j_def: "j ∈c 𝟭∐𝟭 ∧ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝗍,𝗍⟩"
    by (typecheck_cfuncs, auto, smt (verit, ccfv_threshold) XOR_is_pullback id_right_unit2 id_type is_pullback_def)
  show False
  proof(cases "j = left_coproj 𝟭 𝟭")
    assume "j = left_coproj 𝟭 𝟭"
    then have "(⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝗍, 𝖿⟩"
      using  left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝗍, 𝖿⟩ = ⟨𝗍,𝗍⟩"
      using j_def by auto
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  next
    assume "j ≠ left_coproj 𝟭 𝟭"
    then have "j = right_coproj 𝟭 𝟭"
      by (meson j_def maps_into_1u1)
    then have "(⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c j  = ⟨𝖿, 𝗍⟩"
      using  right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝖿, 𝗍⟩ = ⟨𝗍,𝗍⟩"
      using j_def by auto
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  qed
qed

subsection ‹NAND›
definition NAND :: "cfunc" where
  "NAND = (THE χ. is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω ×c Ω) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) χ)"

lemma pre_NAND_type[type_rule]: 
  "⟨𝖿, 𝖿⟩ ⨿ (⟨𝗍, 𝖿⟩ ⨿ ⟨𝖿, 𝗍⟩) : 𝟭∐(𝟭∐𝟭) → Ω ×c Ω"
  by typecheck_cfuncs

lemma pre_NAND_injective:
  "injective(⟨𝖿, 𝖿⟩ ⨿ (⟨𝗍, 𝖿⟩ ⨿ ⟨𝖿, 𝗍⟩))"
  unfolding injective_def
proof(clarify)
  fix x y 
  assume x_type: "x ∈c domain (⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have x_type': "x ∈c 𝟭 ∐ (𝟭∐𝟭)"  
    using cfunc_type_def pre_NAND_type by force
  then have x_form: "(∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 (𝟭∐𝟭) ∘c w)
      ∨  (∃ w. w ∈c 𝟭∐𝟭 ∧ x = right_coproj 𝟭 (𝟭∐𝟭) ∘c w)"
    using coprojs_jointly_surj by auto

  assume y_type: "y ∈c domain (⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have y_type': "y ∈c 𝟭∐ (𝟭∐𝟭)"  
    using cfunc_type_def pre_NAND_type by force
  then have y_form: "(∃ w. w ∈c 𝟭 ∧ y = left_coproj 𝟭 (𝟭∐𝟭) ∘c w)
      ∨  (∃ w. w ∈c 𝟭∐𝟭 ∧ y = right_coproj 𝟭 (𝟭∐𝟭) ∘c w)"
    using coprojs_jointly_surj by auto

  assume mx_eqs_my: "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c x = ⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c y"

  have f1: "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 (𝟭 ∐ 𝟭) = ⟨𝖿, 𝖿⟩"
    by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
  have f2: "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭) ∘c left_coproj 𝟭 𝟭) = ⟨𝗍,𝖿⟩"
  proof- 
    have "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭) ∘c left_coproj 𝟭 𝟭 = 
          (⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭)) ∘c left_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝗍,𝖿⟩"
      by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
    finally show ?thesis.
  qed
  have f3: "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭) = ⟨𝖿,𝗍⟩"
  proof- 
    have "⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭) = 
          (⟨𝖿, 𝖿⟩ ⨿ ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭) )∘c right_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝗍,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝖿,𝗍⟩"
      by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
    finally show ?thesis.
  qed
  show "x = y"
  proof(cases "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)")
    assume case1: "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then show "x = y"
      by (typecheck_cfuncs, smt (z3) mx_eqs_my element_pair_eq f1 f2 f3 false_func_type maps_into_1u1 terminal_func_unique true_false_distinct true_func_type x_form y_form)
  next
    assume not_case1: "x ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "x = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭 ∨ 
               x = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
      by (metis id_right_unit2 id_type left_proj_type maps_into_1u1 terminal_func_unique x_form)
    show "x = y"
    proof(cases "x = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭")
      assume case2: "x = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then show "x = y"
        by (smt (z3) NOT_false_is_true NOT_is_pullback NOT_true_is_false NOT_type x_type x_type' cart_prod_eq2 case2 cfunc_type_def characteristic_func_eq characteristic_func_is_pullback characteristic_function_exists comp_associative diag_on_elements diagonal_type element_monomorphism f1 f2 f3 false_func_type left_proj_type maps_into_1u1 mx_eqs_my terminal_func_unique true_false_distinct true_func_type x_type y_form)
    next
      assume not_case2: "x ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "x = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
        using case2_or_3 by blast
      then show "x = y"
        by (smt (z3) NOT_false_is_true NOT_is_pullback NOT_true_is_false NOT_type x_type x_type' cart_prod_eq2 case3 cfunc_type_def characteristic_func_eq characteristic_func_is_pullback characteristic_function_exists comp_associative diag_on_elements diagonal_type element_monomorphism f1 f2 f3 false_func_type left_proj_type maps_into_1u1 mx_eqs_my terminal_func_unique true_false_distinct true_func_type x_type y_form)
    qed
  qed
qed

lemma NAND_is_pullback:
  "is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) NAND"
  unfolding NAND_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, simp add: the1I2 injective_imp_monomorphism pre_NAND_injective)
      
lemma NAND_type[type_rule]:
  "NAND : Ω ×c Ω → Ω"
  unfolding NAND_def
  by (metis NAND_def NAND_is_pullback is_pullback_def) 

lemma NAND_left_false_is_true:
  assumes "p ∈c Ω"
  shows "NAND ∘c ⟨𝖿,p⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝖿, 𝖿⟩ ⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝖿,p⟩"
    by (typecheck_cfuncs, smt (z3) assms comp_associative2 comp_type left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) NAND_is_pullback comp_associative2 id_right_unit2 is_pullback_def terminal_func_comp_elem)
qed

lemma NAND_right_false_is_true:
  assumes "p ∈c Ω"
  shows "NAND ∘c ⟨p,𝖿⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨p,𝖿⟩"
    by (typecheck_cfuncs, smt (z3) assms comp_associative2 comp_type left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) NAND_is_pullback NOT_false_is_true NOT_is_pullback  comp_associative2 is_pullback_def  terminal_func_comp)
qed

lemma NAND_true_true_is_false:
 "NAND ∘c ⟨𝗍,𝗍⟩ = 𝖿"
proof(rule ccontr)
  assume "NAND ∘c ⟨𝗍,𝗍⟩ ≠ 𝖿"
  then have "NAND ∘c ⟨𝗍,𝗍⟩ = 𝗍"
    using  true_false_only_truth_values by (typecheck_cfuncs, blast)
  then obtain j where j_type[type_rule]:  "j ∈c 𝟭∐(𝟭∐𝟭)" and j_def: "(⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝗍,𝗍⟩"
    using NAND_is_pullback unfolding is_pullback_def
    by (typecheck_cfuncs, smt (z3) NAND_is_pullback id_right_unit2 id_type)
  then have trichotomy: "(⟨𝖿,𝖿⟩ = ⟨𝗍,𝗍⟩) ∨ (⟨𝗍, 𝖿⟩ = ⟨𝗍,𝗍⟩) ∨ (⟨𝖿, 𝗍⟩ = ⟨𝗍,𝗍⟩)"
  proof(cases "j = left_coproj 𝟭 (𝟭 ∐ 𝟭)")
    assume case1: "j = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then show ?thesis
      by (metis cfunc_coprod_type cfunc_prod_type false_func_type j_def left_coproj_cfunc_coprod true_func_type)
  next
    assume not_case1: "j ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "j = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭 ∨ 
               j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
      using not_case1 set_three by (typecheck_cfuncs, auto)
    show ?thesis
    proof(cases "j = right_coproj 𝟭 (𝟭∐𝟭) ∘c left_coproj 𝟭 𝟭")
      assume case2: "j = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      have "⟨𝗍, 𝖿⟩ = ⟨𝗍,𝗍⟩"
      proof - 
        have "(⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ((⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭)) ∘c left_coproj 𝟭 𝟭"
          by (typecheck_cfuncs, simp add: case2 comp_associative2)
        also have "... = (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c left_coproj 𝟭 𝟭"
          using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨𝗍, 𝖿⟩"
          by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
        finally show ?thesis
          using j_def by simp
      qed
      then show ?thesis
        by blast
    next
      assume not_case2: "j ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
        using case2_or_3 by blast
      have "⟨𝖿, 𝗍⟩ = ⟨𝗍,𝗍⟩"
      proof - 
        have "(⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ((⟨𝖿, 𝖿⟩⨿ (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭)) ∘c right_coproj 𝟭 𝟭"
          by (typecheck_cfuncs, simp add: case3 comp_associative2)
        also have "... = (⟨𝗍, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩) ∘c right_coproj 𝟭 𝟭"
          using right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
        also have "... = ⟨𝖿, 𝗍⟩"
          by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
        finally show ?thesis
          using j_def by simp
      qed
      then show ?thesis
        by blast
    qed
  qed
    then have "𝗍 = 𝖿"
      using trichotomy cart_prod_eq2 by (typecheck_cfuncs, force)
    then show False
      using true_false_distinct by auto  
qed

lemma NAND_true_implies_one_is_false:
  assumes "p ∈c Ω" 
  assumes "q ∈c Ω"
  assumes "NAND ∘c ⟨p,q⟩ = 𝗍"
  shows "p = 𝖿 ∨ q = 𝖿"
  by (metis (no_types) NAND_true_true_is_false assms true_false_only_truth_values)

lemma NOT_AND_is_NAND:
 "NAND = NOT ∘c AND"
proof(etcs_rule one_separator)
  fix x 
  assume x_type: "x ∈c Ω ×c Ω"
  then obtain p q where x_def: "p ∈c Ω ∧ q ∈c Ω ∧ x = ⟨p,q⟩"
    by (meson cart_prod_decomp)
  show "NAND ∘c x = (NOT ∘c AND) ∘c x"
    by (typecheck_cfuncs, metis AND_false_left_is_false AND_false_right_is_false AND_true_true_is_true NAND_left_false_is_true NAND_right_false_is_true NAND_true_implies_one_is_false NOT_false_is_true NOT_true_is_false comp_associative2 true_false_only_truth_values x_def x_type)
qed

lemma NAND_not_idempotent:
  assumes "p ∈c Ω"
  shows "NAND ∘c ⟨p,p⟩ = NOT ∘c p"
  using NAND_right_false_is_true NAND_true_true_is_false NOT_false_is_true NOT_true_is_false assms true_false_only_truth_values by fastforce

subsection ‹IFF›

definition IFF :: "cfunc" where
  "IFF = (THE χ. is_pullback (𝟭∐𝟭) 𝟭 (Ω ×c Ω) Ω (β⇘(𝟭∐𝟭)⇙) 𝗍 (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) χ)"

lemma pre_IFF_type[type_rule]: 
  "⟨𝗍, 𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ : 𝟭∐𝟭 → Ω ×c Ω"
  by typecheck_cfuncs

lemma pre_IFF_injective:
 "injective(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩)"
 unfolding injective_def
proof(clarify)
  fix x y 
  assume "x ∈c domain (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩)" 
  then have x_type: "x ∈c (𝟭∐𝟭)"  
    using cfunc_type_def pre_IFF_type by force
  then have x_form: "(∃ w. (w ∈c 𝟭 ∧ x = (left_coproj 𝟭 𝟭) ∘c w))
      ∨  (∃ w. (w ∈c 𝟭 ∧ x = (right_coproj 𝟭 𝟭) ∘c w))"
    using coprojs_jointly_surj by auto

  assume "y ∈c domain (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩)" 
  then have y_type: "y ∈c (𝟭∐𝟭)"  
    using cfunc_type_def pre_IFF_type by force
  then have y_form: "(∃ w. (w ∈c 𝟭 ∧ y = (left_coproj 𝟭 𝟭) ∘c w))
      ∨  (∃ w. (w ∈c 𝟭 ∧ y = (right_coproj 𝟭 𝟭) ∘c w))"
    using coprojs_jointly_surj by auto

  assume eqs: "⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c x = ⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c y"

  show "x = y"
  proof(cases "∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w")
    assume a1: "∃ w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
    then obtain w where x_def: "w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
      by blast
    then have "w = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique x_def)
    have "∃ v. v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
    proof(rule ccontr)
      assume a2: "∄v. v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
      then obtain v where y_def:  "v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
        using y_form by (typecheck_cfuncs, blast)
      then have "v = id 𝟭"
        by (typecheck_cfuncs, metis terminal_func_unique y_def)
      then have "⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c left_coproj 𝟭 𝟭 = ⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c right_coproj 𝟭 𝟭"
        using ‹v = idc 𝟭› ‹w = idc 𝟭› eqs id_right_unit2 x_def y_def by (typecheck_cfuncs, force)
      then have "⟨𝗍, 𝗍⟩ = ⟨𝖿,𝖿⟩"
        by (typecheck_cfuncs, smt (z3)  cfunc_coprod_unique coprod_eq2 pre_IFF_type right_coproj_cfunc_coprod)      
      then have "𝗍 = 𝖿"
        using cart_prod_eq2 false_func_type true_func_type by blast
      then show False
        using true_false_distinct by blast
    qed
    then obtain v where y_def: "v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
      by blast
    then have "v = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique)
    then show ?thesis
      by (simp add: ‹w = idc 𝟭› x_def y_def)
  next
    assume "∄w. w ∈c 𝟭 ∧ x = left_coproj 𝟭 𝟭 ∘c w"
    then obtain w where x_def: "w ∈c 𝟭 ∧ x = right_coproj 𝟭 𝟭 ∘c w"
      using x_form by force
    then have "w = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique x_def)
    have "∃ v. v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
    proof(rule ccontr)
      assume a2: "∄v. v ∈c 𝟭 ∧ y = right_coproj 𝟭 𝟭 ∘c v"
      then obtain v where y_def:  "v ∈c 𝟭 ∧ y = left_coproj 𝟭 𝟭 ∘c v"
        using y_form by (typecheck_cfuncs, blast)
      then have "v = id 𝟭"
        by (typecheck_cfuncs, metis terminal_func_unique y_def)
      then have "⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c left_coproj 𝟭 𝟭 = ⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩ ∘c right_coproj 𝟭 𝟭"
        using ‹v = idc 𝟭› ‹w = idc 𝟭› eqs id_right_unit2 x_def y_def by (typecheck_cfuncs, force)
      then have "⟨𝗍, 𝗍⟩ = ⟨𝖿, 𝖿⟩"
        by (typecheck_cfuncs, smt (z3)  cfunc_coprod_unique coprod_eq2 pre_IFF_type right_coproj_cfunc_coprod)      
      then have "𝗍 = 𝖿"
        using cart_prod_eq2 false_func_type true_func_type by blast
      then show False
        using true_false_distinct by blast
    qed
    then obtain v where y_def: "v ∈c 𝟭 ∧ y = (right_coproj 𝟭 𝟭) ∘c v"
      by blast
    then have "v = id 𝟭"
      by (typecheck_cfuncs, metis terminal_func_unique)
    then show ?thesis
      by (simp add: ‹w = idc 𝟭› x_def y_def)
  qed
qed

lemma IFF_is_pullback:
  "is_pullback (𝟭∐𝟭) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐𝟭)⇙) 𝗍 (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) IFF"
  unfolding IFF_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, simp add: the1I2 injective_imp_monomorphism pre_IFF_injective)

lemma IFF_type[type_rule]:
  "IFF : Ω ×c Ω → Ω"
  unfolding IFF_def
  by (metis IFF_def IFF_is_pullback is_pullback_def)

lemma IFF_true_true_is_true:
 "IFF ∘c ⟨𝗍,𝗍⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c (𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝗍,𝗍⟩"
    by (typecheck_cfuncs, smt (z3)  comp_associative2 comp_type left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (smt (verit, ccfv_threshold) AND_is_pullback AND_true_true_is_true IFF_is_pullback comp_associative2 is_pullback_def  terminal_func_comp)
qed

lemma IFF_false_false_is_true:
 "IFF ∘c ⟨𝖿,𝖿⟩ = 𝗍"
proof - 
  have "∃ j. j ∈c (𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝖿,𝖿⟩"
    by (typecheck_cfuncs, smt (z3)  comp_associative2 comp_type left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type true_false_only_truth_values)
  then show ?thesis 
    by (smt (verit, ccfv_threshold) AND_is_pullback AND_true_true_is_true IFF_is_pullback comp_associative2 is_pullback_def  terminal_func_comp)
qed

lemma IFF_true_false_is_false:
 "IFF ∘c ⟨𝗍,𝖿⟩ = 𝖿"
proof(rule ccontr)
  assume "IFF ∘c ⟨𝗍,𝖿⟩ ≠ 𝖿"
  then have "IFF ∘c ⟨𝗍,𝖿⟩  = 𝗍"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)    
  then obtain j where j_type[type_rule]: "j ∈c 𝟭∐𝟭 ∧ (⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝗍,𝖿⟩"
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) IFF_is_pullback characteristic_function_exists element_monomorphism is_pullback_def)
  show False
  proof(cases "j = left_coproj 𝟭 𝟭")
    assume "j = left_coproj 𝟭 𝟭"
    then have "(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝗍, 𝗍⟩"
      using  left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝗍, 𝖿⟩ = ⟨𝗍,𝗍⟩"
      using  j_type by argo
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  next
    assume "j ≠ left_coproj 𝟭 𝟭"
    then have "j = right_coproj 𝟭 𝟭"
      using j_type maps_into_1u1 by auto
    then have "(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝖿, 𝖿⟩"
      using  right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝖿, 𝗍⟩ = ⟨𝖿, 𝖿⟩"
      using XOR_false_false_is_false XOR_only_true_left_is_true j_type by argo
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
 qed
qed

lemma IFF_false_true_is_false:
 "IFF ∘c ⟨𝖿,𝗍⟩ = 𝖿"
proof(rule ccontr)
  assume "IFF ∘c ⟨𝖿,𝗍⟩ ≠ 𝖿"
  then have "IFF ∘c ⟨𝖿,𝗍⟩  = 𝗍"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)
  then obtain j where j_type[type_rule]: "j ∈c 𝟭∐𝟭" and j_def:  "(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝖿,𝗍⟩"
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) IFF_is_pullback id_right_unit2 is_pullback_def one_unique_element terminal_func_comp terminal_func_comp_elem terminal_func_unique)
  show False
  proof(cases "j = left_coproj 𝟭 𝟭")
    assume "j = left_coproj 𝟭 𝟭"
    then have "(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝗍, 𝗍⟩"
      using  left_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝖿,𝗍⟩ = ⟨𝗍,𝗍⟩"
      using j_def by auto
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
  next
    assume "j ≠ left_coproj 𝟭 𝟭"
    then have "j = right_coproj 𝟭 𝟭"
      using j_type maps_into_1u1 by blast
    then have "(⟨𝗍, 𝗍⟩ ⨿⟨𝖿, 𝖿⟩) ∘c j  = ⟨𝖿, 𝖿⟩"
      using  right_coproj_cfunc_coprod by (typecheck_cfuncs, presburger)
    then have "⟨𝖿,𝗍⟩ = ⟨𝖿, 𝖿⟩"
      using XOR_false_false_is_false XOR_only_true_left_is_true j_def by fastforce
    then have "𝗍 = 𝖿"
      using cart_prod_eq2 false_func_type true_func_type by auto
    then show False
      using true_false_distinct by auto
 qed
qed

lemma NOT_IFF_is_XOR: 
  "NOT ∘c IFF = XOR"
proof(etcs_rule one_separator)
  fix x   
  assume x_type: "x ∈c Ω ×c Ω"
  then obtain u w where x_def: "u ∈c Ω ∧ w ∈c Ω ∧ x = ⟨u,w⟩"
    using cart_prod_decomp by blast
  show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
  proof(cases "u = 𝗍")
    show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
    proof(cases "w = 𝗍")
      show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
        by (metis IFF_false_false_is_true IFF_false_true_is_false IFF_true_false_is_false IFF_true_true_is_true IFF_type NOT_false_is_true NOT_true_is_false NOT_type XOR_false_false_is_false XOR_only_true_left_is_true XOR_only_true_right_is_true XOR_true_true_is_false cfunc_type_def comp_associative true_false_only_truth_values x_def x_type)
    next 
      assume "w ≠ 𝗍"
      then have "w = 𝖿"
        by (metis true_false_only_truth_values x_def)
      then show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
        by (metis IFF_false_false_is_true IFF_true_false_is_false IFF_type NOT_false_is_true NOT_true_is_false NOT_type XOR_false_false_is_false XOR_only_true_left_is_true comp_associative2 true_false_only_truth_values x_def x_type)
    qed
  next 
    assume "u ≠ 𝗍"
    then have "u = 𝖿"
      by (metis true_false_only_truth_values x_def)
    show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
    proof(cases "w = 𝗍")
      show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
        by (metis IFF_false_false_is_true IFF_false_true_is_false IFF_type NOT_false_is_true NOT_true_is_false NOT_type XOR_false_false_is_false XOR_only_true_right_is_true ‹u = 𝖿› comp_associative2 true_false_only_truth_values x_def x_type)
    next
      assume "w ≠ 𝗍"
      then have "w = 𝖿"
        by (metis true_false_only_truth_values x_def)
      then show "(NOT ∘c IFF) ∘c x = XOR ∘c x"
        by (metis IFF_false_false_is_true IFF_type NOT_true_is_false NOT_type XOR_false_false_is_false ‹u = 𝖿› cfunc_type_def comp_associative x_def x_type)
    qed
  qed
qed

subsection ‹IMPLIES›

definition IMPLIES :: "cfunc" where
  "IMPLIES = (THE χ. is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) χ)"

lemma pre_IMPLIES_type[type_rule]: 
  "⟨𝗍, 𝗍⟩ ⨿ (⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿, 𝗍⟩) : 𝟭 ∐ (𝟭 ∐ 𝟭) → Ω ×c Ω"
  by typecheck_cfuncs

lemma pre_IMPLIES_injective:
  "injective(⟨𝗍, 𝗍⟩ ⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩))"
  unfolding injective_def
proof(clarify)
  fix x y 
  assume a1: "x ∈c domain (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have x_type[type_rule]: "x ∈c (𝟭∐(𝟭∐𝟭))"  
    using cfunc_type_def pre_IMPLIES_type by force
  then have x_form: "(∃ w. (w ∈c 𝟭 ∧ x = (left_coproj 𝟭 (𝟭∐𝟭)) ∘c w))
      ∨  (∃ w. (w ∈c (𝟭∐𝟭) ∧ x = (right_coproj 𝟭 (𝟭∐𝟭)) ∘c w))"
    using coprojs_jointly_surj by auto

  assume "y ∈c domain (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)" 
  then have y_type: "y ∈c (𝟭∐(𝟭∐𝟭))"  
    using cfunc_type_def pre_IMPLIES_type by force
  then have y_form: "(∃ w. (w ∈c 𝟭 ∧ y = (left_coproj 𝟭 (𝟭∐𝟭)) ∘c w))
      ∨  (∃ w. (w ∈c (𝟭∐𝟭) ∧ y = (right_coproj 𝟭 (𝟭∐𝟭)) ∘c w))"
    using coprojs_jointly_surj by auto

  assume mx_eqs_my: "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c x = ⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c y"

  have f1: "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 (𝟭 ∐ 𝟭) = ⟨𝗍,𝗍⟩"
    by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
  have f2: "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭) = ⟨𝖿, 𝖿⟩"
  proof- 
    have "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭) = 
          (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭) )∘c left_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c left_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝖿, 𝖿⟩"
      by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
    finally show ?thesis.      
  qed
  have f3: "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c (right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭) = ⟨𝖿,𝗍⟩"
  proof- 
    have "⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭)∘c right_coproj 𝟭 𝟭 = 
          (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 (𝟭∐𝟭))∘c right_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ⟨𝖿, 𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c right_coproj 𝟭 𝟭"
      using right_coproj_cfunc_coprod by (typecheck_cfuncs, smt)
    also have "... = ⟨𝖿,𝗍⟩"
      by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
    finally show ?thesis.
  qed
  show "x = y"
  proof(cases "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)")
    assume case1: "x = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then show "x = y"
      by (typecheck_cfuncs, smt (z3) mx_eqs_my element_pair_eq f1 f2 f3 false_func_type maps_into_1u1 terminal_func_unique true_false_distinct true_func_type x_form y_form)
  next
    assume not_case1: "x ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "x = (right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭)∨ 
               x = right_coproj 𝟭 (𝟭∐𝟭) ∘c(right_coproj 𝟭 𝟭)"
      by (metis id_right_unit2 id_type left_proj_type maps_into_1u1 terminal_func_unique x_form)
    show "x = y"
    proof(cases "x = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭")
      assume case2: "x = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then show "x = y"
        by (typecheck_cfuncs, smt (z3) a1 NOT_false_is_true NOT_is_pullback  cart_prod_eq2 cfunc_prod_comp cfunc_type_def characteristic_func_eq characteristic_func_is_pullback characteristic_function_exists comp_associative element_monomorphism f1 f2 f3 false_func_type left_proj_type maps_into_1u1 mx_eqs_my terminal_func_unique true_false_distinct true_func_type y_form)
    next
      assume not_case2: "x ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "x = right_coproj 𝟭 (𝟭∐𝟭) ∘c(right_coproj 𝟭 𝟭)"
        using case2_or_3 by blast
      then show "x = y"
        by (smt (z3) NOT_false_is_true NOT_is_pullback a1 cart_prod_eq2 cfunc_type_def characteristic_func_eq characteristic_func_is_pullback characteristic_function_exists comp_associative diag_on_elements diagonal_type element_monomorphism f1 f2 f3 false_func_type left_proj_type maps_into_1u1 mx_eqs_my terminal_func_unique true_false_distinct true_func_type x_type y_form)
    qed
  qed
qed

lemma IMPLIES_is_pullback:
  "is_pullback (𝟭∐(𝟭∐𝟭)) 𝟭 (Ω×cΩ) Ω (β⇘(𝟭∐(𝟭∐𝟭))⇙) 𝗍 (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) IMPLIES"
  unfolding IMPLIES_def
  using element_monomorphism characteristic_function_exists
  by (typecheck_cfuncs, simp add: the1I2 injective_imp_monomorphism pre_IMPLIES_injective)
      
lemma IMPLIES_type[type_rule]:
  "IMPLIES : Ω ×c Ω → Ω"
  unfolding IMPLIES_def
  by (metis IMPLIES_def IMPLIES_is_pullback is_pullback_def)

lemma IMPLIES_true_true_is_true:
  "IMPLIES ∘c ⟨𝗍,𝗍⟩ = 𝗍"
proof -   
  have "∃ j. j ∈c 𝟭 ∐ (𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝗍,𝗍⟩"
    by (typecheck_cfuncs, meson left_coproj_cfunc_coprod left_proj_type)
  then show ?thesis
    by (smt (verit, ccfv_threshold) IMPLIES_is_pullback NOT_false_is_true NOT_is_pullback comp_associative2 is_pullback_def  terminal_func_comp)
qed 

lemma IMPLIES_false_true_is_true:
  "IMPLIES ∘c ⟨𝖿,𝗍⟩ = 𝗍"
proof -   
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝖿,𝗍⟩"
    by (typecheck_cfuncs, smt (z3) comp_associative2 comp_type right_coproj_cfunc_coprod right_proj_type)
  then show ?thesis
    by (smt (verit, ccfv_threshold) IMPLIES_is_pullback NOT_false_is_true NOT_is_pullback comp_associative2 is_pullback_def  terminal_func_comp)
qed 

lemma IMPLIES_false_false_is_true:
  "IMPLIES ∘c  ⟨𝖿,𝖿⟩ = 𝗍"
proof -   
  have "∃ j. j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝖿,𝖿⟩"
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) cfunc_type_def comp_associative comp_type left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type)
  then show ?thesis
    by (smt (verit, ccfv_threshold) IMPLIES_is_pullback NOT_false_is_true NOT_is_pullback comp_associative2 is_pullback_def  terminal_func_comp)
qed 

lemma IMPLIES_true_false_is_false:
  "IMPLIES ∘c  ⟨𝗍,𝖿⟩ = 𝖿"
proof(rule ccontr)  
  assume "IMPLIES ∘c ⟨𝗍,𝖿⟩ ≠ 𝖿"
  then have "IMPLIES ∘c ⟨𝗍,𝖿⟩ = 𝗍"
    using true_false_only_truth_values by (typecheck_cfuncs, blast)
  then obtain j where j_def: "j ∈c 𝟭∐(𝟭∐𝟭) ∧ (⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j  = ⟨𝗍,𝖿⟩"
    by (typecheck_cfuncs, smt (verit, ccfv_threshold) IMPLIES_is_pullback  id_right_unit2 is_pullback_def one_unique_element terminal_func_comp terminal_func_comp_elem terminal_func_unique)
  show False
  proof(cases "j = left_coproj 𝟭 (𝟭∐𝟭)")
    assume case1: "j = left_coproj 𝟭 (𝟭∐𝟭)"
    show False
    proof - 
      have "(⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ⟨𝗍, 𝗍⟩"
        by (typecheck_cfuncs, simp add: case1 left_coproj_cfunc_coprod)
      then have "⟨𝗍, 𝗍⟩ = ⟨𝗍,𝖿⟩"
        using j_def by presburger
      then have "𝗍 = 𝖿"
        using IFF_true_false_is_false IFF_true_true_is_true by auto
      then show False
        using true_false_distinct by blast
    qed
  next
    assume "j ≠ left_coproj 𝟭 (𝟭 ∐ 𝟭)"
    then have case2_or_3: "j = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭 ∨ 
                      j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
      by (metis coprojs_jointly_surj id_right_unit2 id_type j_def left_proj_type maps_into_1u1 one_unique_element)
    show False
    proof(cases "j = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭")
      assume case2: "j = right_coproj 𝟭 (𝟭∐𝟭)∘c left_coproj 𝟭 𝟭"
      show False
      proof - 
        have "(⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ⟨𝖿, 𝖿⟩"
          by (typecheck_cfuncs, smt (z3) case2 comp_associative2 left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type)
        then have "⟨𝗍, 𝗍⟩ = ⟨𝖿,𝖿⟩"
          using XOR_false_false_is_false XOR_only_true_left_is_true j_def by auto
        then have "𝗍 = 𝖿"
          by (metis XOR_only_true_left_is_true XOR_true_true_is_false ‹⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩ ∘c j = ⟨𝖿,𝖿⟩› j_def)
        then show False
          using true_false_distinct by blast
      qed
    next
      assume "j ≠ right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have case3: "j = right_coproj 𝟭 (𝟭∐𝟭) ∘c right_coproj 𝟭 𝟭"
        using case2_or_3 by blast
      show False
      proof - 
        have "(⟨𝗍, 𝗍⟩⨿ (⟨𝖿, 𝖿⟩ ⨿⟨𝖿, 𝗍⟩)) ∘c j = ⟨𝖿, 𝗍⟩"
          by (typecheck_cfuncs, smt (z3) case3 comp_associative2 left_coproj_cfunc_coprod left_proj_type right_coproj_cfunc_coprod right_proj_type)
        then have "⟨𝗍, 𝗍⟩ = ⟨𝖿, 𝗍⟩"
          by (metis cart_prod_eq2 false_func_type j_def true_func_type)
        then have "𝗍 = 𝖿"
          using XOR_only_true_right_is_true XOR_true_true_is_false by auto
        then show False
          using true_false_distinct by blast
      qed
    qed
  qed
qed

lemma IMPLIES_false_is_true_false:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"  
  assumes "IMPLIES ∘c  ⟨p,q⟩ = 𝖿"
  shows "p = 𝗍 ∧ q = 𝖿"
  by (metis IMPLIES_false_false_is_true IMPLIES_false_true_is_true IMPLIES_true_true_is_true assms true_false_only_truth_values)

text ‹ETCS analog to $(A \iff B) = (A \implies B) \land (B \implies A)$›
lemma iff_is_and_implies_implies_swap:
"IFF = AND ∘c  ⟨IMPLIES, IMPLIES ∘c  swap Ω Ω⟩"
proof(etcs_rule one_separator)
  fix x 
  assume x_type: "x ∈c Ω ×c Ω"
  then obtain p q where x_def: "p ∈c Ω ∧ q ∈c Ω ∧ x = ⟨p,q⟩"
    by (meson cart_prod_decomp)
  show "IFF ∘c x = (AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩) ∘c x"
  proof(cases "p = 𝗍")
    assume "p = 𝗍"
    show ?thesis
    proof(cases "q = 𝗍")
      assume "q = 𝗍"
      show ?thesis
      proof - 
        have "(AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩) ∘c x =    
               AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩  ∘c x"
          using comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c x,IMPLIES ∘c swap Ω Ω ∘c x⟩"
          using cfunc_prod_comp comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c ⟨𝗍,𝗍⟩, IMPLIES ∘c ⟨𝗍,𝗍⟩⟩"
          using ‹p = 𝗍› ‹q = 𝗍› swap_ap x_def by (typecheck_cfuncs, presburger)
        also have "... = AND ∘c ⟨𝗍, 𝗍⟩"
          using IMPLIES_true_true_is_true by presburger
        also have "... = 𝗍"
          by (simp add: AND_true_true_is_true)
        also have "... = IFF ∘c x"
          by (simp add: IFF_true_true_is_true ‹p = 𝗍› ‹q = 𝗍› x_def)
        finally show ?thesis
          by simp
      qed
    next
      assume "q ≠ 𝗍"
      then have "q = 𝖿"
        by (meson true_false_only_truth_values x_def)
      show ?thesis
      proof - 
        have "(AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩) ∘c x =    
               AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩  ∘c x"
          using comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c x,IMPLIES ∘c swap Ω Ω ∘c x⟩"
          using cfunc_prod_comp comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c ⟨𝗍,𝖿⟩, IMPLIES ∘c ⟨𝖿,𝗍⟩⟩"
          using ‹p = 𝗍› ‹q = 𝖿› swap_ap x_def by (typecheck_cfuncs, presburger)
        also have "... = AND ∘c ⟨𝖿, 𝗍⟩"
          using IMPLIES_false_true_is_true IMPLIES_true_false_is_false by presburger
        also have "... = 𝖿"
          by (simp add: AND_false_left_is_false true_func_type)
        also have "... = IFF ∘c x"
          by (simp add: IFF_true_false_is_false ‹p = 𝗍› ‹q = 𝖿› x_def)
        finally show ?thesis
          by simp
      qed
    qed
  next
    assume "p ≠ 𝗍"
    then have "p = 𝖿"
      using true_false_only_truth_values x_def by blast
    show ?thesis
    proof(cases "q = 𝗍")
      assume "q = 𝗍"
      show ?thesis
      proof - 
        have "(AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩) ∘c x =    
               AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩  ∘c x"
          using comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c x,IMPLIES ∘c swap Ω Ω ∘c x⟩"
          using cfunc_prod_comp comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c ⟨𝖿,𝗍⟩, IMPLIES ∘c ⟨𝗍,𝖿⟩⟩"
          using ‹p = 𝖿› ‹q = 𝗍› swap_ap x_def by (typecheck_cfuncs, presburger)
        also have "... = AND ∘c ⟨𝗍, 𝖿⟩"
          by (simp add: IMPLIES_false_true_is_true IMPLIES_true_false_is_false)
        also have "... = 𝖿"
          by (simp add: AND_false_right_is_false true_func_type)
        also have "... = IFF ∘c x"
          by (simp add: IFF_false_true_is_false ‹p = 𝖿› ‹q = 𝗍› x_def)
        finally show ?thesis
          by simp
      qed
    next
      assume "q ≠ 𝗍"
      then have "q = 𝖿"
        by (meson true_false_only_truth_values x_def)
      show ?thesis
      proof - 
        have "(AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩) ∘c x =    
               AND ∘c ⟨IMPLIES,IMPLIES ∘c swap Ω Ω⟩  ∘c x"
          using comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c x,IMPLIES ∘c swap Ω Ω ∘c x⟩"
          using cfunc_prod_comp comp_associative2 x_type by (typecheck_cfuncs, force)
        also have "... = AND ∘c ⟨IMPLIES ∘c ⟨𝖿,𝖿⟩, IMPLIES ∘c ⟨𝖿,𝖿⟩⟩"
          using ‹p = 𝖿› ‹q = 𝖿› swap_ap x_def by (typecheck_cfuncs, presburger)
        also have "... = AND ∘c ⟨𝗍, 𝗍⟩"
          by (simp add: IMPLIES_false_false_is_true)
        also have "... = 𝗍"
          by (simp add: AND_true_true_is_true)
        also have "... = IFF ∘c x"
          by (simp add: IFF_false_false_is_true ‹p = 𝖿› ‹q = 𝖿› x_def)
        finally show ?thesis
          by simp
      qed
    qed
  qed
qed

lemma IMPLIES_is_OR_NOT_id:
  "IMPLIES = OR ∘c (NOT ×f id(Ω))"
proof(etcs_rule one_separator)
  fix x 
  assume x_type: "x ∈c Ω ×c Ω"
  then obtain u v where x_form: "u ∈c Ω ∧ v ∈c Ω ∧ x = ⟨u, v⟩"
    using cart_prod_decomp by blast
  show "IMPLIES ∘c x = (OR ∘c NOT ×f idc Ω) ∘c x"
  proof(cases "u = 𝗍")
    assume "u = 𝗍"
    show ?thesis
    proof(cases "v = 𝗍")
      assume "v = 𝗍"
      have "(OR ∘c NOT ×f idc Ω) ∘c x = OR ∘c (NOT ×f idc Ω) ∘c x"
        using comp_associative2 x_type by (typecheck_cfuncs, force)
      also have "... = OR ∘c ⟨NOT ∘c 𝗍, idc Ω ∘c 𝗍⟩"
        by (typecheck_cfuncs, simp add: ‹u = 𝗍› ‹v = 𝗍› cfunc_cross_prod_comp_cfunc_prod x_form)
      also have "... = OR ∘c ⟨𝖿, 𝗍⟩"
        by (typecheck_cfuncs, simp add: NOT_true_is_false id_left_unit2)
      also have "... = 𝗍"
        by (simp add: OR_true_right_is_true false_func_type)
      also have "... = IMPLIES ∘c x"
        by (simp add: IMPLIES_true_true_is_true ‹u = 𝗍› ‹v = 𝗍› x_form)
      finally show ?thesis
        by simp
    next
      assume "v ≠ 𝗍"
      then have "v = 𝖿"
        by (metis true_false_only_truth_values x_form)
      have "(OR ∘c NOT ×f idc Ω) ∘c x = OR ∘c (NOT ×f idc Ω) ∘c x"
        using comp_associative2 x_type by (typecheck_cfuncs, force)
      also have "... = OR ∘c ⟨NOT ∘c 𝗍, idc Ω ∘c 𝖿⟩"
        by (typecheck_cfuncs, simp add: ‹u = 𝗍› ‹v = 𝖿› cfunc_cross_prod_comp_cfunc_prod x_form)
      also have "... = OR ∘c ⟨𝖿, 𝖿⟩"
        by (typecheck_cfuncs, simp add: NOT_true_is_false id_left_unit2)
      also have "... = 𝖿"
        by (simp add: OR_false_false_is_false false_func_type)
      also have "... = IMPLIES ∘c x"
        by (simp add: IMPLIES_true_false_is_false ‹u = 𝗍› ‹v = 𝖿› x_form)
      finally show ?thesis
        by simp
      qed
  next
    assume "u ≠ 𝗍"
    then have "u = 𝖿"
        by (metis true_false_only_truth_values x_form)
    show ?thesis 
    proof(cases "v = 𝗍")
      assume "v = 𝗍"
      have "(OR ∘c NOT ×f idc Ω) ∘c x = OR ∘c (NOT ×f idc Ω) ∘c x"
        using comp_associative2 x_type by (typecheck_cfuncs, force)
      also have "... = OR ∘c ⟨NOT ∘c 𝖿, idc Ω ∘c 𝗍⟩"
        by (typecheck_cfuncs, simp add: ‹u = 𝖿› ‹v = 𝗍› cfunc_cross_prod_comp_cfunc_prod x_form)
      also have "... = OR ∘c ⟨𝗍, 𝗍⟩"
        using NOT_false_is_true id_left_unit2 true_func_type by smt
      also have "... = 𝗍"
        by (simp add: OR_true_right_is_true true_func_type)
      also have "... = IMPLIES ∘c x"
        by (simp add: IMPLIES_false_true_is_true ‹u = 𝖿› ‹v = 𝗍› x_form)
      finally show ?thesis
        by simp
    next
      assume "v ≠ 𝗍"
      then have "v = 𝖿"
        by (metis true_false_only_truth_values x_form)
      have "(OR ∘c NOT ×f idc Ω) ∘c x = OR ∘c (NOT ×f idc Ω) ∘c x"
        using comp_associative2 x_type by (typecheck_cfuncs, force)
      also have "... = OR ∘c ⟨NOT ∘c 𝖿, idc Ω ∘c 𝖿⟩"
        by (typecheck_cfuncs, simp add: ‹u = 𝖿› ‹v = 𝖿› cfunc_cross_prod_comp_cfunc_prod x_form)
      also have "... = OR ∘c ⟨𝗍, 𝖿⟩"
        using NOT_false_is_true false_func_type id_left_unit2 by presburger
      also have "... = 𝗍"
        by (simp add: OR_true_left_is_true false_func_type)
      also have "... = IMPLIES ∘c x"
        by (simp add: IMPLIES_false_false_is_true ‹u = 𝖿› ‹v = 𝖿› x_form)
      finally show ?thesis
        by simp
      qed
  qed
qed

lemma IMPLIES_implies_implies:
  assumes P_type[type_rule]: "P : X → Ω" and Q_type[type_rule]: "Q : Y → Ω"
  assumes X_nonempty: "∃x. x ∈c X"
  assumes IMPLIES_true: "IMPLIES ∘c (P ×f Q) = 𝗍 ∘c β⇘X ×c Y⇙"
  shows "P = 𝗍 ∘c β⇘X⇙ ⟹ Q = 𝗍 ∘c β⇘Y⇙"
proof -
  obtain z where z_type[type_rule]: "z : X ×c Y → 𝟭 ∐ 𝟭 ∐ 𝟭"
    and z_eq: "P ×f Q = (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c z"
    using IMPLIES_is_pullback unfolding is_pullback_def
    by (auto, typecheck_cfuncs, metis IMPLIES_true terminal_func_type)  
  assume P_true: "P = 𝗍 ∘c β⇘X⇙"
  
  have "left_cart_proj Ω Ω ∘c (P ×f Q) = left_cart_proj Ω Ω ∘c (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c z"
    using z_eq by simp
  then have "P ∘c left_cart_proj X Y = (left_cart_proj Ω Ω ∘c (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩)) ∘c z"
    using Q_type comp_associative2 left_cart_proj_cfunc_cross_prod by (typecheck_cfuncs, force)
  then have "P ∘c left_cart_proj X Y
    = ((left_cart_proj Ω Ω ∘c ⟨𝗍,𝗍⟩) ⨿ (left_cart_proj Ω Ω ∘c ⟨𝖿,𝖿⟩) ⨿ (left_cart_proj Ω Ω ∘c ⟨𝖿,𝗍⟩)) ∘c z"
    by (typecheck_cfuncs_prems, simp add: cfunc_coprod_comp)
  then have "P ∘c left_cart_proj X Y = (𝗍 ⨿ 𝖿 ⨿ 𝖿) ∘c z"
    by (typecheck_cfuncs_prems, smt left_cart_proj_cfunc_prod)

  show "Q = 𝗍 ∘c β⇘Y⇙"
  proof (etcs_rule one_separator)
    fix y
    assume y_in_Y[type_rule]: "y ∈c Y"
    obtain x where x_in_X[type_rule]: "x ∈c X"
      using X_nonempty by blast

    have "z ∘c ⟨x,y⟩ = left_coproj 𝟭 (𝟭 ∐ 𝟭)
        ∨ z ∘c ⟨x,y⟩ = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭
        ∨ z ∘c ⟨x,y⟩ = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c right_coproj 𝟭 𝟭"
      by (typecheck_cfuncs, smt comp_associative2 coprojs_jointly_surj one_unique_element)
    then show "Q ∘c y = (𝗍 ∘c β⇘Y⇙) ∘c y"
    proof safe
      assume "z ∘c ⟨x,y⟩ = left_coproj 𝟭 (𝟭 ∐ 𝟭)"
      then have "(P ×f Q) ∘c ⟨x,y⟩ = (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c left_coproj 𝟭 (𝟭 ∐ 𝟭)"
        by (typecheck_cfuncs, smt comp_associative2 z_eq z_type)
      then have "(P ×f Q) ∘c ⟨x,y⟩ = ⟨𝗍,𝗍⟩"
        by (typecheck_cfuncs_prems, smt left_coproj_cfunc_coprod)
      then have "Q ∘c y = 𝗍"
        by (typecheck_cfuncs_prems, smt (verit, best) cfunc_cross_prod_comp_cfunc_prod comp_associative2 comp_type id_right_unit2 right_cart_proj_cfunc_prod)
      then show "Q ∘c y = (𝗍 ∘c β⇘Y⇙) ∘c y"
        by (smt (verit, best) comp_associative2 id_right_unit2 terminal_func_comp_elem terminal_func_type true_func_type y_in_Y)
    next
      assume "z ∘c ⟨x,y⟩ = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
      then have "(P ×f Q) ∘c ⟨x,y⟩ = (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c left_coproj 𝟭 𝟭"
        by (typecheck_cfuncs, smt comp_associative2 z_eq z_type)
      then have "(P ×f Q) ∘c ⟨x,y⟩ = (⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c left_coproj 𝟭 𝟭"
        by (typecheck_cfuncs_prems, smt right_coproj_cfunc_coprod comp_associative2)
      then have "(P ×f Q) ∘c ⟨x,y⟩ = ⟨𝖿,𝖿⟩"
        by (typecheck_cfuncs_prems, smt left_coproj_cfunc_coprod)
      then have "P ∘c x = 𝖿"
        by (typecheck_cfuncs_prems, smt (verit, best) cfunc_cross_prod_comp_cfunc_prod comp_associative2 comp_type id_right_unit2 left_cart_proj_cfunc_prod)
      also have "P ∘c x = 𝗍"
        using P_true by (typecheck_cfuncs_prems, smt (z3) comp_associative2 id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type x_in_X)
      ultimately have False
        using true_false_distinct by simp
      then show "Q ∘c y = (𝗍 ∘c β⇘Y⇙) ∘c y"
        by simp
    next
      assume "z ∘c ⟨x,y⟩ = right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c right_coproj 𝟭 𝟭"
      then have "(P ×f Q) ∘c ⟨x,y⟩ = (⟨𝗍,𝗍⟩ ⨿ ⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c right_coproj 𝟭 (𝟭 ∐ 𝟭) ∘c right_coproj 𝟭 𝟭"
        by (typecheck_cfuncs, smt comp_associative2 z_eq z_type)
      then have "(P ×f Q) ∘c ⟨x,y⟩ = (⟨𝖿,𝖿⟩ ⨿ ⟨𝖿,𝗍⟩) ∘c right_coproj 𝟭 𝟭"
        by (typecheck_cfuncs_prems, smt right_coproj_cfunc_coprod comp_associative2)
      then have "(P ×f Q) ∘c ⟨x,y⟩ = ⟨𝖿,𝗍⟩"
        by (typecheck_cfuncs_prems, smt right_coproj_cfunc_coprod)
      then have "Q ∘c y = 𝗍"
        by (typecheck_cfuncs_prems, smt (verit, best) cfunc_cross_prod_comp_cfunc_prod comp_associative2 comp_type id_right_unit2 right_cart_proj_cfunc_prod)
      then show "Q ∘c y = (𝗍 ∘c β⇘Y⇙) ∘c y"
        by (typecheck_cfuncs, smt (z3) comp_associative2 id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
    qed
  qed
qed

lemma IMPLIES_elim:
  assumes IMPLIES_true: "IMPLIES ∘c (P ×f Q) = 𝗍 ∘c β⇘X ×c Y⇙"
  assumes P_type[type_rule]: "P : X → Ω" and Q_type[type_rule]: "Q : Y → Ω"
  assumes X_nonempty: "∃x. x ∈c X"
  shows "(P = 𝗍 ∘c β⇘X⇙) ⟹ ((Q = 𝗍 ∘c β⇘Y⇙) ⟹ R) ⟹ R"
  using IMPLIES_implies_implies assms by blast

lemma IMPLIES_elim'':
  assumes IMPLIES_true: "IMPLIES ∘c (P ×f Q) = 𝗍"
  assumes P_type[type_rule]: "P : 𝟭 → Ω" and Q_type[type_rule]: "Q : 𝟭 → Ω"
  shows "(P = 𝗍) ⟹ ((Q = 𝗍) ⟹ R) ⟹ R"
proof -
  have one_nonempty: "∃x. x ∈c 𝟭"
    using one_unique_element by blast
  have "(IMPLIES ∘c (P ×f Q) = 𝗍 ∘c β⇘𝟭 ×c 𝟭⇙)"
    by (typecheck_cfuncs, metis IMPLIES_true id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
  then have "(P = 𝗍 ∘c β⇘𝟭⇙) ⟹ ((Q = 𝗍 ∘c β⇘𝟭⇙) ⟹ R) ⟹ R"
    using one_nonempty by (-, etcs_erule IMPLIES_elim, auto)
  then show "(P = 𝗍) ⟹ ((Q = 𝗍) ⟹ R) ⟹ R"
    by (typecheck_cfuncs, metis id_right_unit2 id_type one_unique_element terminal_func_type)
qed

lemma IMPLIES_elim':
  assumes IMPLIES_true: "IMPLIES ∘c ⟨P, Q⟩ = 𝗍"
  assumes P_type[type_rule]: "P : 𝟭 → Ω" and Q_type[type_rule]: "Q : 𝟭 → Ω"
  shows "(P = 𝗍) ⟹ ((Q = 𝗍) ⟹ R) ⟹ R"
  using IMPLIES_true IMPLIES_true_false_is_false Q_type true_false_only_truth_values by force

lemma implies_implies_IMPLIES:
  assumes P_type[type_rule]: "P : 𝟭 → Ω" and Q_type[type_rule]: "Q : 𝟭 → Ω"
  shows  "(P = 𝗍 ⟹ Q = 𝗍) ⟹ IMPLIES ∘c ⟨P, Q⟩ = 𝗍"
  by (typecheck_cfuncs, metis IMPLIES_false_is_true_false true_false_only_truth_values)

subsection ‹Other Boolean Identities›

lemma AND_OR_distributive:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  assumes "r ∈c Ω"
  shows "AND ∘c ⟨p, OR ∘c ⟨q,r⟩⟩ = OR ∘c ⟨AND ∘c ⟨p,q⟩, AND ∘c ⟨p,r⟩⟩"
  by (metis AND_commutative AND_false_right_is_false AND_true_true_is_true OR_false_false_is_false OR_true_left_is_true OR_true_right_is_true assms true_false_only_truth_values)

lemma OR_AND_distributive:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  assumes "r ∈c Ω"
  shows "OR ∘c ⟨p, AND ∘c ⟨q,r⟩⟩ = AND ∘c ⟨OR ∘c ⟨p,q⟩, OR ∘c ⟨p,r⟩⟩"
  by (smt (z3) AND_commutative AND_false_right_is_false AND_true_true_is_true OR_commutative OR_false_false_is_false OR_true_right_is_true assms true_false_only_truth_values)

lemma OR_AND_absorption:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "OR ∘c ⟨p, AND ∘c ⟨p,q⟩⟩ = p"
  by (metis AND_commutative AND_complementary AND_idempotent NOT_true_is_false OR_false_false_is_false OR_true_left_is_true assms true_false_only_truth_values)

lemma AND_OR_absorption:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "AND ∘c ⟨p, OR ∘c ⟨p,q⟩⟩ = p"
  by (metis AND_commutative AND_complementary AND_idempotent NOT_true_is_false OR_AND_absorption OR_commutative assms true_false_only_truth_values)

lemma deMorgan_Law1:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "NOT ∘c OR ∘c ⟨p,q⟩ = AND ∘c ⟨NOT ∘c p, NOT ∘c q⟩"
  by (metis AND_OR_absorption AND_complementary AND_true_true_is_true NOT_false_is_true NOT_true_is_false OR_AND_absorption OR_commutative OR_idempotent assms false_func_type true_false_only_truth_values)

lemma deMorgan_Law2:
  assumes "p ∈c Ω"
  assumes "q ∈c Ω"
  shows "NOT ∘c AND ∘c ⟨p,q⟩ = OR ∘c ⟨NOT ∘c p, NOT ∘c q⟩"
  by (metis AND_complementary AND_idempotent NOT_false_is_true NOT_true_is_false OR_complementary OR_false_false_is_false OR_idempotent assms true_false_only_truth_values true_func_type)
 
end