Theory Exponential_Objects

section ‹Exponential Objects, Transposes and Evaluation›

theory Exponential_Objects
  imports Initial
begin

text ‹The axiomatization below corresponds to Axiom 9 (Exponential Objects) in Halvorson.›
axiomatization
  exp_set :: "cset  cset  cset" ("__" [100,100]100) and
  eval_func  :: "cset  cset  cfunc" and
  transpose_func :: "cfunc  cfunc" ("_" [100]100)
where
  exp_set_inj: "XA= YB X = Y  A = B" and
  eval_func_type[type_rule]: "eval_func X A : A×c XA X" and
  transpose_func_type[type_rule]: "f : A ×c Z  X  f : Z  XA⇖" and
  transpose_func_def: "f : A ×c Z  X  (eval_func X A) c (id A ×f f) = f" and
  transpose_func_unique: 
    "f : A×cZ  X  g: Z  XA (eval_func X A) c (id A ×f g) = f  g = f"

lemma eval_func_surj:
  assumes "nonempty(A)"
  shows "surjective((eval_func X A))"
  unfolding surjective_def
proof(clarify)
  fix x
  assume x_type: "x c codomain (eval_func X A)"
  then have x_type2[type_rule]: "x c X"
    using cfunc_type_def eval_func_type by auto
  obtain a where a_def[type_rule]: "a c A"
    using assms nonempty_def by auto
  have needed_type: "a, (x c right_cart_proj A 𝟭) c domain (eval_func X A)"
    using cfunc_type_def by (typecheck_cfuncs, auto)
  have "(eval_func X A) c  a, (x c right_cart_proj A 𝟭) =    
        (eval_func X A) c ((id(A) ×f (x c right_cart_proj A 𝟭)) c a, id(𝟭))"
    by (typecheck_cfuncs, smt a_def cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 x_type2)
  also have "... = ((eval_func X A) c (id(A) ×f (x c right_cart_proj A 𝟭))) c a, id(𝟭)"
    by (typecheck_cfuncs, meson a_def comp_associative2 x_type2)
  also have "... = (x c right_cart_proj A 𝟭) c a, id(𝟭)"
    by (metis comp_type right_cart_proj_type transpose_func_def x_type2) 
  also have "... = x c (right_cart_proj A 𝟭 c a, id(𝟭))"
    using a_def cfunc_type_def comp_associative x_type2 by (typecheck_cfuncs, auto)
  also have "... = x"
    using a_def id_right_unit2 right_cart_proj_cfunc_prod x_type2 by (typecheck_cfuncs, auto)
  ultimately show "y. y c domain (eval_func X A)  eval_func X A c y = x"
    using needed_type by (typecheck_cfuncs, auto)
qed

text ‹The lemma below corresponds to a note above Definition 2.5.1 in Halvorson.›
lemma exponential_object_identity:
  "(eval_func X A) = idc(XA)"
  by (metis cfunc_type_def eval_func_type id_cross_prod id_right_unit id_type transpose_func_unique)

lemma eval_func_X_empty_injective:
  assumes "is_empty Y"
  shows "injective (eval_func X Y)"
  unfolding injective_def
  by (typecheck_cfuncs,metis assms cfunc_type_def comp_type left_cart_proj_type is_empty_def)

subsection ‹Lifting Functions›

text ‹The definition below corresponds to Definition 2.5.1 in Halvorson.›
definition exp_func :: "cfunc  cset  cfunc" ("(_)_f" [100,100]100) where
  "exp_func g A = (g c eval_func (domain g) A)"

lemma exp_func_def2:
  assumes "g : X  Y"
  shows "exp_func g A = (g c eval_func X A)"
  using assms cfunc_type_def exp_func_def by auto

lemma exp_func_type[type_rule]:
  assumes "g : X  Y"
  shows "gAf : XA YA⇖"
  using assms by (unfold exp_func_def2, typecheck_cfuncs)

lemma exp_of_id_is_id_of_exp:
  "id(XA) = (id(X))Af"
  by (metis (no_types) eval_func_type exp_func_def exponential_object_identity id_domain id_left_unit2)

text ‹The lemma below corresponds to a note below Definition 2.5.1 in Halvorson.›
lemma exponential_square_diagram:
  assumes "g : Y  Z"
  shows "(eval_func Z A) c (idc(A)×f gAf)  = g c (eval_func Y A)"
  using assms by (typecheck_cfuncs, simp add: exp_func_def2 transpose_func_def)

text ‹The lemma below corresponds to Proposition 2.5.2 in Halvorson.›
lemma transpose_of_comp:
  assumes f_type: "f: A ×c X  Y" and g_type: "g: Y  Z"
  shows "f: A ×c X  Y  g: Y  Z    (g c f) = gAf c f"
proof clarify
  have left_eq: "(eval_func Z A) c(id(A) ×f (g c f)) = g c f"
    using comp_type f_type g_type transpose_func_def by blast
  have right_eq: "(eval_func Z A) c (idc A ×f (gAf c f)) = g c f"
  proof - 
    have "(eval_func Z A) c (idc A ×f (gAf c f)) =
                   (eval_func Z A) c ((idc A ×f (gAf)) c  (idc A ×f f))"
      by (typecheck_cfuncs, smt identity_distributes_across_composition assms)
    also have "... = (g c eval_func Y A) c  (idc A ×f f)"
      by (typecheck_cfuncs, smt comp_associative2 exp_func_def2 transpose_func_def assms)
    also have "... = g c f"
      by (typecheck_cfuncs, smt (verit, best) comp_associative2 transpose_func_def assms)
    finally show ?thesis.
  qed
  show "(g c f) = gAf c f"
    using assms by (typecheck_cfuncs, metis right_eq transpose_func_unique)
qed

lemma exponential_object_identity2: 
  "id(X)Af = idc(XA)"
  by (metis eval_func_type exp_func_def exponential_object_identity id_domain id_left_unit2)

text ‹The lemma below corresponds to comments below Proposition 2.5.2 and above Definition 2.5.3 in Halvorson.›
lemma eval_of_id_cross_id_sharp1:
  "(eval_func (A ×c X) A) c (id(A) ×f (id(A ×c X)))  = id(A ×c X)"
  using id_type transpose_func_def by blast
lemma eval_of_id_cross_id_sharp2:
  assumes "a : Z  A" "x : Z  X"
  shows "((eval_func (A ×c X) A) c (id(A) ×f (id(A ×c X)))) c a,x = a,x"
  by (smt assms cfunc_cross_prod_comp_cfunc_prod eval_of_id_cross_id_sharp1 id_cross_prod id_left_unit2 id_type)

lemma transpose_factors: 
  assumes "f: X  Y"
  assumes "g: Y  Z"
  shows "(g c f)Af = (gAf) c (fAf)"
  using assms by (typecheck_cfuncs, smt comp_associative2 comp_type eval_func_type exp_func_def2 transpose_of_comp)

subsection ‹Inverse Transpose Function (flat)›

text ‹The definition below corresponds to Definition 2.5.3 in Halvorson.›
definition inv_transpose_func :: "cfunc  cfunc" ("_" [100]100) where
  "f = (THE g.  Z X A. domain f = Z  codomain f = XA g = (eval_func X A) c (id A ×f f))"

lemma inv_transpose_func_def2:
  assumes "f : Z  XA⇖"
  shows " Z X A. domain f = Z  codomain f = XA f = (eval_func X A) c (id A ×f f)"
  unfolding inv_transpose_func_def
proof (rule theI)
  show "Z Y B. domain f = Z  codomain f = YB eval_func X A c idc A ×f f = eval_func Y B c idc B ×f f"
    using assms cfunc_type_def by blast
next
  fix g
  assume "Z X A. domain f = Z  codomain f = XA g = eval_func X A c idc A ×f f"
  then show "g = eval_func X A c idc A ×f f"
    by (metis assms cfunc_type_def exp_set_inj)
qed

lemma inv_transpose_func_def3:
  assumes f_type: "f : Z  XA⇖"
  shows "f = (eval_func X A) c (id A ×f f)"
  by (metis cfunc_type_def exp_set_inj f_type inv_transpose_func_def2)

lemma flat_type[type_rule]:
  assumes f_type[type_rule]: "f : Z  XA⇖"
  shows "f : A ×c Z  X"
  by (etcs_subst inv_transpose_func_def3, typecheck_cfuncs)

text ‹The lemma below corresponds to Proposition 2.5.4 in Halvorson.›
lemma inv_transpose_of_composition:
  assumes "f: X  Y" "g: Y  ZA⇖"
  shows "(g c f) = g c (id(A) ×f f)"
  using assms comp_associative2 identity_distributes_across_composition
  by ((etcs_subst inv_transpose_func_def3)+, typecheck_cfuncs, auto)

text ‹The lemma below corresponds to Proposition 2.5.5 in Halvorson.›
lemma flat_cancels_sharp:
  "f : A ×c Z  X   (f) = f"
  using inv_transpose_func_def3 transpose_func_def transpose_func_type by fastforce

text ‹The lemma below corresponds to Proposition 2.5.6 in Halvorson.›
lemma sharp_cancels_flat:
 "f: Z  XA (f) = f"
proof - 
  assume f_type: "f : Z  XA⇖"
  then have uniqueness: " g. g : Z  XA eval_func X A c (id A ×f g) = f  g = (f)"
    by (typecheck_cfuncs, simp add: transpose_func_unique)
  have "eval_func X A c (id A ×f f) = f"
    by (metis f_type inv_transpose_func_def3)
  then show "f = f"
    using f_type uniqueness by auto
qed

lemma same_evals_equal:
  assumes "f : Z  XA⇖" "g: Z  XA⇖"
  shows "eval_func X A c (id A ×f f) = eval_func X A c (id A ×f g)  f = g"
  by (metis assms inv_transpose_func_def3 sharp_cancels_flat)

lemma sharp_comp:
  assumes f_type[type_rule]: "f : A ×c Z  X" and g_type[type_rule]: "g : W  Z"
  shows "f c g = (f c (id A ×f g))"
proof (etcs_rule same_evals_equal[where X=X, where A=A])

  have "eval_func X A c (id A ×f (f c g)) = eval_func X A c (id A ×f f) c (id A ×f g)"
    using assms by (typecheck_cfuncs, simp add: identity_distributes_across_composition)
  also have "... = f c (id A ×f g)"
    using assms by (typecheck_cfuncs, simp add: comp_associative2 transpose_func_def)
  also have "... = eval_func X A c (idc A ×f (f c (idc A ×f g)))"
    using assms by (typecheck_cfuncs, simp add: transpose_func_def)
  finally show "eval_func X A c (id A ×f (f c g)) = eval_func X A c (idc A ×f (f c (idc A ×f g)))".
qed

lemma flat_pres_epi:
  assumes "nonempty(A)"
  assumes "f : Z  XA⇖"
  assumes "epimorphism f"
  shows "epimorphism(f)"
