Theory Terminal

section ‹Terminal Objects and Elements›

theory Terminal
  imports Cfunc Product
begin

text ‹The axiomatization below corresponds to Axiom 3 (Terminal Object) in Halvorson.›
axiomatization
  terminal_func :: "cset  cfunc" ("β⇘_" 100) and
  one_set :: "cset" ("𝟭")
where
  terminal_func_type[type_rule]: "β⇘X: X  𝟭" and
  terminal_func_unique: "h :  X  𝟭  h = β⇘X⇙" and
  one_separator: "f : X  Y  g : X  Y  ( x. x : 𝟭  X  f c x = g c x)  f = g"

lemma one_separator_contrapos:
  assumes "f : X  Y" "g : X  Y"
  shows "f  g   x. x : 𝟭  X  f c x  g c x"
  using assms one_separator by (typecheck_cfuncs, blast)

lemma terminal_func_comp:
  "x : X  Y  β⇘Yc x = β⇘X⇙"
  by (simp add: comp_type terminal_func_type terminal_func_unique)

lemma terminal_func_comp_elem:
  "x : 𝟭  X  β⇘Xc x = id 𝟭"
  by (metis id_type terminal_func_comp terminal_func_unique)

subsection ‹Set Membership and Emptiness›

text ‹The abbreviation below captures Definition 2.1.16 in Halvorson.›
abbreviation member :: "cfunc  cset  bool" (infix "c" 50) where
  "x c X  (x : 𝟭  X)"

definition nonempty :: "cset  bool" where
  "nonempty X  (x. x c X)"

definition is_empty :: "cset  bool" where
  "is_empty X  ¬(x. x c X)"

text ‹The lemma below corresponds to Exercise 2.1.18 in Halvorson.›
lemma element_monomorphism:
  "x c X  monomorphism x"
  unfolding monomorphism_def
  by (metis cfunc_type_def domain_comp terminal_func_unique)

lemma one_unique_element:
  "∃! x. x c 𝟭"
  using terminal_func_type terminal_func_unique by blast

lemma prod_with_empty_is_empty1:
  assumes "is_empty (A)"
  shows "is_empty(A ×c B)"
  by (meson assms comp_type left_cart_proj_type is_empty_def)

lemma prod_with_empty_is_empty2:
  assumes "is_empty (B)"
  shows "is_empty (A ×c B)"
  using assms cart_prod_decomp is_empty_def by blast

subsection ‹Terminal Objects (sets with one element)›

definition terminal_object :: "cset  bool" where
  "terminal_object X  ( Y. ∃! f. f : Y  X)"

lemma one_terminal_object: "terminal_object(𝟭)"
  unfolding terminal_object_def using terminal_func_type terminal_func_unique by blast

text ‹The lemma below is a generalisation of @{thm element_monomorphism}
lemma terminal_el_monomorphism:
  assumes "x : T  X"
  assumes "terminal_object T"
  shows "monomorphism x"
  unfolding monomorphism_def
  by (metis assms cfunc_type_def domain_comp terminal_object_def)

text ‹The lemma below corresponds to Exercise 2.1.15 in Halvorson.›
lemma terminal_objects_isomorphic:
  assumes "terminal_object X" "terminal_object Y"
  shows "X  Y"
  unfolding is_isomorphic_def
proof -
  obtain f where f_type: "f : X  Y" and f_unique: "g. g : X  Y  f = g"
    using assms(2) terminal_object_def by force

  obtain g where g_type: "g : Y  X" and g_unique: "f. f : Y  X  g = f"
    using assms(1) terminal_object_def by force

  have g_f_is_id: "g c f = id X"
    using assms(1) comp_type f_type g_type id_type terminal_object_def by blast

  have f_g_is_id: "f c g = id Y"
    using assms(2) comp_type f_type g_type id_type terminal_object_def by blast

  have f_isomorphism: "isomorphism f"
    unfolding isomorphism_def
    using cfunc_type_def f_type g_type g_f_is_id f_g_is_id
    by (intro exI[where x=g], auto)

  show "f. f : X  Y  isomorphism f"
    using f_isomorphism f_type by auto
qed

text ‹The two lemmas below show the converse to Exercise 2.1.15 in Halvorson.›
lemma iso_to1_is_term:
  assumes "X  𝟭"
  shows "terminal_object X"
  unfolding terminal_object_def
