Theory Product

section ‹Cartesian Products of Sets›

theory Product
  imports Cfunc
begin

text ‹The axiomatization below corresponds to Axiom 2 (Cartesian Products) in Halvorson.›
axiomatization
  cart_prod :: "cset ⇒ cset ⇒ cset" (infixr "×c" 65) and
  left_cart_proj :: "cset ⇒ cset ⇒ cfunc" and
  right_cart_proj :: "cset ⇒ cset ⇒ cfunc" and
  cfunc_prod :: "cfunc ⇒ cfunc ⇒ cfunc" ("⟨_,_⟩")
where
  left_cart_proj_type[type_rule]: "left_cart_proj X Y : X ×c Y → X" and
  right_cart_proj_type[type_rule]: "right_cart_proj X Y : X ×c Y → Y" and
  cfunc_prod_type[type_rule]: "f : Z → X ⟹ g : Z → Y ⟹ ⟨f,g⟩ : Z → X ×c Y" and
  left_cart_proj_cfunc_prod: "f : Z → X ⟹ g : Z → Y ⟹ left_cart_proj X Y ∘c ⟨f,g⟩ = f" and
  right_cart_proj_cfunc_prod: "f : Z → X ⟹ g : Z → Y ⟹ right_cart_proj X Y ∘c ⟨f,g⟩ = g" and
  cfunc_prod_unique: "f : Z → X ⟹ g : Z → Y ⟹ h : Z → X ×c Y ⟹ 
    left_cart_proj X Y ∘c h = f ⟹ right_cart_proj X Y ∘c h = g ⟹ h = ⟨f,g⟩"

definition is_cart_prod :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cset ⇒ bool" where
  "is_cart_prod W π0 π1 X Y ⟷ 
    (π0 : W → X ∧ π1 : W → Y ∧
    (∀ f g Z. (f : Z → X ∧ g : Z → Y) ⟶ 
      (∃ h. h : Z → W ∧ π0 ∘c h = f ∧ π1 ∘c h = g ∧
        (∀ h2. (h2 : Z → W ∧ π0 ∘c h2 = f ∧ π1 ∘c h2 = g) ⟶ h2 = h))))"

lemma is_cart_prod_def2:
  assumes "π0 : W → X" "π1 : W → Y"
  shows "is_cart_prod W π0 π1 X Y ⟷ 
    (∀ f g Z. (f : Z → X ∧ g : Z → Y) ⟶ 
      (∃ h. h : Z → W ∧ π0 ∘c h = f ∧ π1 ∘c h = g ∧
        (∀ h2. (h2 : Z → W ∧ π0 ∘c h2 = f ∧ π1 ∘c h2 = g) ⟶ h2 = h)))"
  unfolding is_cart_prod_def using assms by auto

abbreviation is_cart_prod_triple :: "cset × cfunc × cfunc ⇒ cset ⇒ cset ⇒ bool" where
  "is_cart_prod_triple Wπ X Y ≡ is_cart_prod (fst Wπ) (fst (snd Wπ)) (snd (snd Wπ)) X Y"

lemma canonical_cart_prod_is_cart_prod:
 "is_cart_prod (X ×c Y) (left_cart_proj X Y) (right_cart_proj X Y) X Y"
  unfolding is_cart_prod_def
proof (typecheck_cfuncs)
  fix f g Z
  assume f_type: "f: Z → X"
  assume g_type: "g: Z → Y"
  show "∃h. h : Z → X ×c Y ∧
           left_cart_proj X Y ∘c h = f ∧
           right_cart_proj X Y ∘c h = g ∧
           (∀h2. h2 : Z → X ×c Y ∧
                 left_cart_proj X Y ∘c h2 = f ∧ right_cart_proj X Y ∘c h2 = g ⟶
                 h2 = h)"
       using f_type g_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod cfunc_prod_unique
       by (intro exI[where x="⟨f,g⟩"], simp add: cfunc_prod_type)
qed

text ‹The lemma below corresponds to Proposition 2.1.8 in Halvorson.›
lemma cart_prods_isomorphic:
  assumes W_cart_prod:  "is_cart_prod_triple (W, π0, π1) X Y"
  assumes W'_cart_prod: "is_cart_prod_triple (W', π'0, π'1) X Y"
  shows "∃ f. f : W → W' ∧ isomorphism f ∧ π'0 ∘c f = π0 ∧ π'1 ∘c f = π1"