proof - 
  have equals: "f = (eval_func X A) c (id(A) ×f f)"
    using assms(2) inv_transpose_func_def3 by auto
  have idA_f_epi: "epimorphism((id(A) ×f f))"
    using assms(2) assms(3) cfunc_cross_prod_surj epi_is_surj id_isomorphism id_type iso_imp_epi_and_monic surjective_is_epimorphism by blast
  have eval_epi: "epimorphism((eval_func X A))"
    by (simp add: assms(1) eval_func_surj surjective_is_epimorphism)
  have "codomain ((id(A) ×f f)) = domain ((eval_func X A))"
    using assms(2) cfunc_type_def by (typecheck_cfuncs, auto)
  then show ?thesis
    by (simp add: composition_of_epi_pair_is_epi equals eval_epi idA_f_epi)
qed

lemma transpose_inj_is_inj:
  assumes "g: X  Y"
  assumes "injective g"
  shows "injective(gAf)"
  unfolding injective_def
proof(clarify)
  fix x y 
  assume x_type[type_rule]: "x c domain (gAf)" 
  assume y_type[type_rule]:"y c domain (gAf)"
  assume eqs: "gAf c x = gAf c y"
  have mono_g: "monomorphism g"
    by (meson CollectI assms(2) injective_imp_monomorphism) 
  have x_type'[type_rule]: "x c  XA⇖"
    using assms(1) cfunc_type_def exp_func_type by (typecheck_cfuncs, force)
  have y_type'[type_rule]: "y c  XA⇖"
    using cfunc_type_def x_type x_type' y_type by presburger  
  have "(g c eval_func X A) c x = (g c eval_func X A) c y"
    unfolding exp_func_def using assms eqs exp_func_def2 by force 
  then have "g c (eval_func X A c(id(A) ×f  x)) = g c (eval_func X A c (id(A) ×f  y))"
    by (smt (z3) assms(1) comp_type eqs flat_cancels_sharp flat_type inv_transpose_func_def3 sharp_cancels_flat transpose_of_comp x_type' y_type')
  then have "eval_func X A c(id(A) ×f  x) =   eval_func X A c (id(A) ×f  y)"  
    by (metis assms(1) mono_g flat_type inv_transpose_func_def3  monomorphism_def2 x_type' y_type')
  then show "x = y"
    by (meson same_evals_equal x_type' y_type')
qed

lemma eval_func_X_one_injective:
  "injective (eval_func X 𝟭)"
proof (cases " x. x c X")
  assume "x. x c X"
  then obtain x where x_type: "x c X"
    by auto
  then have "eval_func X 𝟭 c idc 𝟭 ×f (x c β⇘𝟭 ×c 𝟭) = x c β⇘𝟭 ×c 𝟭⇙"
    using comp_type terminal_func_type transpose_func_def by blast
  
  show "injective (eval_func X 𝟭)"
    unfolding injective_def
  proof clarify
    fix a b
    assume a_type: "a c domain (eval_func X 𝟭)"
    assume b_type: "b c domain (eval_func X 𝟭)"
    assume evals_equal: "eval_func X 𝟭 c a = eval_func X 𝟭 c b"

    have eval_dom: "domain(eval_func X 𝟭) = 𝟭 ×c (X𝟭)"
      using cfunc_type_def eval_func_type by auto

    obtain A where a_def: "A c X𝟭 a = id 𝟭, A"
      by (typecheck_cfuncs, metis a_type cart_prod_decomp eval_dom terminal_func_unique)

    obtain B where b_def: "B c X𝟭 b = id 𝟭, B"
      by (typecheck_cfuncs, metis b_type cart_prod_decomp eval_dom terminal_func_unique)

    have "A c id 𝟭, id 𝟭 = B c id 𝟭, id 𝟭"
    proof - 
      have "A c id 𝟭 , id 𝟭 = (eval_func X 𝟭) c (id 𝟭 ×f (A)) c id 𝟭, id 𝟭"
        by (typecheck_cfuncs, smt (verit, best) a_def comp_associative2 inv_transpose_func_def3 sharp_cancels_flat)
      also have "... = eval_func X 𝟭 c a"
        using a_def cfunc_cross_prod_comp_cfunc_prod id_right_unit2 sharp_cancels_flat by (typecheck_cfuncs, force)
      also have "... = eval_func X 𝟭 c b"
        by (simp add: evals_equal)
      also have "... = (eval_func X 𝟭) c (id 𝟭 ×f (B)) c id 𝟭, id 𝟭"
        using b_def cfunc_cross_prod_comp_cfunc_prod id_right_unit2 sharp_cancels_flat by (typecheck_cfuncs, auto)
      also have "... = B c id 𝟭, id 𝟭"
        by (typecheck_cfuncs, smt (verit) b_def comp_associative2 inv_transpose_func_def3 sharp_cancels_flat)
      finally show "A c id 𝟭, id 𝟭 = B c id 𝟭, id 𝟭".
    qed
    then have "A = B"
      by (typecheck_cfuncs, smt swap_def a_def b_def cfunc_prod_comp comp_associative2 diagonal_def diagonal_type id_right_unit2 id_type left_cart_proj_type right_cart_proj_type swap_idempotent swap_type terminal_func_comp terminal_func_unique)
    then have "A = B"
      by (metis a_def b_def sharp_cancels_flat)
    then show "a = b"
      by (simp add: a_def b_def)
  qed
next
  assume "x. x c X"
  then show "injective (eval_func X 𝟭)"
    by (typecheck_cfuncs, metis  cfunc_type_def comp_type injective_def)
qed

text ‹In the lemma below, the nonempty assumption is required.
      Consider, for example, @{term "X = Ω"} and @{term "A = "}
lemma sharp_pres_mono:
  assumes "f : A ×c Z  X"
  assumes "monomorphism(f)"
  assumes "nonempty A"
  shows   "monomorphism(f)"
  unfolding monomorphism_def2
proof(clarify)
  fix g h U Y x
  assume g_type[type_rule]: "g : U  Y"
  assume h_type[type_rule]: "h : U  Y"
  assume f_sharp_type[type_rule]: "f : Y  x"
  assume equals: "f c g = f c h"

  have f_sharp_type2: "f : Z  XA⇖"
    by (simp add: assms(1) transpose_func_type)
  have Y_is_Z: "Y = Z"
    using cfunc_type_def f_sharp_type f_sharp_type2 by auto
  have x_is_XA: "x = XA⇖"
    using cfunc_type_def f_sharp_type f_sharp_type2 by auto
  have g_type2: "g : U  Z"
    using Y_is_Z g_type by blast
  have h_type2: "h : U  Z"
    using Y_is_Z h_type by blast
  have idg_type: "(id(A) ×f g) : A ×c U  A ×c Z"
    by (simp add: cfunc_cross_prod_type g_type2 id_type)
  have idh_type: "(id(A) ×f h) : A ×c U  A ×c Z"
    by (simp add: cfunc_cross_prod_type h_type2 id_type)

   then have epic: "epimorphism(right_cart_proj A U)"
     using assms(3) nonempty_left_imp_right_proj_epimorphism by blast

   have fIdg_is_fIdh: "f c (id(A) ×f g) = f c (id(A) ×f h)"
   proof - 
    have "f c (id(A) ×f g) = (eval_func X A c (id(A) ×f f)) c (id(A) ×f g)"
      using assms(1) transpose_func_def by auto
    also have "... = (eval_func X A c (id(A) ×f f)) c (id(A) ×f h)"
      by (metis Y_is_Z equals f_sharp_type2 g_type h_type inv_transpose_func_def3 inv_transpose_of_composition)
    also have "... = f c (id(A) ×f h)"
      using assms(1) transpose_func_def by auto
    finally show ?thesis.   
   qed
   then have idg_is_idh: "(id(A) ×f g) = (id(A) ×f h)"
    using assms fIdg_is_fIdh idg_type idh_type monomorphism_def3 by blast
   then have "g c (right_cart_proj A U) = h c (right_cart_proj A U)"
    by (smt g_type2 h_type2 id_type right_cart_proj_cfunc_cross_prod)
   then show "g = h"
    using epic epimorphism_def2 g_type2 h_type2 right_cart_proj_type by blast
qed

subsection ‹Metafunctions and their Inverses (Cnufatems)›

subsubsection ‹Metafunctions›

definition metafunc :: "cfunc  cfunc" where
  "metafunc f  (f c (left_cart_proj (domain f) 𝟭))"

lemma metafunc_def2:
  assumes "f : X  Y"
  shows "metafunc f = (f c (left_cart_proj X 𝟭))"
  using assms unfolding metafunc_def cfunc_type_def by auto

lemma metafunc_type[type_rule]:
  assumes "f : X  Y"
  shows "metafunc f c YX⇖"
  using assms by (unfold metafunc_def2, typecheck_cfuncs)

lemma eval_lemma:
  assumes f_type[type_rule]: "f : X  Y"
  assumes x_type[type_rule]: "x  c X"
  shows "eval_func Y X c x, metafunc f = f c x"
proof - 
  have "eval_func Y X c x, metafunc f = eval_func Y X c (id X ×f (f c (left_cart_proj X 𝟭))) c x, id 𝟭"
    by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 metafunc_def2)
  also have "... = (eval_func Y X c (id X ×f (f c (left_cart_proj X 𝟭)))) c x, id 𝟭"
    using comp_associative2 by (typecheck_cfuncs, blast)
  also have "... = (f c (left_cart_proj X 𝟭)) c x, id 𝟭"
    by (typecheck_cfuncs, metis transpose_func_def)
  also have "... = f c x"
    by (typecheck_cfuncs, metis assms cfunc_type_def comp_associative left_cart_proj_cfunc_prod)
  finally show "eval_func Y X c x, metafunc f = f c x".
qed

subsubsection ‹Inverse Metafunctions (Cnufatems)›

definition cnufatem :: "cfunc  cfunc" where
  "cnufatem f = (THE g.  Y X. f : 𝟭  YX g = eval_func Y X c id X, f c β⇘X)"

