Theory Nats

section ‹Natural Number Object›

theory Nats
  imports Exponential_Objects
begin

text ‹The axiomatization below corresponds to Axiom 10 (Natural Number Object) in Halvorson.›
axiomatization
  natural_numbers :: "cset" ("ℕ⇩c") and
  zero :: "cfunc" and
  successor :: "cfunc"
  where
  zero_type[type_rule]: "zero ∈⇩c ℕ⇩c" and 
  successor_type[type_rule]: "successor: ℕ⇩c → ℕ⇩c" and 
  natural_number_object_property: 
  "q : 𝟭 → X ⟹ f: X → X ⟹
   (∃!u. u: ℕ⇩c → X ∧
   q = u ∘⇩c zero ∧
   f ∘⇩c u = u ∘⇩c successor)"

lemma beta_N_succ_nEqs_Id1:
  assumes n_type[type_rule]: "n ∈⇩c ℕ⇩c"
  shows "β⇘ℕ⇩c⇙ ∘⇩c successor ∘⇩c n = id 𝟭"
  by (typecheck_cfuncs, simp add: terminal_func_comp_elem)

lemma natural_number_object_property2:
  assumes "q : 𝟭 → X" "f: X → X"
  shows "∃!u. u: ℕ⇩c → X ∧ u ∘⇩c zero = q ∧ f ∘⇩c u = u ∘⇩c successor"
  using assms natural_number_object_property[where q=q, where f=f, where X=X]
  by metis

lemma natural_number_object_func_unique:
  assumes u_type: "u : ℕ⇩c → X" and v_type: "v : ℕ⇩c → X" and f_type: "f: X → X"
  assumes zeros_eq: "u ∘⇩c zero = v ∘⇩c zero"
  assumes u_successor_eq: "u ∘⇩c successor = f ∘⇩c u"
  assumes v_successor_eq: "v ∘⇩c successor = f ∘⇩c v"
  shows "u = v"
  by (smt (verit, best) comp_type f_type natural_number_object_property2 u_successor_eq u_type v_successor_eq v_type zero_type zeros_eq)

definition is_NNO :: "cset ⇒ cfunc ⇒ cfunc ⇒ bool"  where
   "is_NNO Y z s ⟷(z: 𝟭 → Y ∧ s: Y → Y  ∧ (∀ X f q. ((q : 𝟭 → X) ∧ (f: X → X))⟶
   (∃!u. u: Y → X ∧
   q = u ∘⇩c z ∧
   f ∘⇩c u = u ∘⇩c s)))"

lemma N_is_a_NNO:
    "is_NNO ℕ⇩c zero successor"
by (simp add: is_NNO_def natural_number_object_property successor_type zero_type)

text ‹The lemma below corresponds to Exercise 2.6.5 in Halvorson.›
lemma NNOs_are_iso_N:
  assumes "is_NNO N z s"
  shows "N ≅ ℕ⇩c"
proof-
  have z_type[type_rule]: "(z : 𝟭 →  N)" 
    using assms is_NNO_def by blast
  have s_type[type_rule]: "(s : N →  N)"
    using assms is_NNO_def by blast 
  then obtain u where u_type[type_rule]: "u: ℕ⇩c → N" 
                 and  u_triangle: "u ∘⇩c zero = z" 
                 and  u_square: "s ∘⇩c u = u ∘⇩c successor"
    using natural_number_object_property z_type by blast
  obtain v where v_type[type_rule]: "v: N → ℕ⇩c" 
                 and  v_triangle: "v ∘⇩c z = zero" 
                 and  v_square: "successor ∘⇩c v = v ∘⇩c s"
    by (metis assms is_NNO_def successor_type zero_type)
  then have vuzeroEqzero: "v ∘⇩c (u ∘⇩c zero) = zero"
    by (simp add: u_triangle v_triangle)
  have id_facts1: "id(ℕ⇩c): ℕ⇩c → ℕ⇩c∧ id(ℕ⇩c) ∘⇩c zero = zero ∧
          (successor ∘⇩c id(ℕ⇩c) = id(ℕ⇩c) ∘⇩c successor)"
    by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
  then have vu_facts: "v ∘⇩c u: ℕ⇩c → ℕ⇩c∧ (v ∘⇩c u) ∘⇩c zero = zero ∧ 
          successor ∘⇩c (v ∘⇩c u) = (v ∘⇩c u) ∘⇩c successor"
    by (typecheck_cfuncs, smt (verit, best) comp_associative2 s_type u_square v_square vuzeroEqzero)
  then have half_isomorphism: "(v ∘⇩c u) = id(ℕ⇩c)"
    by (metis id_facts1 natural_number_object_property successor_type vu_facts zero_type)
  have uvzEqz: "u ∘⇩c (v ∘⇩c z) = z"
    by (simp add: u_triangle v_triangle)
  have id_facts2: "id(N): N → N ∧ id(N) ∘⇩c z = z ∧ s ∘⇩c id(N) = id(N) ∘⇩c  s"
    by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
  then have uv_facts: "u ∘⇩c v: N → N ∧
          (u ∘⇩c v) ∘⇩c  z = z ∧  s ∘⇩c (u ∘⇩c v) =  (u ∘⇩c v) ∘⇩c s"
    by (typecheck_cfuncs, smt (verit, best) comp_associative2 successor_type u_square uvzEqz v_square)
 then have half_isomorphism2: "(u ∘⇩c v) = id(N)"
   by (smt (verit, ccfv_threshold) assms id_facts2 is_NNO_def)
  then show "N ≅ ℕ⇩c"
    using cfunc_type_def half_isomorphism is_isomorphic_def isomorphism_def u_type v_type by fastforce