proof -
  obtain f where f_def: "f : W → W' ∧ π'0 ∘c f = π0 ∧ π'1 ∘c f = π1"
    using W'_cart_prod W_cart_prod unfolding is_cart_prod_def by (metis fstI sndI)

  obtain g where g_def: "g : W' → W ∧ π0 ∘c g = π'0 ∧ π1 ∘c g = π'1"
      using W'_cart_prod W_cart_prod unfolding is_cart_prod_def by (metis fstI sndI)

  have fg0: "π'0 ∘c (f ∘c g) = π'0"
    using W'_cart_prod comp_associative2 f_def g_def is_cart_prod_def by auto
  have fg1: "π'1 ∘c (f ∘c g) = π'1"
    using W'_cart_prod comp_associative2 f_def g_def is_cart_prod_def by auto

  obtain idW' where "idW' : W' → W' ∧ (∀ h2. (h2 : W' → W' ∧ π'0 ∘c h2 = π'0 ∧ π'1 ∘c h2 = π'1) ⟶ h2 = idW')"
    using W'_cart_prod unfolding is_cart_prod_def by (metis fst_conv snd_conv)
  then have fg: "f ∘c g = id W'"
  proof clarify
    assume idW'_unique: "∀h2. h2 : W' → W' ∧ π'0 ∘c h2 = π'0 ∧ π'1 ∘c h2 = π'1 ⟶ h2 = idW'"
    have 1: "f ∘c g = idW'"
      using comp_type f_def fg0 fg1 g_def idW'_unique by blast
    have 2: "id W' = idW'"
      using W'_cart_prod idW'_unique id_right_unit2 id_type is_cart_prod_def by auto
    from 1 2 show "f ∘c g = id W'"
      by auto
  qed

  have gf0: "π0 ∘c (g ∘c f) = π0"
    using W_cart_prod comp_associative2 f_def g_def is_cart_prod_def by auto
  have gf1: "π1 ∘c (g ∘c f) = π1"
    using W_cart_prod comp_associative2 f_def g_def is_cart_prod_def by auto

  obtain idW where "idW : W → W ∧ (∀ h2. (h2 : W → W ∧ π0 ∘c h2 = π0 ∧ π1 ∘c h2 = π1) ⟶ h2 = idW)"
    using W_cart_prod unfolding is_cart_prod_def by (metis fst_conv snd_conv)
  then have gf: "g ∘c f = id W"
  proof clarify
    assume idW_unique: "∀h2. h2 : W → W ∧ π0 ∘c h2 = π0 ∧ π1 ∘c h2 = π1 ⟶ h2 = idW"
    have 1: "g ∘c f = idW"
      using idW_unique cfunc_type_def codomain_comp domain_comp f_def gf0 gf1 g_def by auto
    have 2: "id W = idW"
      using idW_unique W_cart_prod id_right_unit2 id_type is_cart_prod_def by auto
    from 1 2 show "g ∘c f = id W"
      by auto
  qed

  have f_iso: "isomorphism f"
    using f_def fg g_def gf isomorphism_def3 by blast
  from f_iso f_def show "∃f. f : W → W' ∧ isomorphism f ∧ π'0 ∘c f = π0 ∧ π'1 ∘c f = π1"
    by auto
qed

lemma product_commutes:
  "A ×c B ≅ B ×c A"
proof -
  have id_AB: "⟨right_cart_proj B A, left_cart_proj B A⟩ ∘c ⟨right_cart_proj A B, left_cart_proj A B⟩ = id(A ×c B)"
    by (typecheck_cfuncs, smt (z3) cfunc_prod_unique comp_associative2 id_right_unit2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  have id_BA: "⟨right_cart_proj A B, left_cart_proj A B⟩ ∘c ⟨right_cart_proj B A, left_cart_proj B A⟩ = id(B ×c A)"
    by (typecheck_cfuncs, smt (z3) cfunc_prod_unique comp_associative2 id_right_unit2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  show "A ×c B ≅ B ×c A"
    by (smt (verit, ccfv_threshold) canonical_cart_prod_is_cart_prod cfunc_prod_unique cfunc_type_def id_AB id_BA is_cart_prod_def is_isomorphic_def isomorphism_def)
qed

lemma cart_prod_eq:
  assumes "a : Z → X ×c Y" "b : Z →  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)

lemma cart_prod_eqI:
  assumes "a : Z → X ×c Y" "b : Z →  X ×c Y"
  assumes "(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)"
  shows "a = b"
  using assms cart_prod_eq by blast

lemma cart_prod_eq2:
  assumes "a : Z → X" "b : Z → Y" "c : Z →  X" "d : Z →  Y"
  shows "⟨a, b⟩ = ⟨c,d⟩ ⟷ (a = c ∧ b = d)"
  by (metis assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)

lemma cart_prod_decomp:
  assumes "a : A → X ×c Y"
  shows "∃ x y. a = ⟨x, y⟩ ∧ x : A → X ∧ y : A → Y"
proof (rule exI[where x="left_cart_proj X Y ∘c a"], intro exI [where x="right_cart_proj X Y ∘c a"], safe)
  show "a = ⟨left_cart_proj X Y ∘c a,right_cart_proj X Y ∘c a⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_unique)
  show "left_cart_proj X Y ∘c a : A →  X"
    using assms by typecheck_cfuncs
  show "right_cart_proj X Y ∘c a : A → Y"
    using assms by typecheck_cfuncs
qed

subsection ‹Diagonal Functions›

text ‹The definition below corresponds to Definition 2.1.9 in Halvorson.›
definition diagonal :: "cset ⇒ cfunc" where
  "diagonal X = ⟨id X,id X⟩"

lemma diagonal_type[type_rule]:
  "diagonal X : X → X ×c X"
  unfolding diagonal_def by (simp add: cfunc_prod_type id_type)

lemma diag_mono:
"monomorphism(diagonal X)"
proof - 
  have "left_cart_proj X X ∘c diagonal X = id X"
    by (metis diagonal_def id_type left_cart_proj_cfunc_prod)
  then show "monomorphism(diagonal X)"
    by (metis cfunc_type_def comp_monic_imp_monic diagonal_type id_isomorphism iso_imp_epi_and_monic left_cart_proj_type)
qed

subsection ‹Products of Functions›

text ‹The definition below corresponds to Definition 2.1.10 in Halvorson.›
definition cfunc_cross_prod :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "×f" 55) where
  "f ×f g = ⟨f ∘c left_cart_proj (domain f) (domain g), g ∘c right_cart_proj (domain f) (domain g)⟩"

lemma cfunc_cross_prod_def2: 
  assumes "f : X → Y" "g : V→ W"
  shows "f ×f g = ⟨f ∘c left_cart_proj X V, g ∘c right_cart_proj X V⟩"
  using assms cfunc_cross_prod_def cfunc_type_def by auto
    
lemma cfunc_cross_prod_type[type_rule]:
  "f : W → Y ⟹ g : X → Z ⟹ f ×f g : W ×c X → Y ×c Z"
  unfolding cfunc_cross_prod_def
  using cfunc_prod_type cfunc_type_def comp_type left_cart_proj_type right_cart_proj_type by auto

lemma left_cart_proj_cfunc_cross_prod:
  "f : W → Y ⟹ g : X → Z ⟹ left_cart_proj Y Z ∘c f ×f g = f ∘c left_cart_proj W X"
  unfolding cfunc_cross_prod_def
  using cfunc_type_def comp_type left_cart_proj_cfunc_prod left_cart_proj_type right_cart_proj_type by (smt (verit))

lemma right_cart_proj_cfunc_cross_prod:
  "f : W → Y ⟹ g : X → Z ⟹ right_cart_proj Y Z ∘c f ×f g = g ∘c right_cart_proj W X"
  unfolding cfunc_cross_prod_def
  using cfunc_type_def comp_type right_cart_proj_cfunc_prod left_cart_proj_type right_cart_proj_type by (smt (verit))

lemma cfunc_cross_prod_unique: "f : W → Y ⟹ g : X → Z ⟹ h : W ×c X → Y ×c Z ⟹
    left_cart_proj Y Z ∘c h = f ∘c left_cart_proj W X ⟹
    right_cart_proj Y Z ∘c h = g ∘c right_cart_proj W X ⟹ h = f ×f g"
  unfolding cfunc_cross_prod_def
  using cfunc_prod_unique cfunc_type_def comp_type left_cart_proj_type right_cart_proj_type by auto

text ‹The lemma below corresponds to Proposition 2.1.11 in Halvorson.›
lemma identity_distributes_across_composition:
  assumes f_type: "f : A → B" and g_type: "g : B → C"
  shows "id X ×f (g  ∘c f) = (id X ×f g) ∘c (id X ×f f)"
proof -
  from cfunc_cross_prod_unique
  have uniqueness: "∀h. h : X ×c A → X ×c C ∧
    left_cart_proj X C ∘c h = idc X ∘c left_cart_proj X A ∧
    right_cart_proj X C ∘c h = (g ∘c f) ∘c right_cart_proj X A ⟶
    h = idc X ×f (g ∘c f)"
    by (meson comp_type f_type g_type id_type)

  have left_eq: "left_cart_proj X C ∘c (idc X ×f g) ∘c (idc X ×f f) = idc X ∘c left_cart_proj X A"
    using assms by (typecheck_cfuncs, smt comp_associative2 id_left_unit2 left_cart_proj_cfunc_cross_prod left_cart_proj_type)
  have right_eq: "right_cart_proj X C ∘c (idc X ×f g) ∘c (idc X ×f f) = (g ∘c f) ∘c right_cart_proj X A"
    using assms by(typecheck_cfuncs, smt comp_associative2 right_cart_proj_cfunc_cross_prod right_cart_proj_type)
  show "idc X ×f g ∘c f = (idc X ×f g) ∘c idc X ×f f"
    using assms left_eq right_eq uniqueness by (typecheck_cfuncs, auto)
qed

lemma cfunc_cross_prod_comp_cfunc_prod:
  assumes a_type: "a : A → W" and b_type: "b : A → X"
  assumes f_type: "f : W → Y" and g_type: "g : X → Z"
  shows "(f ×f g) ∘c ⟨a, b⟩ = ⟨f ∘c a, g ∘c b⟩"
proof -
  from cfunc_prod_unique have uniqueness:
    "∀h. h : A → Y ×c Z ∧ left_cart_proj Y Z ∘c h = f ∘c a ∧ right_cart_proj Y Z ∘c h = g ∘c b ⟶ 
      h = ⟨f ∘c a, g ∘c b⟩"
    using assms comp_type by blast

  have "left_cart_proj Y Z ∘c (f ×f g) ∘c ⟨a, b⟩ = f ∘c left_cart_proj W X ∘c ⟨a, b⟩"
    using assms by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
  then have left_eq: "left_cart_proj Y Z ∘c (f ×f g) ∘c ⟨a, b⟩ = f ∘c a"
    using a_type b_type left_cart_proj_cfunc_prod by auto
  
  have "right_cart_proj Y Z ∘c (f ×f g) ∘c ⟨a, b⟩ = g ∘c right_cart_proj W X ∘c ⟨a, b⟩"
    using assms by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
  then have right_eq: "right_cart_proj Y Z ∘c (f ×f g) ∘c ⟨a, b⟩ = g ∘c b"
    using a_type b_type right_cart_proj_cfunc_prod by auto

  show "(f ×f g) ∘c ⟨a,b⟩ = ⟨f ∘c a,g ∘c b⟩"
    using uniqueness left_eq right_eq assms by (meson cfunc_cross_prod_type cfunc_prod_type comp_type uniqueness)
qed

lemma cfunc_prod_comp:
  assumes f_type: "f : X → Y"
  assumes a_type: "a : Y → A" and b_type: "b : Y → B"
  shows "⟨a, b⟩ ∘c f = ⟨a ∘c f, b ∘c f⟩"
proof -
  have same_left_proj: "left_cart_proj A B ∘c ⟨a, b⟩ ∘c f = a ∘c f"
    using assms by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_prod)
  have same_right_proj: "right_cart_proj A B ∘c ⟨a, b⟩ ∘c f = b ∘c f"
    using assms comp_associative2 right_cart_proj_cfunc_prod by (typecheck_cfuncs, auto)
  show "⟨a,b⟩ ∘c f = ⟨a ∘c f, b ∘c f⟩"
    by (typecheck_cfuncs, metis a_type b_type cfunc_prod_unique f_type same_left_proj same_right_proj)
qed

text ‹The lemma below corresponds to Exercise 2.1.12 in Halvorson.›
lemma id_cross_prod: "id(X) ×f id(Y) = id(X ×c Y)"
  by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_unique id_left_unit2 id_right_unit2 left_cart_proj_type right_cart_proj_type)