lemma cnufatem_def2:
  assumes "f c YX⇖"
  shows "cnufatem f = eval_func Y X c id X, f c β⇘X"
  using assms unfolding cnufatem_def cfunc_type_def
  by (smt (verit, ccfv_threshold) exp_set_inj theI') 

lemma cnufatem_type[type_rule]:
  assumes "f c YX⇖"
  shows "cnufatem f : X   Y"
  using assms cnufatem_def2 
  by (auto, typecheck_cfuncs)

lemma cnufatem_metafunc:
  assumes f_type[type_rule]: "f : X  Y"
  shows "cnufatem (metafunc f) = f"
proof(etcs_rule one_separator)
  fix x
  assume x_type[type_rule]: "x c X"

  have "cnufatem (metafunc f) c x =  eval_func Y X c id X, (metafunc f) c β⇘X c x"
    using cnufatem_def2 comp_associative2 by (typecheck_cfuncs, fastforce)
  also have "... = eval_func Y X c x, (metafunc f)"
    by (typecheck_cfuncs, metis cart_prod_extract_left)
  also have "... = f c x"
    using eval_lemma by (typecheck_cfuncs, presburger)
  finally show "cnufatem (metafunc f) c x = f c x".
qed

lemma metafunc_cnufatem:
  assumes f_type[type_rule]: "f c YX⇖"
  shows "metafunc (cnufatem f) = f"
proof (etcs_rule same_evals_equal[where X = Y, where A = X], etcs_rule one_separator)
  fix x1
  assume x1_type[type_rule]: "x1 c X ×c 𝟭"
  then obtain x where x_type[type_rule]: "x c X" and x_def: " x1 = x, id 𝟭"
    by (typecheck_cfuncs, metis cart_prod_decomp one_unique_element)
  have "(eval_func Y X c idc X ×f metafunc (cnufatem f)) c x, id 𝟭 =
         eval_func Y X c x , metafunc (cnufatem f)"
    by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_left_unit2 id_right_unit2)
  also have "... = (cnufatem f) c x"
    using eval_lemma by (typecheck_cfuncs, presburger)
  also have "... = (eval_func Y X c id X, f c β⇘X) c x"
    using assms cnufatem_def2 by presburger
  also have "... = eval_func Y X c id X, f c β⇘X c x"
    by (typecheck_cfuncs, metis comp_associative2)
  also have "... = eval_func Y X c id X c x , f c (β⇘Xc x)"
    by (typecheck_cfuncs, metis cart_prod_extract_left id_left_unit2 id_right_unit2 terminal_func_comp_elem)
  also have "... = eval_func Y X c id X c x , f c id 𝟭"
    by (simp add: terminal_func_comp_elem x_type)
  also have "... = eval_func Y X c (idc X ×f f) c x, id 𝟭"
    using cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, force)
  also have "... = (eval_func Y X c idc X ×f f) c x1"
    by (typecheck_cfuncs, metis comp_associative2 x_def)
  ultimately show "(eval_func Y X c idc X ×f metafunc (cnufatem f)) c x1 = (eval_func Y X c idc X ×f f) c x1"
    using x_def by simp
qed

subsubsection ‹Metafunction Composition›

definition meta_comp :: "cset  cset  cset  cfunc"  where 
  "meta_comp X Y Z  = (eval_func Z Y c swap (ZY) Y c (id(ZY) ×f (eval_func Y X c swap (YX) X)) c (associate_right (ZY) (YX) X) c swap X ((ZY) ×c (YX)))"

lemma meta_comp_type[type_rule]:
  "meta_comp X Y Z : ZY×c YX ZX⇖"
  unfolding meta_comp_def by typecheck_cfuncs

definition meta_comp2 :: "cfunc  cfunc  cfunc" (infixr "" 55)
  where "meta_comp2 f g = (THE h.  W X Y. g : W  YX h = (f  c g, right_cart_proj X W))"

lemma meta_comp2_def2: 
  assumes "f: W  ZY⇖"
  assumes "g: W  YX⇖"
  shows "f  g  = (f  c g, right_cart_proj X W)"
  using assms unfolding meta_comp2_def
  by (smt (z3) cfunc_type_def exp_set_inj the_equality)

lemma meta_comp2_type[type_rule]: 
  assumes "f: W  ZY⇖"
  assumes "g: W  YX⇖"
  shows "f  g : W  ZX⇖"
proof - 
  have "(f  c g, right_cart_proj X W) : W  ZX⇖"
    using assms by typecheck_cfuncs
  then show ?thesis 
    using assms by (simp add: meta_comp2_def2)
qed

lemma meta_comp2_elements_aux: 
  assumes "f c ZY⇖"
  assumes "g c YX⇖"
  assumes "x c X"
  shows "(f c g,right_cart_proj X 𝟭)  c x, idc 𝟭 = eval_func Z Y c eval_func Y X c x,g,f"
proof-
    have "(f c g,right_cart_proj X 𝟭)  c x, idc 𝟭=  f c g,right_cart_proj X 𝟭  c x, idc 𝟭"
      using assms by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = f c g c x, idc 𝟭,right_cart_proj X 𝟭 c x, idc 𝟭 "
      using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp)
    also have "... = f c g c x, idc 𝟭,idc 𝟭"
      using assms by (typecheck_cfuncs, metis one_unique_element)
    also have "... = f c (eval_func Y X) c (id X ×f g) c x, idc 𝟭,idc 𝟭"
      using assms by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3)
    also have "... = f c (eval_func Y X) c  x, g,idc 𝟭"
      using assms cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 by (typecheck_cfuncs,force)
    also have "... = (eval_func Z Y) c (id Y ×f f) c (eval_func Y X) c  x, g,idc 𝟭"
      using assms by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3)
    also have "... = (eval_func Z Y) c  (eval_func Y X) c  x, g,f"
      using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
    finally show "(f c g,right_cart_proj X 𝟭) c x,idc 𝟭 = eval_func Z Y c eval_func Y X c x,g,f".
qed

lemma meta_comp2_def3: 
  assumes "f c ZY⇖"
  assumes "g c YX⇖"
  shows "f  g = metafunc ((cnufatem f) c (cnufatem g))"
  using assms
proof(unfold meta_comp2_def2 cnufatem_def2 metafunc_def meta_comp_def)          
  have "f c g,right_cart_proj X 𝟭 = ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c  left_cart_proj X 𝟭"
  proof(rule one_separator[where X = "X ×c 𝟭", where Y = Z])
    show "f c g,right_cart_proj X 𝟭 : X ×c 𝟭  Z"
      using assms by typecheck_cfuncs
    show "((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭 : X ×c 𝟭  Z"
      using assms by typecheck_cfuncs
  next
    fix x1 
    assume x1_type[type_rule]: "x1  c (X ×c 𝟭)"
    then obtain x where x_type[type_rule]: "x c X" and x_def: "x1 = x, idc 𝟭"
      by (metis cart_prod_decomp id_type terminal_func_unique)
    then have "(f c g,right_cart_proj X 𝟭) c x1 = eval_func Z Y c eval_func Y X c x,g,f"
      using assms meta_comp2_elements_aux x_def by blast
    also have "... = eval_func Z Y c idc Y,f c β⇘Y c eval_func Y X c idc X,g c β⇘X c x"
      using assms by (typecheck_cfuncs, metis cart_prod_extract_left)
    also have "... =  (eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X c x"
      using assms by (typecheck_cfuncs, meson comp_associative2)
    also have "... = ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c x"
      using assms by (typecheck_cfuncs, simp add: comp_associative2)
    also have "... = ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭 c x1"
      using assms id_type left_cart_proj_cfunc_prod x_def by (typecheck_cfuncs, auto)
    also have "... = (((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭) c x1"
      using assms by (typecheck_cfuncs, meson comp_associative2)
    finally show "(f c g,right_cart_proj X 𝟭) c x1 = (((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭) c x1".      
  qed
  then show "(f c g,right_cart_proj X 𝟭) = (((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj (domain ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X)) 𝟭)"
    using assms cfunc_type_def cnufatem_def2 cnufatem_type domain_comp by force
qed

lemma meta_comp2_def4:
  assumes f_type[type_rule]: "f c ZY⇖" and g_type[type_rule]: "g c YX⇖"
  shows "f  g   = meta_comp X Y Z c f,g"
  using assms 
proof(unfold meta_comp2_def2 cnufatem_def2 metafunc_def meta_comp_def)          
  have "(((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭) =  
          (eval_func Z Y c  swap (ZY) Y c  (idc (ZY) ×f (eval_func Y X c swap (YX) X)) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c (id (X)  ×f  f,g)"
  proof(etcs_rule one_separator)
    fix x1 
    assume x1_type[type_rule]: "x1  c X ×c 𝟭"
    then obtain x where x_type[type_rule]: "x c X" and x_def: "x1 = x, idc 𝟭"
      by (metis cart_prod_decomp id_type terminal_func_unique)
    have "(((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭) c x1 = 
           ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭 c x1"
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
    also have "... = ((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c x"
      using id_type left_cart_proj_cfunc_prod x_def by (typecheck_cfuncs, presburger)
    also have "... =  (eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X c x"
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
    also have "... = eval_func Z Y c idc Y,f c β⇘Y c eval_func Y X c idc X,g c β⇘X c x"
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative)
    also have "... = eval_func Z Y c idc Y,f c β⇘Y c eval_func Y X c x ,g"
      by (typecheck_cfuncs, metis cart_prod_extract_left)
    also have "... = eval_func Z Y c eval_func Y X c x ,g ,f"
      by (typecheck_cfuncs, metis cart_prod_extract_left)
    also have "... = (eval_func Z Y c swap (ZY) Y) c f , eval_func Y X c  x, g"
      by (typecheck_cfuncs, metis comp_associative2 swap_ap)
    also have "... = (eval_func Z Y c swap (ZY) Y) c idc (ZY)  c  f , (eval_func Y X c swap (YX) X)  c g, x"
      by (typecheck_cfuncs, smt (z3) comp_associative2 id_left_unit2 swap_ap)
    also have "... = (eval_func Z Y c swap (ZY) Y) c (idc (ZY) ×f (eval_func Y X c swap (YX) X)) c   f,g, x"
      using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X)) c   f,g, x"
      using assms comp_associative2 by (typecheck_cfuncs, force)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X)) c associate_right (ZY) (YX) X c   f,g, x "
      using assms by (typecheck_cfuncs, simp add: associate_right_ap)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X) c   f,g, x "
      using assms comp_associative2 by (typecheck_cfuncs, force)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X) c swap X (ZY×c YX) c   x,  f,g"
      using assms by (typecheck_cfuncs, simp add: swap_ap)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c   x,  f,g"
      using assms comp_associative2 by (typecheck_cfuncs, force)
    also have "... = (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c   ((idc X ×f f,g) c  x1)"
      using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2 id_type x_def)
    also have "... = ((eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c idc X ×f f,g) c x1"
      by (typecheck_cfuncs, meson comp_associative2)
    finally show "(((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c left_cart_proj X 𝟭) c x1 =
         ((eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c idc X ×f f,g) c x1".
  qed
  then have "(((eval_func Z Y c idc Y,f c β⇘Y) c eval_func Y X c idc X,g c β⇘X) c
     left_cart_proj X 𝟭) =  (eval_func Z Y c  swap (ZY) Y c (idc (ZY) ×f (eval_func Y X c swap (YX) X))
         c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c f,g"
    using assms by (typecheck_cfuncs, simp add: sharp_comp)  
  then show "(f c g,right_cart_proj X 𝟭) =
    (eval_func Z Y c swap (ZY) Y c (idc (ZY) ×f eval_func Y X c swap (YX) X) c associate_right (ZY) (YX) X c swap X (ZY×c YX)) c f,g"
    using assms cfunc_type_def cnufatem_def2 cnufatem_type domain_comp meta_comp2_def2 meta_comp2_def3 metafunc_def by force
qed

lemma meta_comp_on_els:
  assumes "f : W  ZY⇖"
  assumes "g : W  YX⇖"
  assumes "w c W"
  shows "(f  g) c w = (f c w)  (g c w)"
proof - 
  have "(f  g) c w = (f c g, right_cart_proj X W) c w"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
  also have "... = (eval_func Z Y c (id Y ×f f) c eval_func Y X c (id X ×f g), right_cart_proj X W) c w"
    using assms comp_associative2 inv_transpose_func_def3 by (typecheck_cfuncs, force)
  also have "... = (eval_func Z Y c eval_func Y X c (id X ×f g), f c right_cart_proj X W) c w"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
  also have "... = (eval_func Z Y c eval_func Y X c (id X ×f (gc w)), (f c w) c right_cart_proj X 𝟭)"
  proof - 
    have "(eval_func Z Y c eval_func Y X c (id X ×f g), f c right_cart_proj X W) c (id X ×f w) = 
          eval_func Z Y c eval_func Y X c (id X ×f (gc w)), f c right_cart_proj X W c (id X ×f w)"
    proof - 
      have "eval_func Z Y c eval_func Y X c (id X ×f g), f c right_cart_proj X W c (id X ×f w) 
          =  eval_func Z Y c (eval_func Y X c (id X ×f g)) c (id X ×f w), (f c right_cart_proj X W) c (id X ×f w)"
         using assms cfunc_prod_comp by (typecheck_cfuncs, force)
       also have "... = eval_func Z Y c eval_func Y X c (id X ×f g) c (id X ×f w), f c right_cart_proj X W c (id X ×f w)"
         using assms comp_associative2 by (typecheck_cfuncs, auto)
       also have "... = eval_func Z Y c eval_func Y X c (id X ×f (gc w)), f c right_cart_proj X W c (id X ×f w)"
         using assms by (typecheck_cfuncs, metis identity_distributes_across_composition)
       ultimately show ?thesis
         using assms comp_associative2 flat_cancels_sharp by (typecheck_cfuncs, auto)
     qed
     then show ?thesis
       using assms by (typecheck_cfuncs, smt (z3) comp_associative2 inv_transpose_func_def3 
       inv_transpose_of_composition right_cart_proj_cfunc_cross_prod transpose_func_unique)
  qed
  also have "... = (eval_func Z Y c (idc Y ×f ((f c w) c right_cart_proj X 𝟭)) c eval_func Y X c (id X ×f (gc w)), id (X×c 𝟭))"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
  also have "... = (eval_func Z Y c (idc Y ×f (f c w)) c (id (Y) ×f right_cart_proj X 𝟭) c eval_func Y X c (id X ×f (gc w)), id (X×c 𝟭))"
    using assms comp_associative2 identity_distributes_across_composition by (typecheck_cfuncs, force)
  also have "... = ((fcw) c (id (Y) ×f right_cart_proj X 𝟭) c eval_func Y X c (id X ×f (gc w)), id (X×c 𝟭))"
    using assms by (typecheck_cfuncs, smt (z3) comp_associative2 inv_transpose_func_def3)
  also have "... = ((fcw) c (id (Y) ×f right_cart_proj X 𝟭) c (gc w), id (X×c 𝟭))"
    using assms inv_transpose_func_def3 by (typecheck_cfuncs, force)
  also have "... = ((fc w) c (gc w), right_cart_proj X 𝟭)"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
  also have "... = (fc w)  (g c w)"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
  finally show ?thesis.
qed

lemma meta_comp2_def5:
  assumes "f : W  ZY⇖"
  assumes "g : W  YX⇖"
  shows "f  g   = meta_comp X Y Z c f,g"
proof(rule one_separator[where X = W, where Y = "ZX⇖"])
  show "f  g : W  ZX⇖"
    using assms by typecheck_cfuncs
  show "meta_comp X Y Z c f,g : W  ZX⇖"
    using assms by typecheck_cfuncs
next
  fix w 
  assume w_type[type_rule]: "w c W"
  have "(meta_comp X Y Z c f,g) c w = meta_comp X Y Z c f,g c w"
    using assms by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = meta_comp X Y Z c f c w, g c w"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp)
  also have "... = (fc w)  (g c w)"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def4)
  also have "... = (f  g) c w"
    using assms by (typecheck_cfuncs, simp add: meta_comp_on_els)
  ultimately show "(f  g) c w = (meta_comp X Y Z c f,g) c w"
    by simp