qed

text ‹The lemma below is the converse to Exercise 2.6.5 in Halvorson.›
lemma Iso_to_N_is_NNO:
  assumes "N ≅ ℕ⇩c"
  shows "∃ z s. is_NNO N z s"
proof - 
  obtain i where i_type[type_rule]: "i: ℕ⇩c → N" and i_iso: "isomorphism(i)"
    using assms isomorphic_is_symmetric is_isomorphic_def by blast 
  obtain z where z_type[type_rule]: "z ∈⇩c N" and z_def: "z = i ∘⇩c zero"
    by (typecheck_cfuncs, simp)
  obtain s where s_type[type_rule]: "s: N → N" and s_def: "s = (i ∘⇩c successor) ∘⇩c i❙¯"
    using i_iso by (typecheck_cfuncs, simp)
  have "is_NNO N z s"
    unfolding is_NNO_def
  proof(typecheck_cfuncs)
    fix X q f 
    assume q_type[type_rule]: "q: 𝟭 → X"
    assume f_type[type_rule]: "f:   X → X"

    obtain u where u_type[type_rule]: "u: ℕ⇩c → X" and u_def:  "u ∘⇩c zero =  q ∧ f ∘⇩c u = u ∘⇩c successor"
      using natural_number_object_property2 by (typecheck_cfuncs, blast)
    obtain v where v_type[type_rule]: "v: N → X" and v_def: "v = u ∘⇩c i❙¯"
      using i_iso by (typecheck_cfuncs, simp)
    then have bottom_triangle: "v ∘⇩c z = q"
      unfolding v_def u_def z_def using i_iso
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative id_right_unit2 inv_left u_def)
    have bottom_square: "v ∘⇩c s = f ∘⇩c v"
      unfolding v_def u_def s_def using i_iso
      by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 id_right_unit2 inv_left u_def)
    show "∃!u. u : N → X ∧ q = u ∘⇩c z ∧ f ∘⇩c u = u ∘⇩c s"
    proof safe
      show "∃u. u : N → X ∧ q = u ∘⇩c z ∧ f ∘⇩c u = u ∘⇩c s"
        by (intro exI[where x=v], auto simp add: bottom_triangle bottom_square v_type)
    next
      fix w y
      assume w_type[type_rule]: "w : N → X"
      assume y_type[type_rule]: "y : N → X"
      assume f_w: "f ∘⇩c w = w ∘⇩c s"
      assume f_y: "f ∘⇩c y = y ∘⇩c s"
      assume w_y_z: "w ∘⇩c z = y ∘⇩c z"
      assume q_def: "q = w ∘⇩c z"
      


      have "w ∘⇩c i = u"
      proof (etcs_rule natural_number_object_func_unique[where f=f])
        show "(w ∘⇩c i) ∘⇩c zero = u ∘⇩c zero"
          using q_def u_def w_y_z z_def by (etcs_assocr, argo)
        show "(w ∘⇩c i) ∘⇩c successor = f ∘⇩c w ∘⇩c i"
          using i_iso by (typecheck_cfuncs, smt (verit, best) comp_associative2 comp_type f_w id_right_unit2 inv_left inverse_type s_def)
        show "u ∘⇩c successor = f ∘⇩c u"
          by (simp add: u_def)
      qed
      then have w_eq_v: "w = v"
        unfolding v_def using i_iso
        by (typecheck_cfuncs, smt (verit, best) comp_associative2 id_right_unit2 inv_right)

      have "y ∘⇩c i = u"
      proof (etcs_rule natural_number_object_func_unique[where f=f])
        show "(y ∘⇩c i) ∘⇩c zero = u ∘⇩c zero"
          using q_def u_def w_y_z z_def by (etcs_assocr, argo)
        show "(y ∘⇩c i) ∘⇩c successor = f ∘⇩c y ∘⇩c i"
          using i_iso by (typecheck_cfuncs, smt (verit, best) comp_associative2 comp_type f_y id_right_unit2 inv_left inverse_type s_def)
        show "u ∘⇩c successor = f ∘⇩c u"
          by (simp add: u_def)
      qed
      then have y_eq_v: "y = v"
        unfolding v_def using i_iso
        by (typecheck_cfuncs, smt (verit, best) comp_associative2 id_right_unit2 inv_right)
      show "w = y"
        using w_eq_v y_eq_v by auto
    qed
  qed
  then show ?thesis
    by auto
qed

subsection ‹Zero and Successor›

lemma zero_is_not_successor:
  assumes "n ∈⇩c ℕ⇩c"
  shows "zero ≠ successor ∘⇩c n"
proof (rule ccontr, clarify)
  assume for_contradiction: "zero = successor ∘⇩c n"
  have "∃!u. u: ℕ⇩c → Ω ∧ u ∘⇩c zero = 𝗍 ∧ (𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u = u ∘⇩c successor"
    by (typecheck_cfuncs, rule natural_number_object_property2)
  then obtain u where  u_type:  "u: ℕ⇩c → Ω" and 
                       u_triangle: "u ∘⇩c zero = 𝗍" and  
                       u_square: "(𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u = u ∘⇩c successor"
    by auto
  have "𝗍 = 𝖿" 
  proof -
    have "𝗍 = u  ∘⇩c zero"
      by (simp add: u_triangle)
    also have "... = u ∘⇩c successor ∘⇩c n"
      by (simp add: for_contradiction)
    also have "... = (𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u ∘⇩c n"
      using assms u_type by (typecheck_cfuncs, simp add:  comp_associative2 u_square)
    also have "... = 𝖿"
      using assms u_type by (etcs_assocr,typecheck_cfuncs, simp add: id_right_unit2 terminal_func_comp_elem)
    finally show ?thesis.
  qed
  then show False
    using true_false_distinct by blast