text ‹The lemma below corresponds to Exercise 2.1.14 in Halvorson.›
lemma cfunc_cross_prod_comp_diagonal:
  assumes "f: X → Y" 
  shows "(f ×f f) ∘c diagonal(X) = diagonal(Y) ∘c f"
  unfolding diagonal_def
proof -
  have "(f ×f f) ∘c ⟨idc X, idc X⟩ = ⟨f ∘c idc X, f ∘c idc X⟩"
    using assms cfunc_cross_prod_comp_cfunc_prod id_type by blast
  also have "... = ⟨f, f⟩"
    using assms cfunc_type_def id_right_unit by auto
  also have "... = ⟨idc Y ∘c f, idc Y ∘c f⟩"
    using assms cfunc_type_def id_left_unit by auto
  also have "... = ⟨idc Y, idc Y⟩ ∘c f"
    using assms cfunc_prod_comp id_type by fastforce
  finally show "(f ×f f) ∘c ⟨idc X,idc X⟩ = ⟨idc Y,idc Y⟩ ∘c f".
qed

lemma cfunc_cross_prod_comp_cfunc_cross_prod:
  assumes "a : A → X" "b : B → Y" "x : X → Z" "y : Y → W"
  shows "(x ×f y) ∘c (a ×f b) = (x ∘c a) ×f (y ∘c b)"