proof 
  fix Y
  obtain x where x_type[type_rule]: "x : 𝟭  X" and x_unique: " y. y : 𝟭  X  x = y"
    by (smt assms is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric monomorphism_def2 terminal_func_comp terminal_func_unique)
  show  "∃!f. f : Y  X"
  proof (rule ex1I[where a="x c β⇘Y⇙"], typecheck_cfuncs)
    fix xa
    assume xa_type: "xa : Y  X"
    show "xa = x c β⇘Y⇙"
    proof (rule ccontr)
      assume "xa  x c β⇘Y⇙"
      then obtain y where elems_neq: "xa c y  (x c β⇘Y) c y" and y_type: "y : 𝟭  Y"
        using one_separator_contrapos comp_type terminal_func_type x_type xa_type by blast
      then show False
        by (smt (z3) comp_type elems_neq terminal_func_type x_unique xa_type y_type)     
    qed
  qed
qed

lemma iso_to_term_is_term:
  assumes "X  Y"
  assumes "terminal_object Y"
  shows "terminal_object X"
  by (meson assms iso_to1_is_term isomorphic_is_transitive one_terminal_object terminal_objects_isomorphic)

text ‹The lemma below corresponds to Proposition 2.1.19 in Halvorson.›
lemma single_elem_iso_one:
  "(∃! x. x c X)  X  𝟭"
proof
  assume X_iso_one: "X  𝟭"
  then have "𝟭  X"
    by (simp add: isomorphic_is_symmetric)
  then obtain f where f_type: "f : 𝟭  X" and f_iso: "isomorphism f"
    using is_isomorphic_def by blast
  show "∃!x. x c X"
  proof(safe)
    show "x. x c X"
      by (meson f_type)
  next  
    fix x y
    assume x_type[type_rule]: "x c X"
    assume y_type[type_rule]: "y c X"
    have βx_eq_βy: "β⇘Xc x = β⇘Xc y"
      using one_unique_element by (typecheck_cfuncs, blast)      
    have "isomorphism (β⇘X)"
      using X_iso_one is_isomorphic_def terminal_func_unique by blast
    then have "monomorphism (β⇘X)"
      by (simp add: iso_imp_epi_and_monic)
    then show "x= y"
      using βx_eq_βy  monomorphism_def2 terminal_func_type by (typecheck_cfuncs, blast)      
  qed
next
  assume "∃!x. x c X"
  then obtain x where x_type: "x : 𝟭  X" and x_unique: " y. y : 𝟭  X  x = y"
    by blast
  have "terminal_object X"
    unfolding terminal_object_def  
  proof 
    fix Y
    show "∃!f. f : Y  X"
    proof (rule ex1I [where a="x c β⇘Y⇙"])
      show "x c β⇘Y: Y  X"
        using comp_type terminal_func_type x_type by blast
    next
      fix xa
      assume xa_type: "xa : Y  X"
      show "xa = x c β⇘Y⇙"
      proof (rule ccontr)
        assume "xa  x c β⇘Y⇙"
        then obtain y where elems_neq: "xa c y  (x c β⇘Y) c y" and y_type: "y : 𝟭  Y"
          using one_separator_contrapos[where f=xa, where g="x c β⇘Y⇙", where X=Y, where Y=X]
          using comp_type terminal_func_type x_type xa_type by blast
        have elem1: "xa c y c X"
          using comp_type xa_type y_type by auto
        have elem2: "(x c β⇘Y) c y c X"
          using comp_type terminal_func_type x_type y_type by blast
        show False
          using elem1 elem2 elems_neq x_unique by blast
      qed
    qed
  qed
  then show "X  𝟭"
    by (simp add: one_terminal_object terminal_objects_isomorphic)
qed

subsection ‹Injectivity›

text ‹The definition below corresponds to Definition 2.1.24 in Halvorson.›
definition injective :: "cfunc  bool" where
 "injective f   ( x y. (x c domain f  y c domain f  f c x = f c y)  x = y)"

lemma injective_def2:
  assumes "f : X  Y"
  shows "injective f   ( x y. (x c X  y c X  f c x = f c y)  x = y)"
  using assms cfunc_type_def injective_def by force