qed

text ‹The lemma below corresponds to Proposition 2.6.6 in Halvorson.›
lemma oneUN_iso_N_isomorphism:
 "isomorphism(zero ⨿ successor)" 
proof - 
  obtain i0 where i0_type[type_rule]:  "i0: 𝟭 → (𝟭 ∐ ℕ⇩c)" and i0_def: "i0 = left_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, simp)
  obtain i1 where i1_type[type_rule]:  "i1: ℕ⇩c → (𝟭 ∐ ℕ⇩c)" and i1_def: "i1 = right_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, simp)
  obtain g where g_type[type_rule]: "g: ℕ⇩c → (𝟭 ∐ ℕ⇩c)" and
   g_triangle: " g ∘⇩c zero = i0" and
   g_square: "g ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c g"
    by (typecheck_cfuncs, metis natural_number_object_property)
  then have second_diagram3: "g ∘⇩c (successor ∘⇩c zero)  = (i1 ∘⇩c zero)"
    by (typecheck_cfuncs, smt (verit, best) cfunc_coprod_type comp_associative2 comp_type i0_def left_coproj_cfunc_coprod)
  then have g_s_s_Eqs_i1zUi1s_g_s:
    "(g ∘⇩c successor) ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c (g ∘⇩c successor)"
    by (typecheck_cfuncs, smt (verit, del_insts) comp_associative2 g_square)
  then have g_s_s_zEqs_i1zUi1s_i1z: "((g ∘⇩c successor) ∘⇩c successor)∘⇩c zero =
    ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c (i1 ∘⇩c zero)"
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 g_square second_diagram3)
  then have i1_sEqs_i1zUi1s_i1: "i1 ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c i1"
    by (typecheck_cfuncs, simp add: i1_def right_coproj_cfunc_coprod)   
  then obtain u where u_type[type_rule]: "(u: ℕ⇩c → (𝟭 ∐ ℕ⇩c))" and
      u_triangle: "u ∘⇩c zero = i1 ∘⇩c zero" and
      u_square: "u ∘⇩c successor =  ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c u "
    using i1_sEqs_i1zUi1s_i1 by (typecheck_cfuncs, blast)    
  then have u_Eqs_i1: "u=i1"
    by (typecheck_cfuncs, meson cfunc_coprod_type comp_type i1_sEqs_i1zUi1s_i1 natural_number_object_func_unique successor_type zero_type)
  have g_s_type[type_rule]: "g ∘⇩c successor: ℕ⇩c → (𝟭 ∐ ℕ⇩c)"
    by typecheck_cfuncs
  have g_s_triangle: "(g∘⇩c successor) ∘⇩c zero = i1 ∘⇩c zero"
    using comp_associative2 second_diagram3 by (typecheck_cfuncs, force)
  then have u_Eqs_g_s: "u= g∘⇩c successor"
    by (typecheck_cfuncs, smt (verit, ccfv_SIG) cfunc_coprod_type comp_type g_s_s_Eqs_i1zUi1s_g_s g_s_triangle i1_sEqs_i1zUi1s_i1 natural_number_object_func_unique u_Eqs_i1 zero_type)
  then have g_sEqs_i1: "g∘⇩c successor = i1"
    using u_Eqs_i1 by blast
  have eq1: "(zero ⨿ successor) ∘⇩c g = id(ℕ⇩c)"
    by (typecheck_cfuncs, smt (verit, best) cfunc_coprod_comp comp_associative2 g_square g_triangle i0_def i1_def i1_type id_left_unit2 id_right_unit2 left_coproj_cfunc_coprod natural_number_object_func_unique right_coproj_cfunc_coprod)
  then have eq2: "g ∘⇩c (zero ⨿ successor) = id(𝟭 ∐ ℕ⇩c)"
    by (typecheck_cfuncs, metis cfunc_coprod_comp g_sEqs_i1 g_triangle i0_def i1_def id_coprod)
  show "isomorphism(zero ⨿ successor)"
    using cfunc_coprod_type eq1 eq2 g_type isomorphism_def3 successor_type zero_type by blast
qed

lemma zUs_epic:
 "epimorphism(zero ⨿ successor)"
  by (simp add: iso_imp_epi_and_monic oneUN_iso_N_isomorphism)

lemma zUs_surj:
 "surjective(zero ⨿ successor)"
  by (simp add: cfunc_type_def epi_is_surj zUs_epic)

lemma nonzero_is_succ_aux:
  assumes "x ∈⇩c (𝟭 ∐ ℕ⇩c)"
  shows "(x = (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭) ∨
         (∃n. (n ∈⇩c ℕ⇩c) ∧ (x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n))"
  by(clarify, metis assms coprojs_jointly_surj id_type one_unique_element)

lemma nonzero_is_succ:
  assumes "k ∈⇩c ℕ⇩c"
  assumes "k ≠ zero"
  shows "∃n.(n∈⇩c ℕ⇩c ∧ k = successor ∘⇩c n)"