proof -
  have "(x ×f y) ∘c ⟨a ∘c left_cart_proj A B , b ∘c right_cart_proj A B⟩
      = ⟨x ∘c a ∘c left_cart_proj A B, y ∘c b ∘c right_cart_proj A B⟩"
    by (meson assms cfunc_cross_prod_comp_cfunc_prod comp_type left_cart_proj_type right_cart_proj_type)
  then show "(x ×f y) ∘c a ×f b = (x ∘c a) ×f y ∘c b"
    by (typecheck_cfuncs,smt (z3) assms cfunc_cross_prod_def2 comp_associative2 left_cart_proj_type right_cart_proj_type)
qed

lemma cfunc_cross_prod_mono:
  assumes type_assms: "f : X → Y" "g : Z → W"
  assumes f_mono: "monomorphism f" and g_mono: "monomorphism g"
  shows "monomorphism (f ×f g)"
  using type_assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix x y A
  assume x_type: "x : A → X ×c Z"
  assume y_type: "y : A → X ×c Z"

  obtain x1 x2 where x_expand: "x = ⟨x1, x2⟩" and x1_x2_type: "x1 : A → X" "x2 : A → Z"
    using cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type x_type by blast
  obtain y1 y2 where y_expand: "y = ⟨y1, y2⟩" and y1_y2_type: "y1 : A → X" "y2 : A → Z"
    using cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type y_type by blast

  assume "(f ×f g) ∘c x = (f ×f g) ∘c y"
  then have "(f ×f g) ∘c ⟨x1, x2⟩ = (f ×f g) ∘c ⟨y1, y2⟩"
    using x_expand y_expand by blast
  then have "⟨f ∘c x1, g ∘c x2⟩ = ⟨f ∘c y1, g ∘c y2⟩"
    using cfunc_cross_prod_comp_cfunc_prod type_assms x1_x2_type y1_y2_type by auto
  then have "f ∘c x1 = f ∘c y1 ∧ g ∘c x2 = g ∘c y2"
    by (meson cart_prod_eq2 comp_type type_assms x1_x2_type y1_y2_type)
  then have "x1 = y1 ∧ x2 = y2"
    using cfunc_type_def f_mono g_mono monomorphism_def type_assms x1_x2_type y1_y2_type by auto
  then have "⟨x1, x2⟩ = ⟨y1, y2⟩"
    by blast
  then show "x = y"
    by (simp add: x_expand y_expand)
qed

subsection ‹Useful Cartesian Product Permuting Functions›

subsubsection ‹Swapping a Cartesian Product›

definition swap :: "cset ⇒ cset ⇒ cfunc" where
  "swap X Y = ⟨right_cart_proj X Y, left_cart_proj X Y⟩"

lemma swap_type[type_rule]: "swap X Y : X ×c Y → Y ×c X"
  unfolding swap_def by (simp add: cfunc_prod_type left_cart_proj_type right_cart_proj_type)

lemma swap_ap:
  assumes "x : A → X" "y : A → Y"
  shows "swap X Y ∘c ⟨x, y⟩ = ⟨y, x⟩"
proof -
  have "swap X Y ∘c ⟨x, y⟩ = ⟨right_cart_proj X Y,left_cart_proj X Y⟩ ∘c ⟨x,y⟩"
    unfolding swap_def by auto
  also have "... = ⟨right_cart_proj X Y ∘c ⟨x,y⟩, left_cart_proj X Y ∘c ⟨x,y⟩⟩"
    by (meson assms cfunc_prod_comp cfunc_prod_type left_cart_proj_type right_cart_proj_type)
  also have "... = ⟨y, x⟩"
    using assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by auto
  finally show ?thesis.