text ‹The lemma below corresponds to Exercise 2.1.26 in Halvorson.›
lemma monomorphism_imp_injective:
  "monomorphism f  injective f"
  by (simp add: cfunc_type_def injective_def monomorphism_def)

text ‹The lemma below corresponds to Proposition 2.1.27 in Halvorson.›
lemma injective_imp_monomorphism:
  "injective f  monomorphism f"
  unfolding monomorphism_def injective_def
proof clarify
  fix g h
  assume f_inj: "x y. x c domain f  y c domain f  f c x = f c y  x = y"
  assume cd_g_eq_d_f: "codomain g = domain f"
  assume cd_h_eq_d_f: "codomain h = domain f"
  assume fg_eq_fh: "f c g = f c h"

  obtain X Y where f_type: "f : X  Y"
    using cfunc_type_def by auto    
  obtain A where g_type: "g : A  X" and h_type: "h : A  X"
    by (metis cd_g_eq_d_f cd_h_eq_d_f cfunc_type_def domain_comp f_type fg_eq_fh)

  have "x. x c A  g c x = h c x"
  proof clarify
    fix x
    assume x_in_A: "x c A"

    have "f c g c x = f c h c x"
      using g_type h_type x_in_A f_type comp_associative2 fg_eq_fh by (typecheck_cfuncs, auto)
    then show "g c x = h c x"
      using cd_h_eq_d_f cfunc_type_def comp_type f_inj g_type h_type x_in_A by presburger
  qed
  then show "g = h"
    using g_type h_type one_separator by auto
qed

lemma cfunc_cross_prod_inj:
  assumes type_assms: "f : X  Y" "g : Z  W"
  assumes "injective f  injective g"
  shows "injective (f ×f g)"
  by (typecheck_cfuncs, metis assms cfunc_cross_prod_mono injective_imp_monomorphism monomorphism_imp_injective)

lemma cfunc_cross_prod_mono_converse:
  assumes type_assms: "f : X  Y" "g : Z  W"
  assumes fg_inject: "injective (f ×f g)"
  assumes nonempty: "nonempty X" "nonempty Z"
  shows "injective f  injective g"
  unfolding injective_def
proof safe
  fix x y 
  assume x_type: "x c domain f"
  assume y_type: "y c domain f"
  assume equals: "f c x = f c y"
  have fg_type: "f ×f g : X ×c Z  Y ×c W"
    using assms by typecheck_cfuncs
  have x_type2: "x c X"
    using cfunc_type_def type_assms(1) x_type by auto
  have y_type2: "y c X"
    using cfunc_type_def type_assms(1) y_type by auto
  show "x = y"
  proof - 
    obtain b where b_def: "b c Z"
      using nonempty(2) nonempty_def by blast

    have xb_type: "x,b c X ×c Z"
      by (simp add: b_def cfunc_prod_type x_type2)
    have yb_type: "y,b c X ×c Z"
      by (simp add: b_def cfunc_prod_type y_type2)
    have "(f ×f g) c x,b = f c x,g c b"
      using b_def cfunc_cross_prod_comp_cfunc_prod type_assms x_type2 by blast
    also have "... = f c y,g c b"
      by (simp add: equals)
    also have "... = (f ×f g) c y,b"
      using b_def cfunc_cross_prod_comp_cfunc_prod type_assms y_type2 by auto
    finally have "x,b = y,b"
      by (metis cfunc_type_def fg_inject fg_type injective_def xb_type yb_type)
    then show "x = y"
      using b_def cart_prod_eq2 x_type2 y_type2 by auto
  qed
next
  fix x y 
  assume x_type: "x c domain g"
  assume y_type: "y c domain g"
  assume equals: "g c x = g c y"
  have fg_type: "f ×f g : X ×c Z  Y ×c W"
    using assms by typecheck_cfuncs
  have x_type2: "x c Z"
    using cfunc_type_def type_assms(2) x_type by auto
  have y_type2: "y c Z"
    using cfunc_type_def type_assms(2) y_type by auto
  show "x = y"
  proof - 
    obtain b where b_def: "b c X"
      using nonempty(1) nonempty_def by blast
    have xb_type: "b,x c X ×c Z"
      by (simp add: b_def cfunc_prod_type x_type2)
    have yb_type: "b,y c X ×c Z"
      by (simp add: b_def cfunc_prod_type y_type2)
    have "(f ×f g) c b,x = f c b,g c x"
      using b_def cfunc_cross_prod_comp_cfunc_prod type_assms(1) type_assms(2) x_type2 by blast
    also have "... = (f ×f g) c b,y"
      using b_def cfunc_cross_prod_comp_cfunc_prod equals type_assms(1) type_assms(2) y_type2 by auto
    finally have "b,x = b,y"
      using fg_inject fg_type injective_def2 xb_type yb_type by blast
    then show "x = y"
      using b_def cart_prod_eq2 x_type2 y_type2 by blast
  qed