proof - 
  have x_exists: "∃x. ((x ∈⇩c 𝟭 ∐ ℕ⇩c) ∧ (zero ⨿ successor ∘⇩c x = k))"
    using assms cfunc_type_def surjective_def zUs_surj by (typecheck_cfuncs, auto)
  obtain x where x_def: "((x ∈⇩c 𝟭 ∐ ℕ⇩c) ∧ (zero ⨿ successor ∘⇩c x = k))"
    using x_exists by blast
  have cases: "(x = (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭) ∨ 
                (∃n. (n ∈⇩c ℕ⇩c ∧ x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n))"
    by (simp add: nonzero_is_succ_aux x_def)
  have not_case_1: "x ≠ (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭"
  proof(rule ccontr,clarify)
    assume bwoc: "x = left_coproj 𝟭 ℕ⇩c ∘⇩c id⇩c 𝟭"
    have contradiction: "k = zero"
      by (metis bwoc id_right_unit2 left_coproj_cfunc_coprod left_proj_type successor_type x_def zero_type)
    show False
      using contradiction assms(2) by force
  qed
  then obtain n where n_def: "n ∈⇩c ℕ⇩c ∧ x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n"
    using cases by blast
  then have "k = zero ⨿ successor ∘⇩c x"
    using x_def by blast
  also have "... = zero ⨿ successor ∘⇩c  right_coproj 𝟭 ℕ⇩c ∘⇩c n"
    by (simp add: n_def)
  also have "... =  (zero ⨿ successor ∘⇩c  right_coproj 𝟭 ℕ⇩c) ∘⇩c n"
    using cfunc_coprod_type cfunc_type_def comp_associative n_def right_proj_type successor_type zero_type by auto
  also have "... = successor ∘⇩c n"
    using right_coproj_cfunc_coprod successor_type zero_type by auto
  finally show ?thesis
    using n_def by auto
qed

subsection ‹Predecessor›

definition predecessor' :: "cfunc" where
  "predecessor' = (THE f. f : ℕ⇩c → 𝟭 ∐ ℕ⇩c 
    ∧ f ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c) ∧  (zero ⨿ successor) ∘⇩c f = id ℕ⇩c)"

lemma predecessor'_def2:
  "predecessor' : ℕ⇩c → 𝟭 ∐ ℕ⇩c ∧ predecessor' ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c)
    ∧ (zero ⨿ successor) ∘⇩c predecessor' = id ℕ⇩c"
  unfolding predecessor'_def
proof (rule theI', safe)
  show "∃x. x : ℕ⇩c → 𝟭 ∐ ℕ⇩c ∧
        x ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c) ∧ zero ⨿ successor ∘⇩c x = id⇩c ℕ⇩c"
    using oneUN_iso_N_isomorphism by (typecheck_cfuncs, unfold isomorphism_def cfunc_type_def, auto)
next
  fix x y
  assume x_type[type_rule]: "x : ℕ⇩c → 𝟭 ∐ ℕ⇩c" and y_type[type_rule]: "y : ℕ⇩c → 𝟭 ∐ ℕ⇩c"
  assume x_left_inv: "zero ⨿ successor ∘⇩c x = id⇩c ℕ⇩c"
  assume "x ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c)" "y ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c)"
  then have "x ∘⇩c zero ⨿ successor = y ∘⇩c zero ⨿ successor"
    by auto
  then have "x ∘⇩c zero ⨿ successor ∘⇩c x = y ∘⇩c zero ⨿ successor ∘⇩c x"
    by (typecheck_cfuncs, auto simp add: comp_associative2)
  then show "x = y"
    using id_right_unit2 x_left_inv x_type y_type by auto
qed