qed

lemma swap_cross_prod:
  assumes "x : A → X" "y : B → Y"
  shows "swap X Y ∘c (x ×f y) = (y ×f x) ∘c swap A B"
proof -
  have "swap X Y ∘c (x ×f y) = swap X Y ∘c ⟨x ∘c left_cart_proj A B, y ∘c right_cart_proj A B⟩"
    using assms unfolding cfunc_cross_prod_def cfunc_type_def by auto
  also have "... = ⟨y ∘c right_cart_proj A B, x ∘c left_cart_proj A B⟩"
    by (meson assms comp_type left_cart_proj_type right_cart_proj_type swap_ap)
  also have "... = (y ×f x) ∘c ⟨right_cart_proj A B, left_cart_proj A B⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
  also have "... = (y ×f x) ∘c swap A B"
    unfolding swap_def by auto
  finally show ?thesis.
qed

lemma swap_idempotent:
  "swap Y X ∘c swap X Y = id (X ×c Y)"
  by (metis swap_def cfunc_prod_unique id_right_unit2 id_type left_cart_proj_type
      right_cart_proj_type swap_ap)

lemma swap_mono:
  "monomorphism(swap X Y)"
  by (metis cfunc_type_def iso_imp_epi_and_monic isomorphism_def swap_idempotent swap_type)

subsubsection ‹Permuting a Cartesian Product to Associate to the Right›

definition associate_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "associate_right X Y Z =
    ⟨
      left_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z, 
      ⟨
        right_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z,
        right_cart_proj (X ×c Y) Z
      ⟩
    ⟩"

lemma associate_right_type[type_rule]: "associate_right X Y Z : (X ×c Y) ×c Z → X ×c (Y ×c Z)"
  unfolding associate_right_def by (meson cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type)

lemma associate_right_ap:
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "associate_right X Y Z ∘c ⟨⟨x, y⟩, z⟩ = ⟨x, ⟨y, z⟩⟩"
proof -
  have "associate_right X Y Z ∘c ⟨⟨x, y⟩, z⟩ = ⟨(left_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z) ∘c ⟨⟨x,y⟩,z⟩, 
    ⟨(right_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z) ∘c ⟨⟨x,y⟩,z⟩, right_cart_proj (X ×c Y) Z ∘c ⟨⟨x,y⟩,z⟩⟩⟩"
    by (typecheck_cfuncs, smt (verit, best) assms associate_right_def cfunc_prod_comp cfunc_prod_type)
  also have "... = ⟨left_cart_proj X Y ∘c ⟨x,y⟩, ⟨right_cart_proj X Y ∘c ⟨x,y⟩, z⟩⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  also have "... =⟨x, ⟨y, z⟩⟩"
    using assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by auto
  finally show ?thesis.
qed

lemma associate_right_crossprod_ap:
  assumes "x : A → X" "y : B → Y" "z : C → Z"
  shows "associate_right X Y Z ∘c ((x ×f y) ×f z) = (x ×f (y×f z)) ∘c  associate_right A B C"
proof-
  have "associate_right X Y Z ∘c ((x ×f y) ×f z) =
        associate_right X Y Z ∘c ⟨⟨x  ∘c left_cart_proj A B, y ∘c right_cart_proj A B⟩ ∘c left_cart_proj (A×cB) C, z ∘c right_cart_proj (A ×c B) C⟩"
    using assms unfolding cfunc_cross_prod_def2 by(typecheck_cfuncs, unfold cfunc_cross_prod_def2, auto) 
  also have "... = associate_right X Y Z ∘c ⟨⟨x  ∘c left_cart_proj A B ∘c left_cart_proj (A×cB) C, y  ∘c right_cart_proj A B ∘c left_cart_proj (A×cB) C⟩, z ∘c right_cart_proj (A ×c B) C⟩"
    using assms  cfunc_prod_comp comp_associative2 by (typecheck_cfuncs, auto)
  also have "... = ⟨x  ∘c left_cart_proj A B ∘c left_cart_proj (A×cB) C, ⟨y ∘c right_cart_proj A B ∘c left_cart_proj (A×cB) C, z ∘c right_cart_proj (A ×c B) C⟩⟩"
    using assms by (typecheck_cfuncs, simp add: associate_right_ap)
  also have "... = ⟨x  ∘c left_cart_proj A B ∘c left_cart_proj (A×cB) C, (y ×f z)∘c ⟨right_cart_proj A B ∘c left_cart_proj (A×cB) C,right_cart_proj (A ×c B) C⟩⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
  also have "... = (x ×f (y×f z)) ∘c ⟨left_cart_proj A B ∘c left_cart_proj (A×cB) C,⟨right_cart_proj A B ∘c left_cart_proj (A×cB) C,right_cart_proj (A ×c B) C⟩⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
  also have "... = (x ×f (y×f z)) ∘c  associate_right A B C"   
    unfolding associate_right_def by auto
  finally show ?thesis.
qed

subsubsection ‹Permuting a Cartesian Product to Associate to the Left›

definition associate_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "associate_left X Y Z =
    ⟨
      ⟨
        left_cart_proj X (Y ×c Z),
        left_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)
      ⟩,
      right_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)
    ⟩"

lemma associate_left_type[type_rule]: "associate_left X Y Z : X ×c (Y ×c Z) → (X ×c Y) ×c Z"
  unfolding associate_left_def
  by (meson cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type)