qed

text ‹The next lemma shows that unless both domains are nonempty we gain no new information. 
That is, it will be the case that $f \times g$ is injective, and we cannot infer from this that $f$ or $g$ are
injective since $f \times g$ will be injective no matter what.›
lemma the_nonempty_assumption_above_is_always_required:
  assumes "f : X  Y" "g : Z  W"
  assumes "¬(nonempty X)  ¬(nonempty Z)"
  shows "injective (f ×f g)"
  unfolding injective_def 
proof(cases "nonempty(X)", safe)
  fix x y
  assume nonempty:  "nonempty X"
  assume x_type: "x  c domain (f ×f g)"
  assume "y c domain (f ×f g)"
  then have "¬(nonempty Z)"
    using nonempty assms(3) by blast
  have fg_type: "f ×f g : X ×c Z  Y ×c W"
    by (typecheck_cfuncs, simp add: assms(1,2))
  then have "x  c X ×c Z"
    using x_type cfunc_type_def by auto
  then have "z. zc Z"
    using cart_prod_decomp by blast
  then have False
    using assms(3) nonempty nonempty_def by blast
  then show "x=y"
    by auto
next
  fix x y
  assume X_is_empty: "¬ nonempty X"
  assume x_type: "x  c domain (f ×f g)"
  assume "y c domain(f ×f g)"
  have fg_type: "f ×f g : X ×c Z   Y ×c W"
    by (typecheck_cfuncs, simp add: assms(1,2))
  then have "x  c X ×c Z"
    using x_type cfunc_type_def by auto
  then have "z. zc X"
    using cart_prod_decomp by blast
  then have False
    using assms(3) X_is_empty nonempty_def by blast
  then show "x=y"
    by auto
qed

subsection ‹Surjectivity›

text ‹The definition below corresponds to Definition 2.1.28 in Halvorson.›
definition surjective :: "cfunc  bool" where
 "surjective f   (y. y c codomain f  (x. x c domain f  f c x = y))"

lemma surjective_def2:
  assumes "f : X  Y"
  shows "surjective f   (y. y c Y  (x. x c X  f c x = y))"
  using assms unfolding surjective_def cfunc_type_def by auto

text ‹The lemma below corresponds to Exercise 2.1.30 in Halvorson.›
lemma surjective_is_epimorphism:
  "surjective f  epimorphism f"
  unfolding surjective_def epimorphism_def
proof (cases "nonempty (codomain f)", safe)
  fix g h
  assume f_surj: "y. y c codomain f  (x. x c domain f  f c x = y)"
  assume d_g_eq_cd_f: "domain g = codomain f"
  assume d_h_eq_cd_f: "domain h = codomain f"
  assume gf_eq_hf: "g c f = h c f"
  assume nonempty: "nonempty (codomain f)"

  obtain X Y where f_type: "f : X  Y"
    using nonempty cfunc_type_def f_surj nonempty_def by auto
  obtain A where g_type: "g : Y  A" and h_type: "h : Y  A"
    by (metis cfunc_type_def codomain_comp d_g_eq_cd_f d_h_eq_cd_f f_type gf_eq_hf)
  show "g = h"
  proof (rule ccontr)
    assume "g  h"
    then obtain y where y_in_X: "y c Y" and gy_neq_hy: "g c y  h c y"
      using g_type h_type one_separator by blast
    then obtain x where "x c X" and "f c x = y"
      using cfunc_type_def f_surj f_type by auto
    then have "g c f  h c f"
      using comp_associative2 f_type g_type gy_neq_hy h_type by auto
    then show False
      using gf_eq_hf by auto
  qed
