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 "β⇘cc 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: "(gc successor) c zero = i1 c zero"
    using comp_associative2 second_diagram3 by (typecheck_cfuncs, force)
  then have u_Eqs_g_s: "u= gc 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: "gc 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.(nc 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 idc 𝟭"
    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 = idc (𝟭  c)  zero ⨿ successor c x = idc 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 = idc c"
  assume "x c zero ⨿ successor = idc (𝟭  c)" "y c zero ⨿ successor = idc (𝟭  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 β⇘cc 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 = idc 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 "idc c c successor = successor c idc 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  (UU)UU⇖⇖   u c zero = (metafunc (id U) c (right_cart_proj (UU) 𝟭)) 
    ((meta_comp U U U) c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖)))    c u = u c successor)"

lemma ITER_curried_def2: 
"ITER_curried U : c  (UU)UU⇖⇖   ITER_curried U c zero = (metafunc (id U) c (right_cart_proj (UU) 𝟭)) 
  ((meta_comp U U U) c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖)))    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  (UU)UU⇖⇖"
  by (simp add: ITER_curried_def2)

lemma ITER_curried_zero: 
  "ITER_curried U c zero = (metafunc (id U) c (right_cart_proj (UU) 𝟭))"
  by (simp add: ITER_curried_def2)

lemma ITER_curried_successor:
"ITER_curried U c successor = (meta_comp U U U c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖)))    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 : ((UU) ×c c)  (UU)"
  unfolding ITER_def by typecheck_cfuncs

lemma ITER_zero: 
  assumes f_type[type_rule]: "f : Z  (UU)"
  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 (UU) (UU)) c (idc (UU) ×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 (UU) (UU)) 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 (UU) (UU)) c f c z,(metafunc (id U) c (right_cart_proj (UU) 𝟭))"
    using assms by (simp add: ITER_curried_def2)   
  also have "... = (eval_func (UU) (UU)) c f c z,((left_cart_proj (U) 𝟭) c (right_cart_proj (UU) 𝟭))"
    using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
  also have "... = (eval_func (UU) (UU)) c (idc (UU) ×f  ((left_cart_proj (U) 𝟭) c (right_cart_proj (UU) 𝟭))) c f  c z,idc 𝟭"
    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 (UU) 𝟭)  c f  c z,idc 𝟭"
    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 (idc U))"
    using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
  also have "... = (metafunc (idc 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 (idc U) c β⇘Z) c z".
qed

lemma ITER_zero': 
  assumes "f c (UU)"
  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  (UU)" 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 (UU) (UU)) c (idc (UU) ×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 (UU) (UU)) 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 (UU) (UU)) 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 (UU) (UU)) c f c z, ((meta_comp U U U c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖))) c ITER_curried U) c (n  c z)"
    using assms ITER_curried_successor by presburger
  also have "... = (eval_func (UU) (UU)) c (id (UU) ×f ((meta_comp U U U c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖))) 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 (UU) (UU)) c (id (UU) ×f ((meta_comp U U U c (id (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖))) ))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 (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)) c (diagonal(UU)×f id ((UU)UU⇖⇖)))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 (UU) ×f eval_func (UU) (UU)) c (associate_right (UU) (UU) ((UU)UU⇖⇖)))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 (UU) ×f eval_func (UU) (UU)) 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 (UU) (UU) 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 (UU) (UU) c (id(UU) ×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 (UU)"
 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= idc 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 "... = idc 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 = idc 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,idc c : c  c"
    by typecheck_cfuncs
  show "idc 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,idc c) c zero =
         eval_func c c c zero c β⇘cc zero,ITER c c metafunc successor c β⇘cc zero,idc 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 "... = idc 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,idc c) c zero = idc c c zero".
  show "(eval_func c c c zero c β⇘c,ITER c c metafunc successor c β⇘c,idc c) c successor =
    successor c eval_func c c c zero c β⇘c,ITER c c metafunc successor c β⇘c,idc 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,idc c) c m = 
         successor c eval_func c c c zero c β⇘cc m,ITER c c metafunc successor c β⇘cc m,idc 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 β⇘cc (successor c m),ITER c c metafunc successor c β⇘cc (successor c m),idc 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,idc 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,idc c) c successor) c m =
         (successor c eval_func c c c zero c β⇘c,ITER c c metafunc successor c β⇘c,idc c) c m"
      by simp
  qed
  show "idc c c successor = successor c idc 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 β⇘cc n , ITER c c metafunc successor c β⇘cc 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