lemma associate_left_ap:
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "associate_left X Y Z ∘c ⟨x, ⟨y, z⟩⟩ = ⟨⟨x, y⟩, z⟩"
proof -
  have "associate_left X Y Z ∘c ⟨x, ⟨y, z⟩⟩  = ⟨⟨left_cart_proj X (Y ×c Z),
        left_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)⟩ ∘c ⟨x, ⟨y, z⟩⟩,
        right_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)  ∘c ⟨x, ⟨y, z⟩⟩⟩"
    using assms associate_left_def cfunc_prod_comp cfunc_type_def comp_associative comp_type by (typecheck_cfuncs, auto)
  also have "... = ⟨ ⟨left_cart_proj X (Y ×c Z) ∘c ⟨x, ⟨y, z⟩⟩,
        left_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z) ∘c ⟨x, ⟨y, z⟩⟩⟩,
        right_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)  ∘c ⟨x, ⟨y, z⟩⟩⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = ⟨⟨x, left_cart_proj Y Z ∘c ⟨y, z⟩⟩, right_cart_proj Y Z ∘c ⟨y, z⟩⟩"
    using assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by (typecheck_cfuncs, auto)
  also have "... = ⟨⟨x, y⟩, z⟩"
    using assms left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by auto
  finally show ?thesis.
qed

lemma right_left: 
 "associate_right A B C ∘c associate_left A B C = id (A ×c (B ×c C))"
  by (typecheck_cfuncs, smt (verit, ccfv_threshold) associate_left_def associate_right_ap cfunc_prod_unique comp_type id_right_unit2 left_cart_proj_type right_cart_proj_type)

lemma left_right: 
 "associate_left A B C ∘c associate_right A B C = id ((A ×c B) ×c C)"
    by (smt (z3) associate_left_ap associate_right_def cfunc_cross_prod_def cfunc_prod_unique comp_type id_cross_prod id_domain id_left_unit2 left_cart_proj_type right_cart_proj_type)

lemma product_associates:
  "A ×c (B ×c C)  ≅ (A ×c B) ×c C"
    by (metis associate_left_type associate_right_type cfunc_type_def is_isomorphic_def isomorphism_def left_right right_left) 

lemma associate_left_crossprod_ap:
  assumes "x : A → X" "y : B → Y" "z : C → Z"
  shows "associate_left X Y Z ∘c (x ×f (y×f z)) = ((x ×f y)×f z) ∘c  associate_left A B C"
proof-
  have "associate_left X Y Z ∘c (x ×f (y×f z)) =
        associate_left X Y Z ∘c ⟨x ∘c left_cart_proj A (B×cC), ⟨y ∘c left_cart_proj B C, z ∘c right_cart_proj B C⟩ ∘c right_cart_proj A (B×cC)⟩"
    using assms unfolding cfunc_cross_prod_def2 by(typecheck_cfuncs, unfold cfunc_cross_prod_def2, auto) 
  also have "... = associate_left X Y Z ∘c ⟨x ∘c left_cart_proj A (B×cC), ⟨y ∘c left_cart_proj B C ∘c right_cart_proj A (B×cC), z ∘c right_cart_proj B C ∘c right_cart_proj A (B×cC)⟩⟩"
    using assms  cfunc_prod_comp comp_associative2 by (typecheck_cfuncs, auto)
  also have "... = ⟨⟨x ∘c left_cart_proj A (B×cC), y ∘c left_cart_proj B C ∘c right_cart_proj A (B×cC)⟩,z ∘c right_cart_proj B C ∘c right_cart_proj A (B×cC)⟩"
    using assms by (typecheck_cfuncs, simp add: associate_left_ap)
  also have "... = ⟨(x ×f y)∘c ⟨ left_cart_proj A (B×cC), left_cart_proj B C ∘c right_cart_proj A (B×cC)⟩,z ∘c right_cart_proj B C ∘c right_cart_proj A (B×cC)⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
  also have "... = ((x ×f y)×f z) ∘c ⟨⟨left_cart_proj A (B×cC), left_cart_proj B C ∘c right_cart_proj A (B×cC)⟩,right_cart_proj B C ∘c right_cart_proj A (B×cC)⟩"
    using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
  also have "... = ((x ×f y)×f z) ∘c associate_left A B C"   
    unfolding associate_left_def by auto
  finally show ?thesis.
qed
  
subsubsection ‹Distributing over a Cartesian Product from the Right›

definition distribute_right_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_right_left X Y Z = 
    ⟨left_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z, right_cart_proj (X ×c Y) Z⟩"

lemma distribute_right_left_type[type_rule]:
  "distribute_right_left X Y Z : (X ×c Y) ×c Z → X ×c Z"
  unfolding distribute_right_left_def
  using cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type by blast

lemma distribute_right_left_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_right_left X Y Z ∘c ⟨⟨x, y⟩, z⟩ = ⟨x, z⟩"
  unfolding distribute_right_left_def 
  by (typecheck_cfuncs, smt (verit, best) assms cfunc_prod_comp comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)

definition distribute_right_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_right_right X Y Z = 
    ⟨right_cart_proj X Y ∘c left_cart_proj (X ×c Y) Z, right_cart_proj (X ×c Y) Z⟩"

lemma distribute_right_right_type[type_rule]:
  "distribute_right_right X Y Z : (X ×c Y) ×c Z → Y ×c Z"
  unfolding distribute_right_right_def
  using cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type by blast

lemma distribute_right_right_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_right_right X Y Z ∘c ⟨⟨x, y⟩, z⟩ = ⟨y, z⟩"
  unfolding distribute_right_right_def  
  by (typecheck_cfuncs, smt (z3) assms cfunc_prod_comp comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)