next
  fix g h
  assume empty: "¬ nonempty (codomain f)"
  assume "domain g = codomain f" "domain h = codomain f"
  then show "g c f = h c f  g = h"
    by (metis empty cfunc_type_def codomain_comp nonempty_def one_separator)
qed

text ‹The lemma below corresponds to Proposition 2.2.10 in Halvorson.›
lemma cfunc_cross_prod_surj:
  assumes type_assms: "f : A  C" "g : B  D"
  assumes f_surj: "surjective f" and g_surj: "surjective g"
  shows "surjective (f ×f g)"
  unfolding surjective_def
proof(clarify)
  fix y
  assume y_type: "y c codomain (f ×f g)"
  have fg_type: "f ×f g: A ×c  B  C ×c D"
    using assms  by typecheck_cfuncs    
  then have "y c C ×c D"
    using cfunc_type_def y_type by auto
  then have " c d. c c C  d c D  y = c,d"
    using cart_prod_decomp by blast
  then obtain c d where y_def: "c c C  d c D  y = c,d"
    by blast
  then have " a b. a c A  b c B  f c a = c  g c b = d"
    by (metis cfunc_type_def f_surj g_surj surjective_def type_assms)
  then obtain a b where ab_def: "a c A  b c B  f c a = c  g c b = d"
    by blast
  then obtain x where x_def: "x = a,b"
    by auto
  have x_type: "x c domain (f ×f g)"
    using ab_def cfunc_prod_type cfunc_type_def fg_type x_def by auto
  have "(f ×f g) c x = y"
    using ab_def cfunc_cross_prod_comp_cfunc_prod type_assms(1) type_assms(2) x_def y_def by blast
  then show "x. x c domain (f ×f g)  (f ×f g) c x = y"
    using x_type by blast
qed

lemma cfunc_cross_prod_surj_converse:
  assumes type_assms: "f : A  C" "g : B  D"
  assumes nonempty: "nonempty C  nonempty D"
  assumes "surjective (f ×f g)"
  shows "surjective f  surjective g"
  unfolding surjective_def
proof(safe)
  fix c 
  assume c_type[type_rule]: "c c codomain f"
  then have c_type2:  "c c C"
    using cfunc_type_def type_assms(1) by auto
  obtain d where d_type[type_rule]: "d  c D" 
    using nonempty nonempty_def by blast
  then obtain ab where ab_type[type_rule]: "ab c A ×c B" and ab_def: "(f ×f g) c ab = c, d"
    using assms by (typecheck_cfuncs, metis assms(4) cfunc_type_def surjective_def2)
  then obtain a b where a_type[type_rule]: "a c A" and b_type[type_rule]: "b c B" and ab_def2: "ab = a,b"
    using cart_prod_decomp by blast
  have  "a c domain f  f c a = c"
    using ab_def ab_def2 b_type cfunc_cross_prod_comp_cfunc_prod cfunc_type_def
          comp_type d_type cart_prod_eq2 type_assms by (typecheck_cfuncs, auto)
  then show "x. x c domain f  f c x = c"
    by blast
next
  fix d 
  assume d_type[type_rule]: "d c codomain g"
  then have y_type2:  "d c D"
    using cfunc_type_def type_assms(2) by auto
  obtain c where d_type[type_rule]: "c  c C" 
    using nonempty nonempty_def by blast
  then obtain ab where ab_type[type_rule]: "ab c A ×c B" and ab_def: "(f ×f g) c ab = c, d"
    using assms by (typecheck_cfuncs, metis assms(4) cfunc_type_def surjective_def2)
  then obtain a b where a_type[type_rule]: "a c A" and b_type[type_rule]: "b c B" and ab_def2: "ab = a,b"
    using cart_prod_decomp by blast
  then obtain a b where a_type[type_rule]: "a c A" and b_type[type_rule]: "b c B" and ab_def2: "ab = a,b"
    using cart_prod_decomp by blast
  have  "b c domain g  g c b = d"
    using a_type ab_def ab_def2 cfunc_cross_prod_comp_cfunc_prod cfunc_type_def comp_type d_type cart_prod_eq2 type_assms by(typecheck_cfuncs, force)
  then show "x. x c domain g  g c x = d"
    by blast
qed

subsection ‹Interactions of Cartesian Products with Terminal Objects›