lemma predecessor'_type[type_rule]:
  "predecessor' : ℕ⇩c → 𝟭 ∐ ℕ⇩c"
  by (simp add: predecessor'_def2)

lemma predecessor'_left_inv:
  "(zero ⨿ successor) ∘⇩c predecessor' = id ℕ⇩c"
  by (simp add: predecessor'_def2)

lemma predecessor'_right_inv:
  "predecessor' ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c)"
  by (simp add: predecessor'_def2)

lemma predecessor'_successor:
  "predecessor' ∘⇩c successor = right_coproj 𝟭 ℕ⇩c"
proof -
  have "predecessor' ∘⇩c successor = predecessor' ∘⇩c (zero ⨿ successor) ∘⇩c right_coproj 𝟭 ℕ⇩c"
    using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
  also have "... = (predecessor' ∘⇩c (zero ⨿ successor)) ∘⇩c right_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = right_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, simp add: id_left_unit2 predecessor'_def2)
  finally show ?thesis.
qed

lemma predecessor'_zero:
  "predecessor' ∘⇩c zero = left_coproj 𝟭 ℕ⇩c"
proof -
  have "predecessor' ∘⇩c zero = predecessor' ∘⇩c (zero ⨿ successor) ∘⇩c left_coproj 𝟭 ℕ⇩c"
    using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
  also have "... = (predecessor' ∘⇩c (zero ⨿ successor)) ∘⇩c left_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, auto simp add: comp_associative2)
  also have "... = left_coproj 𝟭 ℕ⇩c"
    by (typecheck_cfuncs, simp add: id_left_unit2 predecessor'_def2)
  finally show ?thesis.
qed

definition predecessor :: "cfunc"
  where "predecessor = (zero ⨿ id ℕ⇩c) ∘⇩c predecessor'"

lemma predecessor_type[type_rule]:
  "predecessor : ℕ⇩c → ℕ⇩c"
  unfolding predecessor_def by typecheck_cfuncs

lemma predecessor_zero:
  "predecessor ∘⇩c zero = zero"
  unfolding predecessor_def 
  using left_coproj_cfunc_coprod predecessor'_zero by (etcs_assocr, typecheck_cfuncs, presburger)

lemma predecessor_successor:
  "predecessor ∘⇩c successor = id ℕ⇩c"
  unfolding predecessor_def
  by (etcs_assocr, typecheck_cfuncs, metis (full_types) predecessor'_successor right_coproj_cfunc_coprod)

subsection ‹Peano's Axioms and Induction›

text ‹The lemma below corresponds to Proposition 2.6.7 in Halvorson.›
lemma Peano's_Axioms:
 "injective successor  ∧ ¬ surjective successor"
proof - 
  have i1_mono: "monomorphism(right_coproj 𝟭 ℕ⇩c)"
    by (simp add: right_coproj_are_monomorphisms)
  have zUs_iso: "isomorphism(zero ⨿ successor)"
    using oneUN_iso_N_isomorphism by blast
  have zUsi1EqsS: "(zero ⨿ successor) ∘⇩c (right_coproj 𝟭 ℕ⇩c) = successor"
    using right_coproj_cfunc_coprod successor_type zero_type by auto
  then have succ_mono: "monomorphism(successor)"
    by (metis cfunc_coprod_type cfunc_type_def composition_of_monic_pair_is_monic i1_mono iso_imp_epi_and_monic oneUN_iso_N_isomorphism right_proj_type successor_type zero_type)
  obtain u where u_type: "u:  ℕ⇩c  → Ω" and u_def: "u ∘⇩c zero = 𝗍  ∧ (𝖿∘⇩cβ⇘Ω⇙) ∘⇩c u = u ∘⇩c  successor"
    by (typecheck_cfuncs, metis natural_number_object_property)    
  have s_not_surj: "¬ surjective successor"
    proof (rule ccontr, clarify)
      assume BWOC : "surjective successor"
      obtain n where n_type: "n : 𝟭 → ℕ⇩c" and snEqz: "successor ∘⇩c n = zero"
        using BWOC cfunc_type_def successor_type surjective_def zero_type by auto
      then show False
        by (metis zero_is_not_successor)
    qed
  then show "injective successor ∧ ¬ surjective successor"
    using monomorphism_imp_injective succ_mono by blast
qed

lemma succ_inject:
  assumes "n ∈⇩c ℕ⇩c" "m ∈⇩c ℕ⇩c"
  shows "successor ∘⇩c n = successor ∘⇩c m ⟹ n = m"
  by (metis Peano's_Axioms assms cfunc_type_def injective_def successor_type) 

theorem nat_induction:
  assumes p_type[type_rule]: "p : ℕ⇩c → Ω" and n_type[type_rule]: "n ∈⇩c ℕ⇩c"
  assumes base_case: "p ∘⇩c zero = 𝗍"
  assumes induction_case: "⋀n. n ∈⇩c ℕ⇩c ⟹ p ∘⇩c n = 𝗍 ⟹ p ∘⇩c successor ∘⇩c n = 𝗍"
  shows "p ∘⇩c n = 𝗍"
proof -
  obtain p' P where
    p'_type[type_rule]: "p' : P → ℕ⇩c" and
    p'_equalizer: "p ∘⇩c p' = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c p'" and
    p'_uni_prop: "∀ h F. (h : F → ℕ⇩c ∧ p ∘⇩c h = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c h) ⟶ (∃! k. k : F → P ∧ p' ∘⇩c k = h)"
    using equalizer_exists2 by (typecheck_cfuncs, blast)

  from base_case have "p ∘⇩c zero = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
    by (etcs_assocr, etcs_subst terminal_func_comp_elem id_right_unit2, -)
  then obtain z' where
    z'_type[type_rule]: "z' ∈⇩c P" and
    z'_def: "zero = p' ∘⇩c z'"
    using p'_uni_prop by (typecheck_cfuncs, metis)

  have "p ∘⇩c successor ∘⇩c p' = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor ∘⇩c p'"
  proof (etcs_rule one_separator)
    fix m
    assume m_type[type_rule]: "m ∈⇩c P"

    have "p  ∘⇩c p' ∘⇩c m = 𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c p' ∘⇩c m"
      by (etcs_assocl, simp add: p'_equalizer)
    then have "p ∘⇩c p' ∘⇩c m = 𝗍"
      by (-, etcs_subst_asm terminal_func_comp_elem id_right_unit2, simp)
    then have "p ∘⇩c successor ∘⇩c p' ∘⇩c m = 𝗍"
      using induction_case by (typecheck_cfuncs, simp)
    then show "(p ∘⇩c successor ∘⇩c p') ∘⇩c m = ((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor ∘⇩c p') ∘⇩c m"
      by (etcs_assocr, etcs_subst terminal_func_comp_elem id_right_unit2, -)
  qed
  then obtain s' where
    s'_type[type_rule]: "s' : P → P" and
    s'_def: "p' ∘⇩c s' = successor ∘⇩c p'"
    using p'_uni_prop by (typecheck_cfuncs, metis)

  obtain u where
    u_type[type_rule]: "u : ℕ⇩c → P" and
    u_zero: "u ∘⇩c zero = z'" and
    u_succ: "u ∘⇩c successor = s' ∘⇩c u"
    using natural_number_object_property2 by (typecheck_cfuncs, metis s'_type)

  have p'_u_is_id: "p' ∘⇩c u = id ℕ⇩c"
  proof (etcs_rule natural_number_object_func_unique[where f=successor])
    show "(p' ∘⇩c u) ∘⇩c zero = id⇩c ℕ⇩c ∘⇩c zero"
      by (etcs_subst id_left_unit2, etcs_assocr, simp add: u_zero sym[OF z'_def])
    show "(p' ∘⇩c u) ∘⇩c successor = successor ∘⇩c p' ∘⇩c u"
      by (etcs_assocr, subst u_succ, etcs_assocl, simp add: s'_def)
    show "id⇩c ℕ⇩c ∘⇩c successor = successor ∘⇩c id⇩c ℕ⇩c"
      by (etcs_subst id_right_unit2 id_left_unit2, simp)
  qed

  have "p ∘⇩c p' ∘⇩c u ∘⇩c n = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c p' ∘⇩c u ∘⇩c n"
    by (typecheck_cfuncs, smt comp_associative2 p'_equalizer)
  then show "p ∘⇩c n = 𝗍"
    by (typecheck_cfuncs, smt (z3) comp_associative2 id_left_unit2 id_right_unit2 p'_type p'_u_is_id terminal_func_comp_elem terminal_func_type u_type)
qed
    
subsection ‹Function Iteration›

definition ITER_curried :: "cset ⇒ cfunc" where 
  "ITER_curried U = (THE u . u : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖ ∧  u ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯ ∧
    ((meta_comp U U U) ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯    ∘⇩c u = u ∘⇩c successor)"

lemma ITER_curried_def2: 
"ITER_curried U : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖ ∧  ITER_curried U ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯ ∧
  ((meta_comp U U U) ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯    ∘⇩c ITER_curried U = ITER_curried U  ∘⇩c successor"
  unfolding ITER_curried_def
  by(rule theI', etcs_rule natural_number_object_property2)
  
lemma ITER_curried_type[type_rule]:
  "ITER_curried U : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖"
  by (simp add: ITER_curried_def2)

lemma ITER_curried_zero: 
  "ITER_curried U ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯"
  by (simp add: ITER_curried_def2)

lemma ITER_curried_successor:
"ITER_curried U ∘⇩c successor = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯    ∘⇩c ITER_curried U"
  using ITER_curried_def2 by simp 

definition ITER :: "cset ⇒ cfunc" where 
  "ITER U = (ITER_curried U)⇧♭"

lemma ITER_type[type_rule]:
  "ITER U : ((U⇗U⇖) ×⇩c ℕ⇩c) → (U⇗U⇖)"
  unfolding ITER_def by typecheck_cfuncs

lemma ITER_zero: 
  assumes f_type[type_rule]: "f : Z → (U⇗U⇖)"
  shows "ITER U ∘⇩c ⟨f, zero ∘⇩c β⇘Z⇙⟩ = metafunc (id U) ∘⇩c β⇘Z⇙"
proof(etcs_rule one_separator)
  fix z 
  assume z_type[type_rule]: "z ∈⇩c Z"
  have "(ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩) ∘⇩c z = ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩ ∘⇩c z"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = ITER U ∘⇩c ⟨f ∘⇩c z,zero⟩"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 id_right_unit2 terminal_func_comp_elem)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f ITER_curried U) ∘⇩c ⟨f ∘⇩c z,zero⟩"
    using assms ITER_def comp_associative2 inv_transpose_func_def3 by (typecheck_cfuncs, auto)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,ITER_curried U ∘⇩c zero⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,(metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯⟩"
    using assms by (simp add: ITER_curried_def2)   
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,((left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯⟩"
    using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f  ((left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯) ∘⇩c ⟨f  ∘⇩c z,id⇩c 𝟭⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
  also have "... = (left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭)  ∘⇩c ⟨f  ∘⇩c z,id⇩c 𝟭⟩"
    using assms by (typecheck_cfuncs,simp add: cfunc_type_def comp_associative transpose_func_def)
  also have "... = (left_cart_proj (U) 𝟭)⇧♯"
    using assms by (typecheck_cfuncs, simp add: id_right_unit2 right_cart_proj_cfunc_prod)
  also have "... = (metafunc (id⇩c U))"
    using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
  also have "... = (metafunc (id⇩c U) ∘⇩c β⇘Z⇙) ∘⇩c z"
    using assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative id_right_unit2 terminal_func_comp_elem)
  finally show "(ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩) ∘⇩c z = (metafunc (id⇩c U) ∘⇩c β⇘Z⇙) ∘⇩c z".
qed

lemma ITER_zero': 
  assumes "f ∈⇩c (U⇗U⇖)"
  shows "ITER U ∘⇩c ⟨f, zero⟩ = metafunc (id U)"
  by (typecheck_cfuncs, metis ITER_zero assms id_right_unit2 id_type one_unique_element terminal_func_type)

lemma ITER_succ:
 assumes f_type[type_rule]: "f : Z → (U⇗U⇖)" and n_type[type_rule]: "n : Z → ℕ⇩c"
 shows "ITER U ∘⇩c ⟨f, successor ∘⇩c n⟩ = f □ (ITER U ∘⇩c ⟨f, n ⟩)"
proof(etcs_rule one_separator)
  fix z 
  assume z_type[type_rule]: "z ∈⇩c Z"
  have "(ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩) ∘⇩c z  = ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩ ∘⇩c z"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = ITER U ∘⇩c ⟨f ∘⇩c z, successor ∘⇩c (n  ∘⇩c z)⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f ITER_curried U) ∘⇩c ⟨f ∘⇩c z, successor ∘⇩c (n  ∘⇩c z)⟩"
    using assms by (typecheck_cfuncs, simp add: ITER_def comp_associative2 inv_transpose_func_def3)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (successor ∘⇩c (n  ∘⇩c z))⟩"
    using assms cfunc_cross_prod_comp_cfunc_prod id_left_unit2 by (typecheck_cfuncs, force)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, (ITER_curried U ∘⇩c successor) ∘⇩c (n  ∘⇩c z)⟩"
    using assms by(typecheck_cfuncs, metis comp_associative2)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U) ∘⇩c (n  ∘⇩c z)⟩"
    using assms ITER_curried_successor by presburger
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id (U⇗U⇖) ×⇩f ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U) ∘⇩c (n  ∘⇩c z))∘⇩c ⟨f ∘⇩c z, id 𝟭⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
  also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id (U⇗U⇖) ×⇩f ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ))∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n  ∘⇩c z)⟩"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_right_unit2)
  also have "... = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n  ∘⇩c z)⟩"
    using assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative transpose_func_def)
  also have "... = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)))∘⇩c ⟨⟨f ∘⇩c z,f ∘⇩c z⟩, ITER_curried U ∘⇩c (n  ∘⇩c z)⟩"
    using assms by (etcs_assocr, typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod diag_on_elements id_left_unit2)
  also have "... = meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n  ∘⇩c z)⟩⟩"
    using assms by (typecheck_cfuncs, smt (z3) associate_right_ap comp_associative2)
  also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, eval_func (U⇗U⇖) (U⇗U⇖) ∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n  ∘⇩c z)⟩⟩"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
  also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, eval_func (U⇗U⇖) (U⇗U⇖) ∘⇩c (id(U⇗U⇖) ×⇩f ITER_curried U)∘⇩c ⟨f ∘⇩c z, n ∘⇩c z⟩⟩"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
  also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, ITER U ∘⇩c ⟨f ∘⇩c z, n ∘⇩c z⟩⟩"
    using assms by (typecheck_cfuncs, smt (z3) ITER_def comp_associative2 inv_transpose_func_def3)
  also have "... = meta_comp U U U ∘⇩c ⟨f, ITER U ∘⇩c ⟨f , n⟩⟩ ∘⇩c z"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
  also have "... = (meta_comp U U U ∘⇩c ⟨f, ITER U ∘⇩c ⟨f , n⟩⟩) ∘⇩c z"
    using assms by (typecheck_cfuncs, meson comp_associative2)
  also have "... = (f □ (ITER U ∘⇩c ⟨f,n⟩)) ∘⇩c z"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def5)
  finally show "(ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩) ∘⇩c z = (f □ ITER U ∘⇩c ⟨f,n⟩) ∘⇩c z".
qed

lemma ITER_one:
 assumes "f ∈⇩c (U⇗U⇖)"
 shows "ITER U ∘⇩c ⟨f, successor ∘⇩c zero⟩ = f □ (metafunc (id U))"
  using ITER_succ ITER_zero' assms zero_type by presburger

definition iter_comp :: "cfunc ⇒ cfunc ⇒ cfunc" ("_⇗∘_⇖"[55,0]55) where
  "iter_comp g n  ≡ cnufatem (ITER (domain g) ∘⇩c ⟨metafunc g,n⟩)"

lemma iter_comp_def2: 
  "g⇗∘n⇖  ≡ cnufatem(ITER (domain g) ∘⇩c ⟨metafunc g,n⟩)"
  by (simp add: iter_comp_def)

lemma iter_comp_type[type_rule]:
  assumes "g : X → X"
  assumes "n ∈⇩c ℕ⇩c"
  shows "g⇗∘n⇖: X → X"
  unfolding iter_comp_def2
  by (smt (verit, ccfv_SIG) ITER_type assms cfunc_type_def cnufatem_type comp_type metafunc_type right_param_on_el right_param_type) 

lemma iter_comp_def3: 
  assumes "g : X → X"
  assumes "n ∈⇩c ℕ⇩c"
  shows "g⇗∘n⇖  = cnufatem (ITER X ∘⇩c ⟨metafunc g,n⟩)"
  using assms cfunc_type_def iter_comp_def2 by auto

lemma zero_iters:
  assumes g_type[type_rule]: "g : X → X"
  shows "g⇗∘zero⇖ = id⇩c X"
proof(etcs_rule one_separator)
  fix x 
  assume x_type[type_rule]: "x ∈⇩c X"
  have "(g⇗∘zero⇖) ∘⇩c x = (cnufatem (ITER X ∘⇩c ⟨metafunc g,zero⟩)) ∘⇩c x"
    using assms iter_comp_def3 by (typecheck_cfuncs, auto)
  also have "... = cnufatem (metafunc (id X)) ∘⇩c x"
    by (simp add: ITER_zero' assms metafunc_type)
  also have "... = id⇩c X ∘⇩c x"
    by (metis cnufatem_metafunc id_type)
  also have "... = x"
    by (typecheck_cfuncs, simp add: id_left_unit2)
  ultimately show "(g⇗∘zero⇖) ∘⇩c x = id⇩c X ∘⇩c x"
    by simp
qed

lemma succ_iters:
  assumes "g : X → X"
  assumes "n ∈⇩c ℕ⇩c"
  shows "g⇗∘(successor ∘⇩c n)⇖ = g ∘⇩c (g⇗∘n⇖)"    
proof - 
  have "g⇗∘successor ∘⇩c n⇖   = cnufatem(ITER X ∘⇩c ⟨metafunc g,successor ∘⇩c n ⟩)"
    using assms by (typecheck_cfuncs, simp add: iter_comp_def3)
  also have "... = cnufatem(metafunc g □ ITER X ∘⇩c ⟨metafunc g, n ⟩)"
    using assms by (typecheck_cfuncs, simp add: ITER_succ)
  also have "... = cnufatem(metafunc g □ metafunc (g⇗∘n⇖))"
    using assms by (typecheck_cfuncs, metis iter_comp_def3 metafunc_cnufatem)
  also have "... = g ∘⇩c (g⇗∘n⇖)"
    using assms by (typecheck_cfuncs, simp add: comp_as_metacomp)
  finally show ?thesis.
qed

corollary one_iter:
  assumes "g : X → X"
  shows "g⇗∘(successor ∘⇩c zero)⇖ = g"
  using assms id_right_unit2 succ_iters zero_iters zero_type by force

lemma eval_lemma_for_ITER:
  assumes "f : X → X"
  assumes "x ∈⇩c X"
  assumes "m ∈⇩c ℕ⇩c"
  shows "(f⇗∘m⇖) ∘⇩c x = eval_func X X ∘⇩c ⟨x ,ITER X ∘⇩c ⟨metafunc f ,m⟩⟩"
  using assms by (typecheck_cfuncs, metis eval_lemma iter_comp_def3 metafunc_cnufatem)

lemma n_accessible_by_succ_iter_aux:
   "eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,  ITER ℕ⇩c ∘⇩c ⟨(metafunc successor) ∘⇩c β⇘ℕ⇩c⇙ ,id ℕ⇩c⟩⟩ = id ℕ⇩c"
proof(rule natural_number_object_func_unique[where X="ℕ⇩c", where f = successor])
  show "eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩ : ℕ⇩c → ℕ⇩c"
    by typecheck_cfuncs
  show "id⇩c ℕ⇩c : ℕ⇩c → ℕ⇩c"
    by typecheck_cfuncs
  show "successor : ℕ⇩c → ℕ⇩c"
    by typecheck_cfuncs
next
  have "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c zero =
         eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c zero,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c zero,id⇩c ℕ⇩c ∘⇩c zero⟩⟩"
    by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
  also have "... =  eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero,ITER ℕ⇩c ∘⇩c ⟨metafunc successor,zero⟩⟩"
    by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
  also have "... =  eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero,metafunc (id ℕ⇩c) ⟩"
    by (typecheck_cfuncs, simp add: ITER_zero')
  also have "... = id⇩c ℕ⇩c ∘⇩c zero"
    using eval_lemma by (typecheck_cfuncs, blast)
  finally show "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c zero = id⇩c ℕ⇩c ∘⇩c zero".
  show "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor =
    successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩"
  proof(etcs_rule one_separator)
    fix m
    assume m_type[type_rule]: "m ∈⇩c ℕ⇩c"
    have "(successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c m = 
         successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m,id⇩c ℕ⇩c ∘⇩c m⟩⟩"
      by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
    also have "... = successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ,m⟩⟩"
      by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
    also have "... = successor ∘⇩c (successor⇗∘m⇖) ∘⇩c zero"
      by (typecheck_cfuncs, simp add: eval_lemma_for_ITER)
    also have "... = (successor⇗∘successor ∘⇩c m⇖) ∘⇩c zero"
      by (typecheck_cfuncs, simp add: comp_associative2 succ_iters)
    also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ,successor ∘⇩c m⟩⟩"
      by (typecheck_cfuncs, simp add: eval_lemma_for_ITER)
    also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c (successor ∘⇩c m),ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙∘⇩c (successor ∘⇩c m),id⇩c ℕ⇩c ∘⇩c (successor ∘⇩c m)⟩⟩"
      by (typecheck_cfuncs,simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
    also have "... = ((eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor) ∘⇩c m"
      by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
    ultimately show "((eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor) ∘⇩c m =
         (successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c m"
      by simp
  qed
  show "id⇩c ℕ⇩c ∘⇩c successor = successor ∘⇩c id⇩c ℕ⇩c"
    by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
qed

lemma n_accessible_by_succ_iter:
  assumes "n ∈⇩c ℕ⇩c"
  shows "(successor⇗∘n⇖) ∘⇩c zero = n"
proof - 
  have "n = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙, ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙, id ℕ⇩c⟩⟩ ∘⇩c n"
    using assms by (typecheck_cfuncs, simp add: comp_associative2 id_left_unit2 n_accessible_by_succ_iter_aux)
  also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c n , ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c n, id ℕ⇩c ∘⇩c n⟩⟩"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
  also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero,  ITER ℕ⇩c ∘⇩c ⟨metafunc successor, n⟩⟩"
    using assms by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
  also have "... = (successor⇗∘n⇖) ∘⇩c zero"
    using assms by (typecheck_cfuncs, metis eval_lemma iter_comp_def3 metafunc_cnufatem)
  ultimately show ?thesis
    by simp
qed

subsection ‹Relation of Nat to Other Sets›

lemma oneUN_iso_N:
  "𝟭 ∐ ℕ⇩c ≅ ℕ⇩c"
  using cfunc_coprod_type is_isomorphic_def oneUN_iso_N_isomorphism successor_type zero_type by blast

lemma NUone_iso_N:
  "ℕ⇩c ∐ 𝟭 ≅ ℕ⇩c"
  using coproduct_commutes isomorphic_is_transitive oneUN_iso_N by blast
  
end