qed

lemma meta_left_identity:
  assumes "g c XX⇖"
  shows "g  metafunc (id X) = g"
  using assms by (typecheck_cfuncs, metis cfunc_type_def cnufatem_metafunc cnufatem_type id_right_unit meta_comp2_def3 metafunc_cnufatem)
  
lemma meta_right_identity:
  assumes "g c XX⇖"
  shows "metafunc(id X)  g = g"
  using assms by (typecheck_cfuncs, smt (z3) cnufatem_metafunc cnufatem_type id_left_unit2 meta_comp2_def3 metafunc_cnufatem)

lemma comp_as_metacomp:
  assumes "g : X  Y"
  assumes "f : Y  Z"
  shows "f c g = cnufatem(metafunc f  metafunc g)"
  using assms by (typecheck_cfuncs, simp add: cnufatem_metafunc meta_comp2_def3)

lemma metacomp_as_comp:
  assumes "g c YX⇖"
  assumes "f c ZY⇖"
  shows "cnufatem f c cnufatem g = cnufatem(f  g)"
  using assms by (typecheck_cfuncs, simp add: comp_as_metacomp metafunc_cnufatem)

lemma meta_comp_assoc:
  assumes "e : W  AZ⇖"
  assumes "f : W  ZY⇖"
  assumes "g : W  YX⇖"
  shows "(e  f)   g  = e  (f  g)"
proof -
  have "(e  f)   g = (e c f, right_cart_proj Y W)  g"
    using assms by (simp add: meta_comp2_def2)
  also have "... = ((e c f, right_cart_proj Y W) c g, right_cart_proj X W)"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
  also have "... = ((e c f, right_cart_proj Y W) c g, right_cart_proj X W)"
    using assms by (typecheck_cfuncs, simp add: flat_cancels_sharp)    
  also have "... = (e c f c g, right_cart_proj X W ,right_cart_proj X W)"
    using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 right_cart_proj_cfunc_prod)
  also have "... = (e c (f c g, right_cart_proj X W) ,right_cart_proj X W)"
    using assms by (typecheck_cfuncs, simp add: flat_cancels_sharp)
  also have "... = e  (f c g, right_cart_proj X W)"
    using assms by (typecheck_cfuncs, simp add: meta_comp2_def2)
  also have "... = e  (f  g)"
    using assms by (simp add: meta_comp2_def2)
  finally show ?thesis.
qed

subsection ‹Partially Parameterized Functions on Pairs›

definition left_param :: "cfunc  cfunc  cfunc" ("_⇘[_,-]⇙" [100,0]100) where
  "left_param k p  (THE f.   P Q R. k : P ×c Q  R  f = k c p c β⇘Q, id Q)"

lemma left_param_def2:
  assumes "k : P ×c Q  R"
  shows "k⇘[p,-]⇙  k c p c β⇘Q, id Q"
proof - 
  have " P Q R. k : P ×c Q  R  left_param k p = k c p c β⇘Q, id Q"
    unfolding left_param_def by (smt (z3) cfunc_type_def the1I2 transpose_func_type assms) 
  then show "k⇘[p,-]⇙  k c p c β⇘Q, id Q"
    by (smt (z3) assms cfunc_type_def transpose_func_type)
qed

lemma left_param_type[type_rule]:
  assumes "k : P ×c Q  R"
  assumes "p c P"
  shows "k⇘[p,-]⇙ : Q  R"
  using assms by (unfold left_param_def2, typecheck_cfuncs)

lemma left_param_on_el:
  assumes "k : P ×c Q  R"
  assumes "p c P"
  assumes "q c Q"
  shows  "k⇘[p,-]⇙ c q = k c p, q"
proof - 
  have "k⇘[p,-]⇙ c q = k c p c β⇘Q, id Q  c q"
    using assms cfunc_type_def comp_associative left_param_def2 by (typecheck_cfuncs, force)
  also have "... = k c p, q"
    using  assms(2,3) cart_prod_extract_right by force
  finally show ?thesis.
qed

definition right_param :: "cfunc  cfunc  cfunc" ("_⇘[-,_]⇙" [100,0]100) where
  "right_param k q  (THE f.   P Q R. k : P ×c Q  R  f = k c id P, q c β⇘P)"

lemma right_param_def2:
  assumes "k : P ×c Q  R"
  shows "k⇘[-,q]⇙  k c id P, q c β⇘P"