lemma diag_on_elements:
  assumes "x c X"
  shows "diagonal X c x = x,x"
  using assms cfunc_prod_comp cfunc_type_def diagonal_def id_left_unit id_type by auto

lemma one_cross_one_unique_element:
  "∃! x. x c 𝟭 ×c 𝟭"
proof (rule ex1I[where a="diagonal 𝟭"])
  show "diagonal 𝟭 c 𝟭 ×c 𝟭"
    by (simp add: cfunc_prod_type diagonal_def id_type)
next
  fix x
  assume x_type: "x c 𝟭 ×c 𝟭"
  
  have left_eq: "left_cart_proj 𝟭 𝟭 c x = id 𝟭"
    using x_type one_unique_element by (typecheck_cfuncs, blast)
  have right_eq: "right_cart_proj 𝟭 𝟭 c x = id 𝟭"
    using x_type one_unique_element by (typecheck_cfuncs, blast)

  then show "x = diagonal 𝟭"
    unfolding diagonal_def using cfunc_prod_unique id_type left_eq x_type by blast
qed

text ‹The lemma below corresponds to Proposition 2.1.20 in Halvorson.›
lemma X_is_cart_prod1:
  "is_cart_prod X (id X) (β⇘X) X 𝟭"
  unfolding is_cart_prod_def
proof safe
  show "idc X : X  X"
    by typecheck_cfuncs
next
  show "β⇘X: X  𝟭"
    by typecheck_cfuncs
next
  fix f g Y
  assume f_type: "f : Y  X" and g_type: "g : Y  𝟭"
  then show "h. h : Y  X 
           idc X c h = f  β⇘Xc h = g  (h2. h2 : Y  X  idc X c h2 = f  β⇘Xc h2 = g  h2 = h)"
  proof (intro exI[where x=f], safe)
    show "id X c f = f"
      using cfunc_type_def f_type id_left_unit by auto
    show "β⇘Xc f = g"
      by (metis comp_type f_type g_type terminal_func_type terminal_func_unique)
    show "h2. h2 : Y  X  h2 = idc X c h2"
      using cfunc_type_def id_left_unit by auto
  qed
qed

lemma X_is_cart_prod2:
  "is_cart_prod X (β⇘X) (id X) 𝟭 X"
  unfolding is_cart_prod_def
proof safe
  show "idc X : X  X"
    by typecheck_cfuncs
next
  show "β⇘X: X  𝟭"
    by typecheck_cfuncs
next
  fix f g Z
  assume f_type: "f : Z  𝟭" and g_type: "g : Z  X"
  then show "h. h : Z  X 
           β⇘Xc h = f  idc X c h = g  (h2. h2 : Z  X  β⇘Xc h2 = f  idc X c h2 = g  h2 = h)"
  proof (intro exI[where x=g], safe)
    show "idc X c g = g"
      using cfunc_type_def g_type id_left_unit by auto
    show "β⇘Xc g = f"
      by (metis comp_type f_type g_type terminal_func_type terminal_func_unique)
    show "h2. h2 : Z  X  h2 = idc X c h2"
      using cfunc_type_def id_left_unit by auto
  qed
qed

lemma A_x_one_iso_A:
  "X ×c 𝟭  X"
  by (metis X_is_cart_prod1 canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def snd_conv)

lemma one_x_A_iso_A:
  "𝟭 ×c X  X"
  by (meson A_x_one_iso_A isomorphic_is_transitive product_commutes)

text ‹The following four lemmas provide some concrete examples of the above isomorphisms›
lemma left_cart_proj_one_left_inverse:
  "id X,β⇘X c left_cart_proj X 𝟭 = id (X ×c 𝟭)"
  by (typecheck_cfuncs, smt (z3) cfunc_prod_comp cfunc_prod_unique id_left_unit2 id_right_unit2 right_cart_proj_type terminal_func_comp terminal_func_unique)

lemma left_cart_proj_one_right_inverse:
  "left_cart_proj X 𝟭 c id X,β⇘X = id X"
  using left_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)

lemma right_cart_proj_one_left_inverse:
  "β⇘X,id X c right_cart_proj 𝟭 X = id (𝟭 ×c X)"
  by (typecheck_cfuncs, smt (z3) cart_prod_decomp cfunc_prod_comp id_left_unit2 id_right_unit2 right_cart_proj_cfunc_prod terminal_func_comp terminal_func_unique)