definition distribute_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_right X Y Z = ⟨distribute_right_left X Y Z, distribute_right_right X Y Z⟩"

lemma distribute_right_type[type_rule]:
  "distribute_right X Y Z : (X ×c Y) ×c Z → (X ×c Z) ×c (Y ×c Z)"
  unfolding distribute_right_def
  by (simp add: cfunc_prod_type distribute_right_left_type distribute_right_right_type)

lemma distribute_right_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_right X Y Z ∘c ⟨⟨x, y⟩, z⟩ = ⟨⟨x, z⟩, ⟨y, z⟩⟩"
  using assms unfolding distribute_right_def  
  by (typecheck_cfuncs, simp add: cfunc_prod_comp distribute_right_left_ap distribute_right_right_ap)

lemma distribute_right_mono:
  "monomorphism (distribute_right X Y Z)"
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix g h A
  assume "g : A → (X ×c Y) ×c Z"
  then obtain g1 g2 g3 where g_expand: "g = ⟨⟨g1, g2⟩, g3⟩"
      and g1_g2_g3_types: "g1 : A → X" "g2 : A → Y" "g3 : A → Z"
    using cart_prod_decomp by blast 
  assume "h : A → (X ×c Y) ×c Z"
  then obtain h1 h2 h3 where h_expand: "h = ⟨⟨h1, h2⟩, h3⟩"
      and h1_h2_h3_types: "h1 : A → X" "h2 : A → Y" "h3 : A → Z"
    using cart_prod_decomp by blast 

  assume "distribute_right X Y Z ∘c g = distribute_right X Y Z ∘c h"
  then have "distribute_right X Y Z ∘c ⟨⟨g1, g2⟩, g3⟩ = distribute_right X Y Z ∘c ⟨⟨h1, h2⟩, h3⟩"
    using g_expand h_expand by auto
  then have "⟨⟨g1, g3⟩, ⟨g2, g3⟩⟩ = ⟨⟨h1, h3⟩, ⟨h2, h3⟩⟩"
    using distribute_right_ap g1_g2_g3_types h1_h2_h3_types by auto
  then have "⟨g1, g3⟩ = ⟨h1, h3⟩ ∧ ⟨g2, g3⟩ = ⟨h2, h3⟩"
    using g1_g2_g3_types h1_h2_h3_types cart_prod_eq2 by (typecheck_cfuncs, auto)
  then have "g1 = h1 ∧ g2 = h2 ∧ g3 = h3"
    using g1_g2_g3_types h1_h2_h3_types cart_prod_eq2 by auto
  then have "⟨⟨g1, g2⟩, g3⟩ = ⟨⟨h1, h2⟩, h3⟩"
    by simp
  then show "g = h"
    by (simp add: g_expand h_expand)
qed

subsubsection ‹Distributing over a Cartesian Product from the Left›

definition distribute_left_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_left_left X Y Z = 
    ⟨left_cart_proj X (Y ×c Z), left_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)⟩"

lemma distribute_left_left_type[type_rule]:
  "distribute_left_left X Y Z : X ×c (Y ×c Z) → X ×c Y"
  unfolding distribute_left_left_def
  using cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type by blast

lemma distribute_left_left_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_left_left X Y Z ∘c ⟨x, ⟨y, z⟩⟩ = ⟨x, y⟩"
  using assms distribute_left_left_def  
  by (typecheck_cfuncs, smt (z3) associate_left_ap associate_left_def cart_prod_decomp cart_prod_eq2 cfunc_prod_comp comp_associative2 distribute_left_left_def right_cart_proj_cfunc_prod right_cart_proj_type)

definition distribute_left_right :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_left_right X Y Z = 
    ⟨left_cart_proj X (Y ×c Z), right_cart_proj Y Z ∘c right_cart_proj X (Y ×c Z)⟩"

lemma distribute_left_right_type[type_rule]:
  "distribute_left_right X Y Z : X ×c (Y ×c Z) → X ×c Z"
  unfolding distribute_left_right_def
  using cfunc_prod_type comp_type left_cart_proj_type right_cart_proj_type by blast

lemma distribute_left_right_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_left_right X Y Z ∘c ⟨x, ⟨y, z⟩⟩ = ⟨x, z⟩"
  using assms unfolding distribute_left_right_def  
  by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)

definition distribute_left :: "cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "distribute_left X Y Z = ⟨distribute_left_left X Y Z, distribute_left_right X Y Z⟩"

lemma distribute_left_type[type_rule]:
  "distribute_left X Y Z : X ×c (Y ×c Z) → (X ×c Y) ×c (X ×c Z)"
  unfolding distribute_left_def
  by (simp add: cfunc_prod_type distribute_left_left_type distribute_left_right_type)

lemma distribute_left_ap: 
  assumes "x : A → X" "y : A → Y" "z : A → Z"
  shows "distribute_left X Y Z ∘c ⟨x, ⟨y, z⟩⟩ = ⟨⟨x, y⟩, ⟨x, z⟩⟩"
  using assms unfolding distribute_left_def 
  by (typecheck_cfuncs, simp add: cfunc_prod_comp distribute_left_left_ap distribute_left_right_ap)