proof - 
  have " P Q R. k : P ×c Q  R  right_param k q = k c id P, q c β⇘P"
    unfolding right_param_def by (rule theI', insert assms, auto, metis cfunc_type_def exp_set_inj transpose_func_type) 
  then show "k⇘[-,q]⇙  k c idc P,q c β⇘P"
    by (smt (z3) assms cfunc_type_def exp_set_inj transpose_func_type)
qed

lemma right_param_type[type_rule]:
  assumes "k : P ×c Q  R"
  assumes "q c Q"
  shows "k⇘[-,q]⇙ : P  R"
  using assms by (unfold right_param_def2, typecheck_cfuncs)

lemma right_param_on_el:
  assumes "k : P ×c Q  R"
  assumes "p c P"
  assumes "q c Q"
  shows  "k⇘[-,q]⇙ c p = k c p, q"
proof - 
  have "k⇘[-,q]⇙ c p = k c  id P, q c β⇘P  c p"
    using assms cfunc_type_def comp_associative right_param_def2 by (typecheck_cfuncs, force)
  also have "... = k c p, q"
    using assms(2,3) cart_prod_extract_left by force
  finally show ?thesis.
qed

subsection ‹Exponential Set Facts›

text ‹The lemma below corresponds to Proposition 2.5.7 in Halvorson.›
lemma exp_one:
  "X𝟭 X"
proof -
  obtain e where e_defn: "e = eval_func X 𝟭" and e_type: "e : 𝟭 ×c X𝟭 X"
    using eval_func_type by auto
  obtain i where i_type: "i: 𝟭 ×c 𝟭  𝟭"
    using terminal_func_type by blast
  obtain i_inv where i_iso: "i_inv: 𝟭  𝟭 ×c 𝟭  
                             i c i_inv = id(𝟭)   
                             i_inv c i = id(𝟭 ×c 𝟭)"
    by (smt cfunc_cross_prod_comp_cfunc_prod cfunc_cross_prod_comp_diagonal cfunc_cross_prod_def cfunc_prod_type cfunc_type_def diagonal_def i_type id_cross_prod id_left_unit id_type left_cart_proj_type right_cart_proj_cfunc_prod right_cart_proj_type terminal_func_unique)
  then have i_inv_type: "i_inv: 𝟭  𝟭 ×c 𝟭"
    by auto

  have inj: "injective(e)"
    by (simp add: e_defn eval_func_X_one_injective)

  have surj: "surjective(e)"
     unfolding surjective_def
   proof clarify
    fix y 
    assume "y c codomain e"
    then have y_type: "y c X"
      using cfunc_type_def e_type by auto

    have witness_type: "(idc 𝟭 ×f (y c i)) c i_inv c 𝟭 ×c X𝟭⇖"
      using y_type i_type i_inv_type by typecheck_cfuncs

    have square: "e c (id(𝟭) ×f (y c i)) = y c i"
      using comp_type e_defn i_type transpose_func_def y_type by blast
    then show "x. x c domain e  e c x = y" 
      unfolding cfunc_type_def using y_type i_type i_inv_type e_type 
      by (intro exI[where x="(id(𝟭) ×f (y c i)) c i_inv"], typecheck_cfuncs, metis cfunc_type_def comp_associative i_iso id_right_unit2)
  qed

  have "isomorphism e"
    using epi_mon_is_iso inj injective_imp_monomorphism surj surjective_is_epimorphism by fastforce
  then show "X𝟭 X"
    using e_type is_isomorphic_def isomorphic_is_symmetric isomorphic_is_transitive one_x_A_iso_A by blast
qed

text ‹The lemma below corresponds to Proposition 2.5.8 in Halvorson.›
lemma exp_empty:
  "X 𝟭"
proof - 
  obtain f where f_type: "f = α⇘Xc (left_cart_proj  𝟭)" and fsharp_type[type_rule]: "f c X⇖"
    using transpose_func_type by (typecheck_cfuncs, force)
  have uniqueness: "z. z c X z=f"
  proof clarify
    fix z
    assume z_type[type_rule]: "z c X⇖"
    obtain j where j_iso:"j:   ×c 𝟭  isomorphism(j)"
      using is_isomorphic_def isomorphic_is_symmetric empty_prod_X by presburger
    obtain ψ where psi_type: "ψ :  ×c 𝟭   
                     j c ψ = id( ×c 𝟭)  ψ c j = id()"
      using cfunc_type_def isomorphism_def j_iso by fastforce 
    then have f_sharp : "id()×f z = id()×f f"
      by (typecheck_cfuncs, meson comp_type emptyset_is_empty one_separator)
    then show "z = f"
      using  fsharp_type same_evals_equal z_type by force
  qed
  then have "∃! x. x c X⇖"
    by (intro ex1I[where a="f"], simp_all add: fsharp_type)
  then show "X 𝟭"
    using single_elem_iso_one by auto
qed

lemma one_exp:
  "𝟭X 𝟭"
proof - 
  have nonempty: "nonempty(𝟭X)"
    using nonempty_def right_cart_proj_type transpose_func_type by blast
  obtain e where e_defn: "e = eval_func 𝟭 X" and e_type: "e : X ×c 𝟭X 𝟭"
    by (simp add: eval_func_type)
  have uniqueness: "y. (yc 𝟭X e c (id(X) ×f y) : X ×c 𝟭   𝟭)"
    by (meson cfunc_cross_prod_type comp_type e_type id_type)
  have uniquess_form: "y. (yc 𝟭X e c (id(X) ×f y) = β⇘X ×c 𝟭)"
    using terminal_func_unique uniqueness by blast
  then have ex1: "(∃! x. x c 𝟭X)"
    by (metis e_defn nonempty nonempty_def transpose_func_unique uniqueness)
  show "𝟭X 𝟭"
    using ex1 single_elem_iso_one by auto
qed

text ‹The lemma below corresponds to Proposition 2.5.9 in Halvorson.›
lemma power_rule:
  "(X ×c Y)A XA×c YA⇖"
proof - 
  have "is_cart_prod ((X ×c Y)A) ((left_cart_proj X Y)Af) (right_cart_proj X YAf) (XA) (YA)"
  proof (etcs_subst is_cart_prod_def2, clarify)
    fix f g Z 
    assume f_type[type_rule]: "f : Z  XA⇖"
    assume g_type[type_rule]: "g : Z  YA⇖"

    show "h. h : Z  (X ×c Y)A
           left_cart_proj X YAf c h = f 
           right_cart_proj X YAf c h = g 
           (h2. h2 : Z  (X ×c Y)A left_cart_proj X YAf c h2 = f  right_cart_proj X YAf c h2 = g 
                 h2 = h)"
    proof (intro exI[where x="f ,g"], safe, typecheck_cfuncs)
      have "((left_cart_proj X Y)Af) c f ,g = ((left_cart_proj X Y) c f ,g)"
        by (typecheck_cfuncs, metis transpose_of_comp)
      also have "... = f"
        by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod)
      also have "... = f"
        by (typecheck_cfuncs, simp add: sharp_cancels_flat)
      finally show projection_property1: "((left_cart_proj X Y)Af) c f ,g = f".
      show projection_property2: "((right_cart_proj X Y)Af) c f ,g = g"
        by (typecheck_cfuncs, metis right_cart_proj_cfunc_prod sharp_cancels_flat transpose_of_comp)
      show "h2. h2 : Z  (X ×c Y)A
          f = left_cart_proj X YAf c h2 
          g = right_cart_proj X YAf c h2 
          h2 = (left_cart_proj X YAf c h2),(right_cart_proj X YAf c h2)"
      proof -
        fix h
        assume h_type[type_rule]: "h : Z  (X ×c Y)A⇖"
        assume h_property1:  "f = ((left_cart_proj X Y)Af) c h"
        assume h_property2:  "g = ((right_cart_proj X Y)Af) c h"
    
        have "f = (left_cart_proj X Y)Af c h"
          by (metis  h_property1 h_type sharp_cancels_flat)
        also have "... = ((left_cart_proj X Y) c h)"
          by (typecheck_cfuncs, simp add: transpose_of_comp)
        ultimately have computation1: "f = ((left_cart_proj X Y) c h)"
          by simp
        then have unqiueness1: "(left_cart_proj X Y) c  h =  f"
          by (typecheck_cfuncs, simp add: flat_cancels_sharp)
        have "g = ((right_cart_proj X Y)Af) c (h)"
          by (metis h_property2 h_type sharp_cancels_flat)
        have "... = ((right_cart_proj X Y) c h)"
          by (typecheck_cfuncs, metis transpose_of_comp)
        have computation2: "g = ((right_cart_proj X Y) c h)"
           by (simp add: g = right_cart_proj X YAf c h right_cart_proj X YAf c h = (right_cart_proj X Y c h))
        then have unqiueness2: "(right_cart_proj X Y) c  h =  g"
          using h_type g_type by (typecheck_cfuncs, simp add: computation2 flat_cancels_sharp)
        then have h_flat: "h = f, g"
          by (typecheck_cfuncs, simp add: cfunc_prod_unique unqiueness1 unqiueness2)
        then have h_is_sharp_prod_fflat_gflat: "h = f, g"
          by (metis  h_type sharp_cancels_flat)
        then show "h = (left_cart_proj X YAf c h),(right_cart_proj X YAf c h)"
          using h_property1 h_property2 by force
      qed
    qed
  qed
  then show "(X ×c Y)A XA×c YA⇖"
    using canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def by fastforce
qed

lemma exponential_coprod_distribution:
  "Z(X  Y) (ZX) ×c (ZY)"
proof - 
  have "is_cart_prod (Z(X  Y)) ((eval_func Z (X  Y) c (left_coproj X Y) ×f (id(Z(X  Y))) )) ((eval_func Z (X  Y) c (right_coproj X Y) ×f (id(Z(X  Y))) )) (ZX) (ZY)"
  proof (etcs_subst is_cart_prod_def2, clarify)
    fix f g H
    assume f_type[type_rule]: "f : H  ZX⇖"
    assume g_type[type_rule]: "g : H  ZY⇖"
    show "h. h : H  Z(X  Y)
           (eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c h = f 
           (eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c h = g 
           (h2. h2 : H  Z(X  Y)
                 (eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c h2 = f 
                 (eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c h2 = g 
                 h2 = h)"
    proof (intro exI[where x="(f ⨿ g c dist_prod_coprod_right X Y H)"], safe, typecheck_cfuncs)
      have "(eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c (f ⨿ g c dist_prod_coprod_right X Y H) = 
            ((eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c (id X ×f (f ⨿ g c dist_prod_coprod_right X Y H)))"
        using sharp_comp by (typecheck_cfuncs, blast)
      also have "... = (eval_func Z (X  Y) c  (left_coproj X Y ×f (f ⨿ g c dist_prod_coprod_right X Y H)))"
        by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
      also have "... = (eval_func Z (X  Y) c  (id (X  Y) ×f (f ⨿ g c dist_prod_coprod_right X Y H)) c (left_coproj X Y ×f id H))"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
      also have "... = (f ⨿ g c (dist_prod_coprod_right X Y H c left_coproj X Y ×f id H))"
        using comp_associative2 transpose_func_def by (typecheck_cfuncs, force)
      also have "... = (f ⨿ g c left_coproj (X ×c H) (Y ×c H))"
        by (simp add: dist_prod_coprod_right_left_coproj)
      also have "... = f"
        by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod sharp_cancels_flat)
      finally show "(eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c (f ⨿ g c dist_prod_coprod_right X Y H) = f".
    next
      have "(eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c (f ⨿ g c dist_prod_coprod_right X Y H) = 
            ((eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c (id Y ×f (f ⨿ g c dist_prod_coprod_right X Y H)))"
        using sharp_comp by (typecheck_cfuncs, blast)
      also have "... = (eval_func Z (X  Y) c  (right_coproj X Y ×f (f ⨿ g c dist_prod_coprod_right X Y H)))"
        by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
      also have "... = (eval_func Z (X  Y) c  (id (X  Y) ×f (f ⨿ g c dist_prod_coprod_right X Y H)) c (right_coproj X Y ×f id H))"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
      also have "... = (f ⨿ g c (dist_prod_coprod_right X Y H c right_coproj X Y ×f id H))"
        using comp_associative2 transpose_func_def by (typecheck_cfuncs, force)
      also have "... = (f ⨿ g c right_coproj (X ×c H) (Y ×c H))"
        by (simp add: dist_prod_coprod_right_right_coproj)
      also have "... = g"
        by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod sharp_cancels_flat)
      finally show "(eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c (f ⨿ g c dist_prod_coprod_right X Y H) = g".
    next
      fix h 
      assume h_type[type_rule]: "h : H  Z(X  Y)⇖"
      assume f_eqs: "f = (eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c  h"
      assume g_eqs: "g = (eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c h"
      have "(f ⨿ g c dist_prod_coprod_right X Y H) = h"
      proof(etcs_rule one_separator[where X = "(X  Y) ×c H", where Y = Z])
        show "xyh. xyh c (X  Y) ×c H  (f ⨿ g c dist_prod_coprod_right X Y H) c xyh = h c xyh"
        proof-
          fix xyh
          assume l_type[type_rule]: "xyh c (X  Y) ×c H"
          then obtain xy and z where xy_type[type_rule]: "xy c X  Y" and z_type[type_rule]: "z c H"
            and xyh_def: "xyh = xy,z"
            using cart_prod_decomp by blast
          show "(f ⨿ g c dist_prod_coprod_right X Y H) c xyh = h c xyh"
          proof(cases "x. x c X  xy =  left_coproj X Y c x")
            assume "x. x c X  xy = left_coproj X Y c x"
            then obtain x where x_type[type_rule]: "x c X" and xy_def: "xy =  left_coproj X Y c x"
              by blast
            have "(f ⨿ g c dist_prod_coprod_right X Y H) c xyh = (f ⨿ g) c (dist_prod_coprod_right X Y H  c left_coproj X Y c x,z)"
              by (typecheck_cfuncs, simp add: comp_associative2 xy_def xyh_def)
            also have "... = (f ⨿ g) c ((dist_prod_coprod_right X Y H  c (left_coproj X Y ×f id H)) c x,z)"
              using dist_prod_coprod_right_ap_left dist_prod_coprod_right_left_coproj by (typecheck_cfuncs, presburger)
            also have "... = (f ⨿ g) c (left_coproj (X ×c H) (Y ×c H)  c x,z)"
              using dist_prod_coprod_right_left_coproj by presburger
            also have "... = f c x,z"
              by (typecheck_cfuncs,  simp add: comp_associative2 left_coproj_cfunc_coprod)
            also have "... = ((eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c  h)  c x,z"
              using f_eqs by fastforce
            also have "... = (((eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y)))) c  (id X ×f h)) c x,z"
              using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
            also have "... = ((eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c  (id X ×f h)) c x,z"
              by (typecheck_cfuncs, simp add: flat_cancels_sharp)
            also have "... = (eval_func Z (X  Y) c left_coproj X Y ×f h) c x,z"
              by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
            also have "... = eval_func Z (X  Y) c  left_coproj X Y c x, h c z"
              by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2)
            also have "... = eval_func Z (X  Y) c  ((id(X  Y) ×f h) c xy,z)"
              by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 xy_def)
            also have "... = h c xyh"
              by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3 xyh_def)
            finally show ?thesis.
          next
            assume "x. x c X  xy = left_coproj X Y c x"
            then obtain y where y_type[type_rule]: "y c Y" and xy_def: "xy =  right_coproj X Y c y"
              using  coprojs_jointly_surj by (typecheck_cfuncs, blast)
            have "(f ⨿ g c dist_prod_coprod_right X Y H) c xyh = (f ⨿ g) c (dist_prod_coprod_right X Y H  c right_coproj X Y c y,z)"
              by (typecheck_cfuncs, simp add: comp_associative2 xy_def xyh_def)
            also have "... = (f ⨿ g) c ((dist_prod_coprod_right X Y H  c (right_coproj X Y ×f id H)) c y,z)"
              using dist_prod_coprod_right_ap_right dist_prod_coprod_right_right_coproj by (typecheck_cfuncs, presburger)
            also have "... = (f ⨿ g) c (right_coproj (X ×c H) (Y ×c H)  c y,z)"
              using dist_prod_coprod_right_right_coproj by presburger
            also have "... = g c y,z"
              by (typecheck_cfuncs,  simp add: comp_associative2 right_coproj_cfunc_coprod)
            also have "... = ((eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c  h)  c y,z"
              using g_eqs by fastforce
            also have "... = (((eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y)))) c  (id Y ×f h)) c y,z"
              using inv_transpose_of_composition by (typecheck_cfuncs, presburger)
            also have "... = ((eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c  (id Y ×f h)) c y,z"
              by (typecheck_cfuncs, simp add: flat_cancels_sharp)
            also have "... = (eval_func Z (X  Y) c right_coproj X Y ×f h) c y,z"
              by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_cross_prod comp_associative2 id_left_unit2 id_right_unit2)
            also have "... = eval_func Z (X  Y) c  right_coproj X Y c y, h c z"
              by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2)
            also have "... = eval_func Z (X  Y) c  ((id(X  Y) ×f h) c xy,z)"
              by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 xy_def)
            also have "... = h c xyh"
              by (typecheck_cfuncs, simp add: comp_associative2 inv_transpose_func_def3 xyh_def)
            finally show ?thesis.
          qed
        qed
      qed
      then show "h = (((eval_func Z (X  Y) c left_coproj X Y ×f idc (Z(X  Y))) c h) ⨿
                     ((eval_func Z (X  Y) c right_coproj X Y ×f idc (Z(X  Y))) c h) c
                                                                      dist_prod_coprod_right X Y H)"
        using f_eqs g_eqs h_type sharp_cancels_flat by force
    qed
  qed
  then show ?thesis
    by (metis canonical_cart_prod_is_cart_prod cart_prods_isomorphic is_isomorphic_def prod.sel(1,2))