lemma right_cart_proj_one_right_inverse:
  "right_cart_proj 𝟭 X c β⇘X,id X = id X"
  using right_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)

lemma cfunc_cross_prod_right_terminal_decomp:
  assumes "f : X  Y" "x : 𝟭  Z"
  shows "f ×f x = f, x c β⇘X c left_cart_proj X 𝟭"
  using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_def cfunc_prod_comp cfunc_type_def
      comp_associative2 right_cart_proj_type terminal_func_comp terminal_func_unique)

text ‹The lemma below corresponds to Proposition 2.1.21 in Halvorson.›
lemma cart_prod_elem_eq:
  assumes "a c X ×c Y" "b c X ×c Y"
  shows "a = b  
    (left_cart_proj X Y c a = left_cart_proj X Y c b 
       right_cart_proj X Y c a = right_cart_proj X Y c b)"
  by (metis (full_types) assms cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type)

text ‹The lemma below corresponds to Note 2.1.22 in Halvorson.›
lemma  element_pair_eq:
  assumes "x c X" "x' c X" "y c Y" "y' c Y"
  shows "x, y = x', y'  x = x'  y = y'"
  by (metis assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)

text ‹The lemma below corresponds to Proposition 2.1.23 in Halvorson.›
lemma nonempty_right_imp_left_proj_epimorphism:
  "nonempty Y  epimorphism (left_cart_proj X Y)"
proof -
  assume "nonempty Y"
  then obtain y where y_in_Y: "y : 𝟭  Y"
    using nonempty_def by blast
  then have id_eq: "(left_cart_proj X Y) c id X, y c β⇘X = id X"
    using comp_type id_type left_cart_proj_cfunc_prod terminal_func_type by blast
  then show "epimorphism (left_cart_proj X Y)"
    unfolding epimorphism_def
  proof clarify
    fix g h
    assume domain_g: "domain g = codomain (left_cart_proj X Y)"
    assume domain_h: "domain h = codomain (left_cart_proj X Y)"
    assume "g c left_cart_proj X Y = h c left_cart_proj X Y"
    then have "g c left_cart_proj X Y c id X, y c β⇘X = h c left_cart_proj X Y c id X, y c β⇘X"
      using y_in_Y by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative domain_g domain_h)
    then show "g = h"
      by (metis cfunc_type_def domain_g domain_h id_eq id_right_unit left_cart_proj_type)
  qed
qed

text ‹The lemma below is the dual of Proposition 2.1.23 in Halvorson.›
lemma nonempty_left_imp_right_proj_epimorphism:
  "nonempty X  epimorphism (right_cart_proj X Y)"
proof - 
  assume "nonempty X"
  then obtain y where y_in_Y: "y: 𝟭  X"
    using nonempty_def by blast
  then have id_eq: "(right_cart_proj X Y) c y c β⇘Y, id Y = id Y"
     using comp_type id_type right_cart_proj_cfunc_prod terminal_func_type by blast
  then show "epimorphism (right_cart_proj X Y)"
    unfolding epimorphism_def
  proof clarify
    fix g h
    assume domain_g: "domain g = codomain (right_cart_proj X Y)"
    assume domain_h: "domain h = codomain (right_cart_proj X Y)"
    assume "g c right_cart_proj X Y = h c right_cart_proj X Y"
    then have "g c right_cart_proj X Y c y c β⇘Y, id Y = h c right_cart_proj X Y c y c β⇘Y, id Y"
      using y_in_Y by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative domain_g domain_h)
    then show "g = h"
      by (metis cfunc_type_def domain_g domain_h id_eq id_right_unit right_cart_proj_type)
  qed
qed

lemma cart_prod_extract_left:
  assumes "f : 𝟭  X" "g : 𝟭  Y"
  shows "f, g = id X, g c β⇘X c f"
proof -
  have "f, g = id X c f, g c β⇘Xc f"
    using assms by (typecheck_cfuncs, metis id_left_unit2 id_right_unit2 id_type one_unique_element)
  also have "... = id X, g c β⇘X c f"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  finally show ?thesis.
qed