lemma distribute_left_mono:
  "monomorphism (distribute_left X Y Z)"
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix g h A
  assume g_type: "g : A → X ×c (Y ×c Z)"
  then obtain g1 g2 g3 where g_expand: "g = ⟨g1, ⟨g2, g3⟩⟩"
      and g1_g2_g3_types: "g1 : A → X" "g2 : A → Y" "g3 : A → Z"
    using cart_prod_decomp by blast 
  assume h_type: "h : A → X ×c (Y ×c Z)"
  then obtain h1 h2 h3 where h_expand: "h = ⟨h1, ⟨h2, h3⟩⟩"
      and h1_h2_h3_types: "h1 : A → X" "h2 : A → Y" "h3 : A → Z"
    using cart_prod_decomp by blast 

  assume "distribute_left X Y Z ∘c g = distribute_left X Y Z ∘c h"
  then have "distribute_left X Y Z ∘c ⟨g1, ⟨g2, g3⟩⟩ = distribute_left X Y Z ∘c ⟨h1, ⟨h2, h3⟩⟩"
    using g_expand h_expand by auto
  then have "⟨⟨g1, g2⟩, ⟨g1, g3⟩⟩ = ⟨⟨h1, h2⟩, ⟨h1, h3⟩⟩"
    using distribute_left_ap g1_g2_g3_types h1_h2_h3_types by auto
  then have "⟨g1, g2⟩ = ⟨h1, h2⟩ ∧ ⟨g1, g3⟩ = ⟨h1, h3⟩"
    using g1_g2_g3_types h1_h2_h3_types cart_prod_eq2 by (typecheck_cfuncs, auto)
  then have "g1 = h1 ∧ g2 = h2 ∧ g3 = h3"
    using g1_g2_g3_types h1_h2_h3_types cart_prod_eq2 by auto
  then have "⟨g1, ⟨g2, g3⟩⟩ = ⟨h1, ⟨h2, h3⟩⟩"
    by simp
  then show "g = h"
    by (simp add: g_expand h_expand)
qed

subsubsection ‹Selecting Pairs from a Pair of Pairs›

definition outers :: "cset ⇒ cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "outers A B C D = ⟨
      left_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D),
      right_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D)
    ⟩"

lemma outers_type[type_rule]: "outers A B C D : (A ×c B) ×c (C ×c D) → (A ×c D)"
  unfolding outers_def by typecheck_cfuncs

lemma outers_apply:
  assumes "a : Z → A" "b : Z → B" "c : Z → C" "d : Z → D"
  shows "outers A B C D ∘c ⟨⟨a,b⟩, ⟨c,d⟩⟩ = ⟨a,d⟩"
proof -
  have "outers A B C D ∘c ⟨⟨a,b⟩, ⟨c,d⟩⟩ = ⟨
      left_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩,
      right_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩
    ⟩"
    unfolding outers_def  using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = ⟨left_cart_proj A B ∘c ⟨a,b⟩, right_cart_proj C D ∘c ⟨c,d⟩⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  also have "... = ⟨a, d⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  finally show ?thesis.
qed

definition inners :: "cset ⇒ cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "inners A B C D = ⟨
      right_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D),
      left_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D)
    ⟩"

lemma inners_type[type_rule]: "inners A B C D : (A ×c B) ×c (C ×c D) → (B ×c C)"
  unfolding inners_def by typecheck_cfuncs
    
lemma inners_apply:
  assumes "a : Z → A" "b : Z → B" "c : Z → C" "d : Z → D"
  shows "inners A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨b,c⟩"
proof -
  have "inners A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨
      right_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩,
      left_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩⟩"
    unfolding inners_def using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = ⟨right_cart_proj A B ∘c ⟨a,b⟩, left_cart_proj C D ∘c ⟨c,d⟩⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  also have "... = ⟨b, c⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  finally show ?thesis.
qed

definition lefts :: "cset ⇒ cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "lefts A B C D = ⟨
      left_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D),
      left_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D)
    ⟩"

lemma lefts_type[type_rule]: "lefts A B C D : (A ×c B) ×c (C ×c D) → (A ×c C)"
  unfolding lefts_def by typecheck_cfuncs

lemma lefts_apply:
  assumes "a : Z → A" "b : Z → B" "c : Z → C" "d : Z → D"
  shows "lefts A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨a,c⟩"
proof -
  have "lefts A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨left_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩, left_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩⟩"
    unfolding lefts_def using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = ⟨left_cart_proj A B ∘c ⟨a,b⟩, left_cart_proj C D ∘c ⟨c,d⟩⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  also have "... = ⟨a, c⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod)
  finally show ?thesis.
qed

definition rights :: "cset ⇒ cset ⇒ cset ⇒ cset ⇒ cfunc" where
  "rights A B C D = ⟨
      right_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D),
      right_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D)
    ⟩"

lemma rights_type[type_rule]: "rights A B C D : (A ×c B) ×c (C ×c D) → (B ×c D)"
  unfolding rights_def by typecheck_cfuncs

lemma rights_apply:
  assumes "a : Z → A" "b : Z → B" "c : Z → C" "d : Z → D"
  shows "rights A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨b,d⟩"
proof -
  have "rights A B C D ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩ = ⟨right_cart_proj A B ∘c left_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩, right_cart_proj C D ∘c right_cart_proj (A ×c B) (C ×c D) ∘c ⟨⟨a,b⟩, ⟨c, d⟩⟩⟩"
    unfolding rights_def using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
  also have "... = ⟨right_cart_proj A B ∘c ⟨a,b⟩, right_cart_proj C D ∘c ⟨c,d⟩⟩"
    using assms by (typecheck_cfuncs, simp add: left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  also have "... = ⟨b, d⟩"
    using assms by (typecheck_cfuncs, simp add: right_cart_proj_cfunc_prod)
  finally show ?thesis.
qed

end