qed

lemma empty_exp_nonempty:
  assumes "nonempty X"
  shows "X "
proof-
  obtain j where j_type[type_rule]: "j: X 𝟭×c X⇖" and j_def: "isomorphism(j)"
    using is_isomorphic_def isomorphic_is_symmetric one_x_A_iso_A by blast
  obtain y where y_type[type_rule]: "y c X"
    using assms nonempty_def by blast
  obtain e where e_type[type_rule]: "e: X×c X "
    using eval_func_type by blast
  have iso_type[type_rule]: "(e c y ×f id(X)) c j :  X "
    by typecheck_cfuncs
  show "X "
    using function_to_empty_is_iso is_isomorphic_def iso_type by blast
qed

lemma exp_pres_iso_left:
  assumes "A  X" 
  shows "AY  XY⇖"
proof - 
  obtain φ where φ_def: "φ: X  A  isomorphism(φ)"
    using assms is_isomorphic_def isomorphic_is_symmetric by blast
  obtain ψ where ψ_def: "ψ: A  X  isomorphism(ψ)  (ψ c φ = id(X))"
    using φ_def cfunc_type_def isomorphism_def by fastforce
  have idA: "φ c ψ = id(A)"
    by (metis φ_def ψ_def cfunc_type_def comp_associative id_left_unit2 isomorphism_def)
  have phi_eval_type: "(φ c eval_func X Y): XY AY⇖"
    using φ_def by (typecheck_cfuncs, blast)
  have psi_eval_type: "(ψ c eval_func A Y): AY XY⇖"
    using ψ_def by (typecheck_cfuncs, blast)

  have idXY: "(ψ c eval_func A Y) c  (φ c eval_func X Y) = id(XY)"
  proof - 
    have "(ψ c eval_func A Y) c (φ c eval_func X Y) = ψYf c φYf"
      using φ_def ψ_def exp_func_def2 by auto
    also have "... = (ψ c φ)Yf"
      by (metis φ_def ψ_def transpose_factors)
    also have "... = (id X)Yf"
      by (simp add: ψ_def)
    also have "...  = id(XY)"
      by (simp add: exponential_object_identity2)
    finally show "(ψ c eval_func A Y) c  (φ c eval_func X Y) = id(XY)".
  qed
  have idAY: "(φ c eval_func X Y) c (ψ c eval_func A Y)  = id(AY)"
  proof - 
    have "(φ c eval_func X Y) c (ψ c eval_func A Y) = φYf c ψYf"
      using φ_def ψ_def exp_func_def2 by auto
    also have "... = (φ c ψ)Yf"
      by (metis φ_def ψ_def transpose_factors)
    also have "... = (id A)Yf"
      by (simp add: idA)
    also have "...  = id(AY)"
      by (simp add: exponential_object_identity2)
    finally show "(φ c eval_func X Y) c (ψ c eval_func A Y)  = id(AY)".
  qed
  show  "AY  XY⇖"
    by (metis cfunc_type_def comp_epi_imp_epi comp_monic_imp_monic epi_mon_is_iso idAY idXY id_isomorphism is_isomorphic_def iso_imp_epi_and_monic phi_eval_type psi_eval_type)
qed

lemma expset_power_tower:
  "(AB)C A(B×c C)⇖"