lemma cart_prod_extract_right:
  assumes "f : 𝟭  X" "g : 𝟭  Y"
  shows "f, g = f c β⇘Y, id Y c g"
proof -
  have "f, g = f c β⇘Yc g, id Y c g"
    using assms by (typecheck_cfuncs, metis id_left_unit2 id_right_unit2 id_type one_unique_element)
  also have "... = f c β⇘Y, id Y c g"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  finally show ?thesis.
qed

subsubsection ‹Cartesian Products as Pullbacks›

text ‹The definition below corresponds to a definition stated between Definition 2.1.42 and Definition 2.1.43 in Halvorson.›
definition is_pullback :: "cset  cset  cset  cset  cfunc  cfunc  cfunc  cfunc  bool" where
  "is_pullback A B C D ab bd ac cd  
    (ab : A  B  bd : B  D  ac : A  C  cd : C  D  bd c ab = cd c ac  
    ( Z k h. (k : Z  B  h : Z  C  bd c k = cd c h)  
      (∃! j. j : Z  A  ab c j = k  ac c j = h)))"

lemma pullback_unique:
  assumes "ab : A  B" "bd : B  D" "ac : A  C" "cd : C  D"
  assumes "k : Z  B" "h : Z  C"
  assumes "is_pullback A B C D ab bd ac cd"
  shows "bd c k = cd c h  (∃! j. j : Z  A  ab c j = k  ac c j = h)"
  using assms unfolding is_pullback_def by simp

lemma pullback_iff_product:
  assumes "terminal_object(T)"
  assumes f_type[type_rule]: "f : Y  T" 
  assumes g_type[type_rule]: "g : X  T"
  shows "(is_pullback P Y X T (pY) f (pX) g) = (is_cart_prod P pX pY X Y)"
proof(safe)
  assume pullback: "is_pullback P Y X T pY f pX g"
  have f_type[type_rule]: "f : Y  T"
    using is_pullback_def pullback by force
  have g_type[type_rule]: "g : X  T"
    using is_pullback_def pullback by force
  show "is_cart_prod P pX pY X Y"
    unfolding is_cart_prod_def
  proof(safe)
    show pX_type[type_rule]: "pX : P  X"
      using pullback is_pullback_def by force
    show pY_type[type_rule]: "pY : P  Y"
      using pullback is_pullback_def by force
    show "x y Z.
       x : Z  X 
       y : Z  Y 
       h. h : Z  P 
           pX c h = x  pY c h = y  (h2. h2 : Z  P  pX c h2 = x  pY c h2 = y  h2 = h)"
    proof - 
      fix x y Z
      assume x_type[type_rule]: "x : Z  X"
      assume y_type[type_rule]: "y : Z  Y"
      have  "Z k h. k : Z  Y  h : Z  X  f c k = g c h  j. j : Z  P  pY c j = k  pX c j = h"
        using is_pullback_def pullback by blast
      then have "h. h : Z  P 
           pX c h = x  pY c h = y"
        by (smt (verit, ccfv_threshold) assms cfunc_type_def codomain_comp domain_comp f_type g_type terminal_object_def x_type y_type)
      then show "h. h : Z  P 
           pX c h = x  pY c h = y  (h2. h2 : Z  P  pX c h2 = x  pY c h2 = y  h2 = h)"
        by (typecheck_cfuncs, smt (verit, ccfv_threshold) comp_associative2 is_pullback_def pullback)
    qed
  qed
next
  assume prod: "is_cart_prod P pX pY X Y"
  then show "is_pullback P Y X T pY f pX g"
    unfolding is_cart_prod_def is_pullback_def
  proof(typecheck_cfuncs, safe)
    assume pX_type[type_rule]: "pX : P  X"
    assume pY_type[type_rule]: "pY : P  Y"
    show "f c pY = g c pX"
      using assms(1) terminal_object_def by (typecheck_cfuncs, auto)  
    show "Z k h. k : Z  Y  h : Z  X  f c k = g c h  j. j : Z  P  pY c j = k  pX c j = h"
      using is_cart_prod_def prod by blast
    show "Z j y.
       pY c j : Z  Y 
       pX c j : Z  X 
       f c pY c j = g c pX c j  j : Z  P  y : Z  P  pY c y = pY c j  pX c y = pX c j  j = y"
      using is_cart_prod_def prod by blast
  qed
qed

end