proof - 
  obtain φ where φ_def: "φ = ((eval_func A (B×c C)) c (associate_left B C (A(B×c C))))" and
                 φ_type[type_rule]: "φ: B ×c (C×c (A(B×c C)))  A" and 
                 φdbsharp_type[type_rule]: "(φ) : (A(B×c C))  ((AB)C)"
    using transpose_func_type by (typecheck_cfuncs, fastforce)

  obtain ψ where ψ_def: "ψ = (eval_func A B) c (id(B)×f eval_func (AB) C) c (associate_right B C ((AB)C))" and
                 ψ_type[type_rule]: "ψ :  (B ×c C) ×c ((AB)C)  A" and
                 ψsharp_type[type_rule]: "ψ: (AB)C (A(B×c C))"
    using transpose_func_type by (typecheck_cfuncs, blast)

  have "φ c ψ = id((AB)C)"
  proof(etcs_rule same_evals_equal[where X = "(AB)", where A = "C"])
    show "eval_func (AB) C c idc C ×f φ c ψ =
          eval_func (AB) C c idc C ×f idc (AB⇖⇗C)"
    proof(etcs_rule same_evals_equal[where X = "A", where A = "B"])
      show "eval_func A B c idc B ×f (eval_func (AB) C c (idc C ×f φ c ψ)) =
            eval_func A B c idc B ×f eval_func (AB) C c idc C ×f idc (AB⇖⇗C)"
      proof - 
        have "eval_func A B c idc B ×f (eval_func (AB) C c (idc C ×f φ c ψ)) =
              eval_func A B c idc B ×f (eval_func (AB) C c (idc C ×f φ) c (idc C ×f ψ))"
          by (typecheck_cfuncs, metis identity_distributes_across_composition)
        also have "... = eval_func A B c idc B ×f ((eval_func (AB) C c (idc C ×f φ)) c (idc C ×f ψ))"
          by (typecheck_cfuncs, simp add: comp_associative2)
        also have "... = eval_func A B c idc B ×f (φ c (idc C ×f ψ))"
          by (typecheck_cfuncs, simp add: transpose_func_def)        
        also have "... = eval_func A B c ((idc B ×f φ)  c (idc B ×f (idc C ×f ψ)))"
          using identity_distributes_across_composition by (typecheck_cfuncs, auto)
        also have "... = (eval_func A B c ((idc B ×f φ)))  c (idc B ×f (idc C ×f ψ))"
          using comp_associative2 by (typecheck_cfuncs,blast)
        also have "... = φ  c (idc B ×f (idc C ×f ψ))"
          by (typecheck_cfuncs, simp add: transpose_func_def)
        also have "... = ((eval_func A (B×c C)) c (associate_left B C (A(B×c C)))) c (idc B ×f (idc C ×f ψ))"
          by (simp add: φ_def)
        also have "... = (eval_func A (B×c C)) c (associate_left B C (A(B×c C))) c (idc B ×f (idc C ×f ψ))"
          using comp_associative2 by (typecheck_cfuncs, auto)
        also have "... = (eval_func A (B×c C)) c ((idc B ×f idc C) ×f ψ) c associate_left B C ((AB)C)"
          by (typecheck_cfuncs, simp add: associate_left_crossprod_ap)
        also have "... = (eval_func A (B×c C)) c ((idc (B ×c C)) ×f ψ) c associate_left B C ((AB)C)"
          by (simp add: id_cross_prod)
        also have "... = ψ c associate_left B C ((AB)C)"
          by (typecheck_cfuncs, simp add: comp_associative2 transpose_func_def)
        also have "... = ((eval_func A B) c (id(B)×f eval_func (AB) C)) c ((associate_right B C ((AB)C))c  associate_left B C ((AB)C))"
          by (typecheck_cfuncs, simp add: ψ_def cfunc_type_def comp_associative)
        also have "... = ((eval_func A B) c (id(B)×f eval_func (AB) C)) c id(B ×c (C ×c ((AB)C)))"
          by (simp add: right_left)
        also have "... = (eval_func A B) c (id(B)×f eval_func (AB) C)"
          by (typecheck_cfuncs, meson id_right_unit2)
        also have "... = eval_func A B c idc B ×f eval_func (AB) C c idc C ×f idc (AB⇖⇗C)"
          by (typecheck_cfuncs, simp add: id_cross_prod id_right_unit2)
        finally show ?thesis.
      qed
    qed
  qed
  have "ψ c φ = id(A(B ×c C))"
  proof(etcs_rule same_evals_equal[where X = "A", where A = "(B ×c C)"])
    show "eval_func A (B ×c C) c (idc (B ×c C) ×f (ψ c φ)) = 
          eval_func A (B ×c C) c idc (B ×c C) ×f idc (A(B ×c C))"
    proof -
      have "eval_func A (B ×c C) c (idc (B ×c C) ×f (ψ c φ)) =
            eval_func A (B ×c C) c ((idc (B ×c C) ×f (ψ)) c (idc (B ×c C) ×f φ))"
        by (typecheck_cfuncs, simp add: identity_distributes_across_composition)
      also have "... = ( eval_func A (B ×c C) c (idc (B ×c C) ×f (ψ))) c (idc (B ×c C) ×f φ)"
        using comp_associative2 by (typecheck_cfuncs, blast)
      also have "... = ψ c (idc (B ×c C) ×f φ)"
        by (typecheck_cfuncs, simp add: transpose_func_def)
      also have "... =(eval_func A B) c (id(B)×f eval_func (AB) C) c (associate_right B C ((AB)C)) c (idc (B ×c C) ×f φ)"
        by (typecheck_cfuncs, smt ψ_def cfunc_type_def comp_associative domain_comp)
      also have "... =(eval_func A B) c (id(B)×f eval_func (AB) C) c (associate_right B C ((AB)C)) c ((idc (B) ×f id( C)) ×f φ)"
        by (typecheck_cfuncs, simp add: id_cross_prod)
      also have "... =(eval_func A B) c ((id(B)×f eval_func (AB) C) c ((idc (B) ×f (id(C) ×f φ)) c (associate_right B C (A(B ×c C)))))"
        using associate_right_crossprod_ap by (typecheck_cfuncs, auto)
      also have "... =(eval_func A B) c ((id(B)×f eval_func (AB) C) c (idc (B) ×f (id(C) ×f φ))) c (associate_right B C (A(B ×c C)))"
        by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... =(eval_func A B) c (id(B)×f ((eval_func (AB) C)c (id(C) ×f φ))) c (associate_right B C (A(B ×c C)))"
        using identity_distributes_across_composition by (typecheck_cfuncs, auto)
      also have "... =(eval_func A B) c (id(B)×f φ) c (associate_right B C (A(B ×c C)))"
        by (typecheck_cfuncs, simp add: transpose_func_def)
      also have "... =((eval_func A B) c (id(B)×f φ)) c (associate_right B C (A(B ×c C)))"
        using comp_associative2 by (typecheck_cfuncs, blast)
      also have "... = φ c (associate_right B C (A(B ×c C)))"
        by (typecheck_cfuncs, simp add: transpose_func_def)
      also have "... = (eval_func A (B×c C)) c ((associate_left B C (A(B×c C))) c (associate_right B C (A(B ×c C))))"
        by (typecheck_cfuncs, simp add: φ_def comp_associative2)  
      also have "... = eval_func A (B×c C) c id ((B ×c C) ×c (A(B×c C)))"
        by (typecheck_cfuncs, simp add: left_right)
      also have "... = eval_func A (B ×c C) c idc (B ×c C) ×f idc (A(B ×c C))"
        by (typecheck_cfuncs, simp add: id_cross_prod)
      finally show ?thesis.
    qed
  qed
  show ?thesis
    by (metis φ c ψ = idc (AB⇖⇗C) ψ c φ = idc (A(B ×c C)) φdbsharp_type ψsharp_type cfunc_type_def is_isomorphic_def isomorphism_def)
qed

lemma exp_pres_iso_right:
  assumes "A  X" 
  shows "YA  YX⇖"
proof - 
  obtain φ where φ_def: "φ: X  A  isomorphism(φ)"
    using assms is_isomorphic_def isomorphic_is_symmetric by blast
  obtain ψ where ψ_def: "ψ: A  X  isomorphism(ψ)  (ψ c φ = id(X))"
    using φ_def cfunc_type_def isomorphism_def by fastforce
  have idA: "φ c ψ = id(A)"
    by (metis φ_def ψ_def cfunc_type_def comp_associative id_left_unit2 isomorphism_def)
  obtain f where f_def: "f = (eval_func Y X) c (ψ ×f id(YX))" and f_type[type_rule]: "f: A×c (YX)  Y" and fsharp_type[type_rule]: "f : YX YA⇖"
    using ψ_def transpose_func_type by (typecheck_cfuncs, presburger)
  obtain g where g_def: "g = (eval_func Y A) c (φ ×f id(YA))" and  g_type[type_rule]: "g: X×c (YA)  Y" and gsharp_type[type_rule]: "g : YA YX⇖"
    using φ_def transpose_func_type by (typecheck_cfuncs, presburger)

  have fsharp_gsharp_id: "f c g = id(YA)"
  proof(etcs_rule same_evals_equal[where X = Y, where A = A])
    have "eval_func Y A c idc A ×f f c g = eval_func Y A c (idc A ×f f) c (idc A ×f g)"
      using fsharp_type gsharp_type identity_distributes_across_composition by auto
    also have "... = eval_func Y X c (ψ ×f id(YX)) c (idc A ×f g)"
      using ψ_def cfunc_type_def comp_associative f_def f_type gsharp_type transpose_func_def by (typecheck_cfuncs, smt)
    also have "... = eval_func Y X c (ψ ×f g)"
      by (smt ψ_def cfunc_cross_prod_comp_cfunc_cross_prod gsharp_type id_left_unit2 id_right_unit2 id_type)
    also have "... = eval_func Y X c (id X ×f g) c (ψ ×f id(YA))"
      by (smt ψ_def cfunc_cross_prod_comp_cfunc_cross_prod gsharp_type id_left_unit2 id_right_unit2 id_type)
    also have "... = eval_func Y A c (φ ×f id(YA)) c (ψ ×f id(YA))"
      by (typecheck_cfuncs, smt φ_def ψ_def comp_associative2 flat_cancels_sharp g_def g_type inv_transpose_func_def3)
    also have "... = eval_func Y A c ((φ c ψ) ×f (id(YA) c id(YA)))"
      using φ_def ψ_def cfunc_cross_prod_comp_cfunc_cross_prod by (typecheck_cfuncs, auto)
    also have "... = eval_func Y A c id(A) ×f id(YA)"
      using idA id_right_unit2 by (typecheck_cfuncs, auto)
    finally show "eval_func Y A c idc A ×f f c g = eval_func Y A c idc A ×f idc (YA)".
  qed

  have gsharp_fsharp_id: "g c f = id(YX)"
  proof(etcs_rule same_evals_equal[where X = Y, where A = X])
    have "eval_func Y X c idc X ×f g c f = eval_func Y X c (idc X ×f g) c (idc X ×f f)"
      using fsharp_type gsharp_type identity_distributes_across_composition by auto
    also have "... = eval_func Y A c (φ ×f idc (YA)) c (idc X ×f f)"
      using φ_def cfunc_type_def comp_associative fsharp_type g_def g_type transpose_func_def by (typecheck_cfuncs, smt)
    also have "... = eval_func Y A c (φ ×f f)"
      by (smt φ_def cfunc_cross_prod_comp_cfunc_cross_prod fsharp_type id_left_unit2 id_right_unit2 id_type)
    also have "... = eval_func Y A c (id(A) ×f f) c (φ ×f idc (YX))"
      by (smt φ_def cfunc_cross_prod_comp_cfunc_cross_prod fsharp_type id_left_unit2 id_right_unit2 id_type)
    also have "... = eval_func Y X c (ψ ×f idc (YX)) c (φ ×f idc (YX))"
      by (typecheck_cfuncs, smt φ_def ψ_def comp_associative2 f_def f_type flat_cancels_sharp inv_transpose_func_def3)
    also have "... = eval_func Y X c ((ψ c φ) ×f (id(YX) c id(YX)))"
      using φ_def ψ_def cfunc_cross_prod_comp_cfunc_cross_prod by (typecheck_cfuncs, auto)
    also have "... = eval_func Y X c id(X) ×f id(YX)"
      using ψ_def id_left_unit2 by (typecheck_cfuncs, auto)
    finally show "eval_func Y X c idc X ×f g c f = eval_func Y X c idc X ×f idc (YX)".
  qed
  show ?thesis
    by (metis cfunc_type_def comp_epi_imp_epi comp_monic_imp_monic epi_mon_is_iso fsharp_gsharp_id fsharp_type gsharp_fsharp_id gsharp_type id_isomorphism is_isomorphic_def iso_imp_epi_and_monic)
qed

lemma exp_pres_iso:
  assumes "A  X" "B  Y" 
  shows "AB  XY⇖"
  by (meson assms exp_pres_iso_left exp_pres_iso_right isomorphic_is_transitive)

lemma empty_to_nonempty:
  assumes "nonempty X" "is_empty Y" 
  shows "YX "
  by (meson assms exp_pres_iso_left isomorphic_is_transitive no_el_iff_iso_empty empty_exp_nonempty)

lemma exp_is_empty:
  assumes "is_empty X" 
  shows "YX 𝟭"
  using assms exp_pres_iso_right isomorphic_is_transitive no_el_iff_iso_empty exp_empty by blast

lemma nonempty_to_nonempty:
  assumes "nonempty X" "nonempty Y"
  shows "nonempty(YX)"
  by (meson assms(2) comp_type nonempty_def terminal_func_type transpose_func_type)

lemma empty_to_nonempty_converse:
  assumes "YX "
  shows "is_empty Y  nonempty X"
  by (metis is_empty_def exp_is_empty assms no_el_iff_iso_empty nonempty_def nonempty_to_nonempty single_elem_iso_one)

text ‹The definition below corresponds to Definition 2.5.11 in Halvorson.›
definition powerset :: "cset  cset" ("𝒫_" [101]100) where
  "𝒫 X = ΩX⇖"

lemma sets_squared:
  "AΩ A ×c A"
proof - 
  obtain φ where φ_def: "φ = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ),
                              eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ)" and
                 φ_type[type_rule]: "φ : AΩ A ×c A"
                  by (typecheck_cfuncs, simp)
  have "injective φ"
    unfolding injective_def
  proof(clarify)
    fix f g 
    assume "f c domain φ" then have f_type[type_rule]: "f c AΩ⇖" 
      using φ_type cfunc_type_def by (typecheck_cfuncs, auto)
    assume "g c domain φ" then have g_type[type_rule]: "g c AΩ⇖" 
      using φ_type cfunc_type_def by (typecheck_cfuncs, auto)
    assume eqs: "φ c f = φ c g"
    show "f = g"
    proof(etcs_rule one_separator)
      show "id_1. id_1 c 𝟭  f c id_1 = g c id_1"
      proof(etcs_rule same_evals_equal[where X = A, where A = Ω])
        fix id_1
        assume id1_is: "id_1 c 𝟭"
        then have id1_eq: "id_1 = id(𝟭)"
          using id_type one_unique_element by auto

        obtain a1 a2 where phi_f_def: "φ c f = a1,a2  a1 c A  a2 c A"
          using φ_type cart_prod_decomp comp_type f_type by blast
        have equation1: "a1,a2 =  eval_func A Ω c 𝗍, f,
                            eval_func A Ω c 𝖿, f"
        proof - 
          have "a1,a2 = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ),
                              eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ) c f"
            using φ_def phi_f_def by auto
          also have "... = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ) c f,
                              eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ) c f"
            by (typecheck_cfuncs,smt cfunc_prod_comp comp_associative2)
          also have "... = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙ c f, id(AΩ) c f,
                              eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙ c f, id(AΩ)c f"
            by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
          also have "... = eval_func A Ω c 𝗍, f,
                              eval_func A Ω c 𝖿, f"    
            by (typecheck_cfuncs, metis id1_eq id1_is id_left_unit2 id_right_unit2 terminal_func_unique)
          finally show ?thesis.
        qed
        have equation2: "a1,a2 =  eval_func A Ω c 𝗍, g,
                                    eval_func A Ω c 𝖿, g"
        proof - 
          have "a1,a2 = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ),
                          eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ) c g"
            using φ_def eqs phi_f_def by auto
          also have "... = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ) c g ,
                            eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ) c g"
            by (typecheck_cfuncs,smt cfunc_prod_comp comp_associative2)
          also have "... = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙ c g, id(AΩ) c g,
                            eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙ c g, id(AΩ)c g "
            by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
          also have "... = eval_func A Ω c 𝗍, g,
                            eval_func A Ω c 𝖿, g"    
            by (typecheck_cfuncs, metis id1_eq id1_is id_left_unit2 id_right_unit2 terminal_func_unique)
          finally show ?thesis.
        qed
        have "eval_func A Ω c 𝗍, f, eval_func A Ω c 𝖿, f = 
              eval_func A Ω c 𝗍, g, eval_func A Ω c 𝖿, g"
          using equation1 equation2 by auto
        then have equation3: "(eval_func A Ω c 𝗍, f = eval_func A Ω c 𝗍, g)  
                              (eval_func A Ω c 𝖿, f = eval_func A Ω c 𝖿, g)"
          using  cart_prod_eq2 by (typecheck_cfuncs, auto)
        have "eval_func A Ω c idc Ω ×f f  = eval_func A Ω c idc Ω ×f g"
        proof(etcs_rule one_separator)
          fix x
          assume x_type[type_rule]: "x c Ω ×c 𝟭"
          then obtain w i where  x_def: "(w c Ω)  (i c 𝟭)  (x = w,i)"
            using cart_prod_decomp by blast
          then have i_def: "i = id(𝟭)"
            using id1_eq id1_is one_unique_element by auto
          have w_def: "(w = 𝖿)  (w = 𝗍)"
            by (simp add: true_false_only_truth_values x_def)
          then have x_def2: "(x = 𝖿,i)  (x = 𝗍,i)"
            using x_def by auto
          show "(eval_func A Ω c idc Ω ×f f) c x = (eval_func A Ω c idc Ω ×f g) c x"
          proof(cases "(x = 𝖿,i)", clarify)
            assume case1: "x = 𝖿,i"
            have "(eval_func A Ω c (idc Ω ×f f)) c 𝖿,i = eval_func A Ω c ((idc Ω ×f f) c 𝖿,i)"
              using case1 comp_associative2 x_type by (typecheck_cfuncs, auto)
            also have "... = eval_func A Ω c idc Ω c  𝖿,f c i"
              using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
            also have "... = eval_func A Ω c 𝖿, f "
              using f_type false_func_type i_def id_left_unit2 id_right_unit2 by auto
            also have "... = eval_func A Ω c 𝖿, g"
              using equation3 by blast
            also have "... = eval_func A Ω c idc Ω c  𝖿,g c i"
              by (typecheck_cfuncs, simp add: i_def id_left_unit2 id_right_unit2)
            also have "... = eval_func A Ω c ((idc Ω ×f g) c 𝖿,i)"
              using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
            also have "... = (eval_func A Ω c (idc Ω ×f g)) c 𝖿,i"
              using case1 comp_associative2 x_type by (typecheck_cfuncs, auto)
            finally show "(eval_func A Ω c idc Ω ×f f) c 𝖿,i = (eval_func A Ω c idc Ω ×f g) c 𝖿,i".
          next
            assume case2: "x  𝖿,i"
            then have x_eq: "x = 𝗍,i"
              using x_def2 by blast
            have "(eval_func A Ω c (idc Ω ×f f)) c 𝗍,i = eval_func A Ω c ((idc Ω ×f f) c 𝗍,i)"
                using case2 x_eq comp_associative2 x_type by (typecheck_cfuncs, auto)
            also have "... = eval_func A Ω c idc Ω c  𝗍,f c i"
                using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
            also have "... = eval_func A Ω c 𝗍, f "
              using f_type i_def id_left_unit2 id_right_unit2 true_func_type by auto
            also have "... = eval_func A Ω c 𝗍, g"
              using equation3 by blast
            also have "... = eval_func A Ω c idc Ω c  𝗍,g c i"
                by (typecheck_cfuncs, simp add: i_def id_left_unit2 id_right_unit2)
            also have "... = eval_func A Ω c ((idc Ω ×f g) c 𝗍,i)"
                using cfunc_cross_prod_comp_cfunc_prod i_def id1_eq id1_is by (typecheck_cfuncs, auto)
            also have "... = (eval_func A Ω c (idc Ω ×f g)) c 𝗍,i"
              using comp_associative2 x_eq x_type by (typecheck_cfuncs, blast)
            ultimately show "(eval_func A Ω c idc Ω ×f f) c x = (eval_func A Ω c idc Ω ×f g) c x"
              by (simp add: x_eq)
          qed
        qed
        then show "eval_func A Ω c idc Ω ×f f c id_1 = eval_func A Ω c idc Ω ×f g c id_1"
          using  f_type g_type same_evals_equal by blast
        qed
      qed
    qed
    then have "monomorphism(φ)"
      using injective_imp_monomorphism by auto
    have "surjective(φ)"
      unfolding surjective_def
    proof(clarify)
      fix y 
      assume "y c codomain φ" then have y_type[type_rule]: "y c A ×c A"
        using φ_type cfunc_type_def by auto
      then obtain a1 a2 where y_def[type_rule]: "y = a1,a2  a1 c A  a2 c A"
        using cart_prod_decomp by blast
      then have aua: "(a1 ⨿ a2): 𝟭  𝟭  A"
        by (typecheck_cfuncs, simp add: y_def)     
    
      obtain f where f_def: "f = ((a1 ⨿ a2) c case_bool  c left_cart_proj Ω 𝟭)" and
                     f_type[type_rule]: "f c AΩ⇖"
        by (meson aua case_bool_type comp_type left_cart_proj_type transpose_func_type)
     have a1_is: "(eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ)) c f = a1"
     proof-
       have "(eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ)) c f = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙, id(AΩ) c f"
         by (typecheck_cfuncs, simp add: comp_associative2)
       also have "... = eval_func A Ω c 𝗍 c β⇘AΩ⇖⇙ c f, id(AΩ) c f"
         by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
       also have "... = eval_func A Ω c 𝗍, f"
         by (metis cfunc_type_def f_type id_left_unit id_right_unit id_type one_unique_element terminal_func_comp terminal_func_type true_func_type)
       also have "... = eval_func A Ω c id(Ω) c 𝗍, f c id(𝟭)"
         by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
       also have "... = eval_func A Ω c (id(Ω) ×f f) c 𝗍, id(𝟭)"
         by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
       also have "... = (eval_func A Ω c (id(Ω) ×f f)) c 𝗍, id(𝟭)"
         using comp_associative2 by (typecheck_cfuncs, blast)
       also have "... = ((a1 ⨿ a2) c case_bool  c left_cart_proj Ω 𝟭) c 𝗍, id(𝟭)"
         by (typecheck_cfuncs, metis  aua f_def flat_cancels_sharp inv_transpose_func_def3)
       also have "... = (a1 ⨿ a2) c case_bool  c 𝗍"
         by (typecheck_cfuncs, smt case_bool_type aua comp_associative2 left_cart_proj_cfunc_prod)
       also have "... = (a1 ⨿ a2) c left_coproj 𝟭 𝟭"
         by (simp add: case_bool_true)
       also have "... = a1"
         using left_coproj_cfunc_coprod y_def by blast
       finally show ?thesis.
     qed
     have a2_is: "(eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ)) c f = a2"
     proof-
       have "(eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ)) c f = eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙, id(AΩ) c f"
         by (typecheck_cfuncs, simp add: comp_associative2)
       also have "... = eval_func A Ω c 𝖿 c β⇘AΩ⇖⇙ c f, id(AΩ) c f"
         by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
       also have "... = eval_func A Ω c 𝖿, f"
         by (metis cfunc_type_def f_type id_left_unit id_right_unit id_type one_unique_element terminal_func_comp terminal_func_type false_func_type)
       also have "... = eval_func A Ω c id(Ω) c 𝖿, f c id(𝟭)"
         by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
       also have "... = eval_func A Ω c (id(Ω) ×f f) c 𝖿, id(𝟭)"
         by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
       also have "... = (eval_func A Ω c (id(Ω) ×f f)) c 𝖿, id(𝟭)"
         using comp_associative2 by (typecheck_cfuncs, blast)
       also have "... = ((a1 ⨿ a2) c case_bool  c left_cart_proj Ω 𝟭) c 𝖿, id(𝟭)"
         by (typecheck_cfuncs, metis  aua f_def flat_cancels_sharp inv_transpose_func_def3)
       also have "... = (a1 ⨿ a2) c case_bool  c 𝖿"
         by (typecheck_cfuncs, smt aua comp_associative2 left_cart_proj_cfunc_prod)
       also have "... = (a1 ⨿ a2) c right_coproj 𝟭 𝟭"
         by (simp add: case_bool_false)
       also have "... = a2"
         using right_coproj_cfunc_coprod y_def by blast
       finally show ?thesis.
     qed
     have "φ c f  = a1,a2"
       unfolding φ_def by (typecheck_cfuncs, simp add: a1_is a2_is cfunc_prod_comp)
     then show "x. x c domain φ  φ c x = y"
       using φ_type cfunc_type_def f_type y_def by auto
   qed
   then have "epimorphism(φ)"
     by (simp add: surjective_is_epimorphism)
   then have "isomorphism(φ)"
     by (simp add: monomorphism φ epi_mon_is_iso)
   then show ?thesis
     using φ_type is_isomorphic_def by blast
qed

end