Theory Equivalence

section  ‹Equivalence Classes and Coequalizers›

theory Equivalence
  imports Truth
begin
 
definition reflexive_on :: "cset ⇒ cset × cfunc ⇒ bool" where
  "reflexive_on X R = (R ⊆c X×cX ∧ 
    (∀x. x ∈c X ⟶ (⟨x,x⟩ ∈⇘X×cX⇙ R)))"

definition symmetric_on :: "cset ⇒ cset × cfunc ⇒ bool" where
  "symmetric_on X R = (R  ⊆c X×cX ∧
    (∀x y. x ∈c X ∧  y ∈c X ⟶ 
      (⟨x,y⟩ ∈⇘X×cX⇙ R ⟶ ⟨y,x⟩ ∈⇘X×cX⇙ R)))" 

definition transitive_on :: "cset ⇒ cset × cfunc ⇒ bool" where
  "transitive_on X R = (R  ⊆c X×cX ∧
    (∀x y z. x ∈c X ∧  y ∈c X ∧ z ∈c X  ⟶
      (⟨x,y⟩ ∈⇘X×cX⇙ R ∧ ⟨y,z⟩ ∈⇘X×cX⇙ R ⟶ ⟨x,z⟩ ∈⇘X×cX⇙ R)))"

definition equiv_rel_on :: "cset ⇒ cset × cfunc ⇒ bool" where
  "equiv_rel_on X R  ⟷ (reflexive_on X R ∧ symmetric_on X R ∧ transitive_on X R)"

definition const_on_rel :: "cset ⇒ cset × cfunc ⇒ cfunc ⇒ bool" where
  "const_on_rel X R f = (∀x y. x ∈c X ⟶ y ∈c X ⟶ ⟨x, y⟩ ∈⇘X×cX⇙ R ⟶ f ∘c x = f ∘c y)"

lemma reflexive_def2:
  assumes reflexive_Y: "reflexive_on X (Y, m)"
  assumes x_type: "x ∈c X" 
  shows "∃y. y ∈c Y ∧  m ∘c y = ⟨x,x⟩"
  using assms unfolding reflexive_on_def relative_member_def factors_through_def2
proof -
    assume a1: "(Y, m) ⊆c X ×c X ∧ (∀x. x ∈c X ⟶ ⟨x,x⟩ ∈c X ×c X ∧ monomorphism (snd (Y, m)) ∧ snd (Y, m) : fst (Y, m) → X ×c X ∧ ⟨x,x⟩ factorsthru snd (Y, m))"
    have xx_type: "⟨x,x⟩ ∈c X ×c X"
      by (typecheck_cfuncs, simp add: x_type)
    have "⟨x,x⟩ factorsthru m"
      using a1 x_type by auto
    then show ?thesis
      using a1 xx_type cfunc_type_def factors_through_def subobject_of_def2 by force
qed

lemma symmetric_def2:
  assumes symmetric_Y: "symmetric_on X (Y, m)"
  assumes x_type: "x ∈c X"
  assumes y_type: "y ∈c X"
  assumes relation: "∃v. v ∈c Y ∧  m ∘c v = ⟨x,y⟩"
  shows "∃w. w ∈c Y ∧  m ∘c w = ⟨y,x⟩"
  using assms unfolding symmetric_on_def relative_member_def factors_through_def2
  by (metis cfunc_prod_type factors_through_def2 fst_conv snd_conv subobject_of_def2)

lemma transitive_def2:
  assumes transitive_Y: "transitive_on X (Y, m)"
  assumes x_type: "x ∈c X"
  assumes y_type: "y ∈c X"
  assumes z_type: "z ∈c X"
  assumes relation1: "∃v. v ∈c Y ∧  m ∘c v = ⟨x,y⟩"
  assumes relation2: "∃w. w ∈c Y ∧  m ∘c w = ⟨y,z⟩"
  shows "∃u. u ∈c Y ∧  m ∘c u = ⟨x,z⟩"
  using assms unfolding transitive_on_def relative_member_def factors_through_def2
  by (metis cfunc_prod_type factors_through_def2 fst_conv snd_conv subobject_of_def2)

text ‹The lemma below corresponds to Exercise 2.3.3 in Halvorson.›
lemma kernel_pair_equiv_rel:
  assumes "f : X → Y"
  shows "equiv_rel_on X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
proof (unfold equiv_rel_on_def, safe)
  show "reflexive_on X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
  proof (unfold reflexive_on_def, safe)
    show "(X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) ⊆c X ×c X"
      using assms kernel_pair_subset by auto
  next
    fix x
    assume x_type: "x ∈c X"
    then show "⟨x,x⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
      by (smt (z3) assms comp_type diag_on_elements diagonal_type fibered_product_morphism_monomorphism
          fibered_product_morphism_type pair_factorsthru_fibered_product_morphism relative_member_def2)
  qed

  show "symmetric_on X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
  proof (unfold symmetric_on_def, safe)
    show "(X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) ⊆c X ×c X"
      using assms kernel_pair_subset by auto
  next 
    fix x y
    assume x_type: "x ∈c X" and y_type: "y ∈c X"
    assume xy_in: "⟨x,y⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    then have "f ∘c x = f ∘c y"
      using assms fibered_product_pair_member x_type y_type by blast
    
    then show "⟨y,x⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
      using assms fibered_product_pair_member x_type y_type by auto
  qed

  show "transitive_on X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
  proof (unfold transitive_on_def, safe)
    show "(X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) ⊆c X ×c X"
      using assms kernel_pair_subset by auto
  next 
    fix x y z 
    assume x_type: "x ∈c X" and y_type: "y ∈c X" and z_type: "z ∈c X"
    assume xy_in: "⟨x,y⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    assume yz_in: "⟨y,z⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"

    have eqn1: "f ∘c x = f ∘c y"
      using assms fibered_product_pair_member x_type xy_in y_type by blast

    have eqn2: "f ∘c y = f ∘c z"
      using assms fibered_product_pair_member y_type yz_in z_type by blast

    show "⟨x,z⟩ ∈⇘X ×c X⇙ (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
      using assms eqn1 eqn2 fibered_product_pair_member x_type z_type by auto
  qed
qed

text ‹The axiomatization below corresponds to Axiom 6 (Equivalence Classes) in Halvorson.›
axiomatization 
  quotient_set :: "cset ⇒ (cset × cfunc) ⇒ cset" (infix "⫽" 50) and
  equiv_class :: "cset × cfunc ⇒ cfunc" and
  quotient_func :: "cfunc ⇒ cset × cfunc ⇒ cfunc"
where
  equiv_class_type[type_rule]: "equiv_rel_on X R ⟹ equiv_class R : X → quotient_set X R" and
  equiv_class_eq: "equiv_rel_on X R ⟹ ⟨x, y⟩ ∈c X×cX ⟹
    ⟨x, y⟩ ∈⇘X×cX⇙ R ⟷ equiv_class R ∘c x = equiv_class R ∘c y" and
  quotient_func_type[type_rule]: 
    "equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
      quotient_func f R : quotient_set X R → Y" and 
  quotient_func_eq: "equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
     quotient_func f R ∘c equiv_class R = f" and  
  quotient_func_unique: "equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
    h : quotient_set X R → Y ⟹ h ∘c equiv_class R = f ⟹ h = quotient_func f R"
text ‹Note that @{const quotient_set} corresponds to $X/R$, @{const equiv_class} corresponds to the
  canonical quotient mapping $q$, and @{const quotient_func} corresponds to $\bar{f}$ in Halvorson's
  formulation of this axiom.›

abbreviation equiv_class' :: "cfunc ⇒ cset × cfunc ⇒ cfunc" ("[_]⇘_⇙") where
  "[x]⇘R⇙ ≡ equiv_class R ∘c x"

subsection ‹Coequalizers›

text ‹The definition below corresponds to a comment after Axiom 6 (Equivalence Classes) in Halvorson.›
definition coequalizer :: "cset ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ bool" where
  "coequalizer E m f g ⟷ (∃ X Y. (f : Y → X) ∧ (g : Y → X) ∧ (m : X → E)
    ∧ (m ∘c f = m ∘c g)
    ∧ (∀ h F. ((h : X → F) ∧ (h ∘c f = h ∘c g)) ⟶ (∃! k. (k : E → F) ∧ k ∘c m = h)))"

lemma coequalizer_def2:
  assumes "f : Y → X" "g : Y → X" "m : X → E"
  shows "coequalizer E m f g ⟷
    (m ∘c f = m ∘c g)
      ∧ (∀ h F. ((h : X → F) ∧ (h ∘c f = h ∘c g)) ⟶ (∃! k. (k : E → F) ∧ k ∘c m = h))"
  using assms unfolding coequalizer_def cfunc_type_def by auto

text ‹The lemma below corresponds to Exercise 2.3.1 in Halvorson.›
lemma coequalizer_unique:
  assumes "coequalizer E m f g" "coequalizer F n f g"
  shows "E ≅ F"
proof - 
  obtain k where k_def: "k: E → F ∧ k ∘c m =  n"
     by (typecheck_cfuncs, metis assms cfunc_type_def coequalizer_def)
  obtain k' where k'_def: "k': F → E ∧ k' ∘c n =  m"
     by (typecheck_cfuncs, metis assms cfunc_type_def coequalizer_def)
  obtain k'' where k''_def: "k'': F → F ∧ k'' ∘c n =  n"
    by (typecheck_cfuncs, smt (verit) assms(2)  cfunc_type_def coequalizer_def)

  have k''_def2: "k'' = id F"
    using assms(2) coequalizer_def id_left_unit2 k''_def by (typecheck_cfuncs, blast)
  have kk'_idF: "k ∘c k' = id F"
    by (typecheck_cfuncs, smt (verit) assms(2) cfunc_type_def coequalizer_def comp_associative k''_def k''_def2 k'_def k_def)
  have k'k_idE: "k' ∘c k = id E"
    by (typecheck_cfuncs, smt (verit) assms(1) coequalizer_def comp_associative2 id_left_unit2 k'_def k_def)

  show "E ≅ F"
    using cfunc_type_def is_isomorphic_def isomorphism_def k'_def k'k_idE k_def kk'_idF by fastforce
qed

text ‹The lemma below corresponds to Exercise 2.3.2 in Halvorson.›
lemma coequalizer_is_epimorphism:
  "coequalizer E m f g ⟹  epimorphism(m)"
  unfolding coequalizer_def epimorphism_def
proof clarify
  fix k h X Y
  assume f_type: "f : Y → X"
  assume g_type: "g : Y → X"
  assume m_type: "m : X → E"
  assume fm_gm: "m ∘c f = m ∘c g"
  assume uniqueness: "∀h F. h : X → F ∧ h ∘c f = h ∘c g ⟶ (∃!k. k : E → F ∧ k ∘c m = h)"
  assume relation_k: "domain k =codomain m "
  assume relation_h: "domain h = codomain m" 
  assume m_k_mh: "k ∘c m = h ∘c m" 

  have "k ∘c m ∘c f = h ∘c m ∘c g"
    using cfunc_type_def comp_associative fm_gm g_type m_k_mh m_type relation_k relation_h by auto

  then obtain z where "z: E → codomain(k) ∧ z ∘c m  = k ∘c m ∧
    (∀ j. j:E → codomain(k) ∧  j ∘c m = k ∘c m ⟶ j = z)"
    using uniqueness by (smt (z3) cfunc_type_def codomain_comp comp_associative domain_comp f_type g_type m_k_mh m_type relation_k relation_h)

  then show "k = h"
    by (metis cfunc_type_def codomain_comp m_k_mh m_type relation_k relation_h)
qed

lemma canonical_quotient_map_is_coequalizer:
  assumes "equiv_rel_on X (R,m)"
  shows "coequalizer (X ⫽ (R,m)) (equiv_class (R,m))
                     (left_cart_proj X X ∘c m) (right_cart_proj X X ∘c m)"
  unfolding coequalizer_def 
proof(rule exI[where x=X], intro exI[where x= R], safe)
  have m_type: "m: R → X ×c X"
    using assms equiv_rel_on_def subobject_of_def2 transitive_on_def by blast
  show "left_cart_proj X X ∘c m : R → X"
    using m_type by typecheck_cfuncs
  show "right_cart_proj X X ∘c m : R → X"
    using m_type by typecheck_cfuncs
  show "equiv_class (R, m) : X → X ⫽ (R, m)"
    by (simp add: assms equiv_class_type)
  show "[left_cart_proj X X ∘c m]⇘(R, m)⇙ = [right_cart_proj X X ∘c m]⇘(R, m)⇙"
  proof(rule one_separator[where X="R", where Y = "X ⫽ (R,m)"], typecheck_cfuncs)
    show "[left_cart_proj X X ∘c m]⇘(R, m)⇙ : R → X ⫽ (R, m)"
      using m_type assms by typecheck_cfuncs
    show "[right_cart_proj X X ∘c m]⇘(R, m)⇙ : R → X ⫽ (R, m)"
      using m_type assms by typecheck_cfuncs
  next
    fix x 
    assume x_type: "x ∈c R"
    then have m_x_type: "m ∘c x ∈c X ×c X"
      using m_type by typecheck_cfuncs
    then obtain a b where a_type: "a ∈c X" and b_type: "b ∈c X" and m_x_eq: "m ∘c x = ⟨a,b⟩"
      using cart_prod_decomp by blast
    then have ab_inR_relXX: "⟨a,b⟩ ∈⇘X ×c X⇙(R,m)"
      using assms cfunc_type_def equiv_rel_on_def factors_through_def m_x_type reflexive_on_def relative_member_def2 x_type by auto
    then have "equiv_class (R, m) ∘c a = equiv_class (R, m) ∘c b"
      using equiv_class_eq assms relative_member_def by blast
    then have "equiv_class (R, m) ∘c left_cart_proj X X ∘c ⟨a,b⟩ = equiv_class (R, m) ∘c right_cart_proj X X ∘c ⟨a,b⟩"
      using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by auto
    then have "equiv_class (R, m) ∘c left_cart_proj X X ∘c m ∘c x = equiv_class (R, m) ∘c right_cart_proj X X ∘c m ∘c x"
      by (simp add: m_x_eq)
    then show "[left_cart_proj X X ∘c m]⇘(R, m)⇙ ∘c x = [right_cart_proj X X ∘c m]⇘(R, m)⇙ ∘c x"
      using x_type m_type assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative m_x_eq)
  qed   
next
  fix h F 
  assume h_type: " h : X → F"
  assume h_proj1_eqs_h_proj2: "h ∘c left_cart_proj X X ∘c m = h ∘c right_cart_proj X X ∘c m"

  have m_type: "m : R → X ×c X"
    using assms equiv_rel_on_def reflexive_on_def subobject_of_def2 by blast
  have "const_on_rel X (R, m) h"
  proof (unfold const_on_rel_def, clarify)
    fix x y
    assume x_type: "x ∈c X" and y_type: "y ∈c X"
    assume "⟨x,y⟩ ∈⇘X ×c X⇙ (R, m)"
    then obtain xy where xy_type: "xy ∈c R" and m_h_eq: "m ∘c xy = ⟨x,y⟩"
      unfolding relative_member_def2 factors_through_def using cfunc_type_def by auto

    have "h ∘c left_cart_proj X X ∘c m ∘c xy = h ∘c right_cart_proj X X ∘c m ∘c xy"
      using h_type m_type xy_type by (typecheck_cfuncs, smt comp_associative2 comp_type h_proj1_eqs_h_proj2)
    then have "h ∘c left_cart_proj X X ∘c ⟨x,y⟩ = h ∘c right_cart_proj X X ∘c ⟨x,y⟩"
      using m_h_eq by auto
    then show "h ∘c x = h ∘c y"
      using left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod x_type y_type by auto
  qed
  then show "∃k. k : X ⫽ (R, m) → F ∧ k ∘c equiv_class (R, m) = h"
    using assms h_type quotient_func_type quotient_func_eq
    by (intro exI[where x="quotient_func h (R, m)"], safe)
next
  fix F k y
  assume k_type[type_rule]: "k : X ⫽ (R, m) → F"
  assume y_type[type_rule]: "y : X ⫽ (R, m) → F"
  assume k_equiv_class_type[type_rule]: "k ∘c equiv_class (R, m) : X → F"
  assume k_equiv_class_eq: "(k ∘c equiv_class (R, m)) ∘c left_cart_proj X X ∘c m =
       (k ∘c equiv_class (R, m)) ∘c right_cart_proj X X ∘c m"
  assume y_k_eq: "y ∘c equiv_class (R, m) = k ∘c equiv_class (R, m)"

  have m_type[type_rule]: "m : R → X ×c X"
    using assms equiv_rel_on_def reflexive_on_def subobject_of_def2 by blast

  have y_eq: "y = quotient_func (y ∘c equiv_class (R, m)) (R, m)"
    using assms y_k_eq
  proof (etcs_rule quotient_func_unique[where X=X, where Y=F], unfold const_on_rel_def, safe)
    fix a b
    assume a_type[type_rule]: "a ∈c X" and b_type[type_rule]: "b ∈c X"
    assume ab_in_R: "⟨a,b⟩ ∈⇘X ×c X⇙ (R, m)"
    then obtain h where h_type[type_rule]: "h ∈c R" and m_h_eq: "m ∘c h = ⟨a, b⟩"
      unfolding relative_member_def factors_through_def using cfunc_type_def by auto 

    have "(k ∘c equiv_class (R, m)) ∘c left_cart_proj X X ∘c m ∘c h =
       (k ∘c equiv_class (R, m)) ∘c right_cart_proj X X ∘c m ∘c h"
      using assms 
      by (typecheck_cfuncs, smt comp_associative2 comp_type k_equiv_class_eq)
    then have "(k ∘c equiv_class (R, m)) ∘c left_cart_proj X X ∘c ⟨a, b⟩ =
       (k ∘c equiv_class (R, m)) ∘c right_cart_proj X X ∘c ⟨a, b⟩"
      by (simp add: m_h_eq)
    then show "(y ∘c equiv_class (R, m)) ∘c a = (y ∘c equiv_class (R, m)) ∘c b"
      using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_k_eq by auto
  qed

  have k_eq: "k = quotient_func (y ∘c equiv_class (R, m)) (R, m)"
    using assms sym[OF y_k_eq]
  proof (etcs_rule quotient_func_unique[where X=X, where Y=F], unfold const_on_rel_def, safe)
    fix a b
    assume a_type: "a ∈c X" and b_type: "b ∈c X"
    assume ab_in_R: "⟨a,b⟩ ∈⇘X ×c X⇙ (R, m)"
    then obtain h where h_type: "h ∈c R" and m_h_eq: "m ∘c h = ⟨a, b⟩"
      unfolding relative_member_def factors_through_def using cfunc_type_def by auto 
    
    have "(k ∘c equiv_class (R, m)) ∘c left_cart_proj X X ∘c m ∘c h =
       (k ∘c equiv_class (R, m)) ∘c right_cart_proj X X ∘c m ∘c h"
      using k_type m_type h_type assms 
      by (typecheck_cfuncs, smt comp_associative2 comp_type k_equiv_class_eq)
    then have "(k ∘c equiv_class (R, m)) ∘c left_cart_proj X X ∘c ⟨a, b⟩ =
       (k ∘c equiv_class (R, m)) ∘c right_cart_proj X X ∘c ⟨a, b⟩"
      by (simp add: m_h_eq)
    then show "(y ∘c equiv_class (R, m)) ∘c a = (y ∘c equiv_class (R, m)) ∘c b"
      using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_k_eq by auto
  qed
  show "k = y"
    using y_eq k_eq by auto
qed

lemma canonical_quot_map_is_epi:
  assumes "equiv_rel_on X (R,m)"
  shows "epimorphism((equiv_class (R,m)))"
  by (meson assms canonical_quotient_map_is_coequalizer coequalizer_is_epimorphism)

subsection  ‹Regular Epimorphisms›

text ‹The definition below corresponds to Definition 2.3.4 in Halvorson.›
definition regular_epimorphism :: "cfunc ⇒ bool" where
  "regular_epimorphism f = (∃ g h. coequalizer (codomain f) f g h)"

text ‹The lemma below corresponds to Exercise 2.3.5 in Halvorson.›
lemma reg_epi_and_mono_is_iso:
  assumes "f : X → Y" "regular_epimorphism f" "monomorphism f"
  shows "isomorphism f"
proof -   
  obtain g h where gh_def: "coequalizer (codomain f) f g h"
    using assms(2) regular_epimorphism_def by auto
  obtain W where W_def: "(g: W → X) ∧ (h: W → X) ∧ (coequalizer Y f g h)"
    using assms(1) cfunc_type_def coequalizer_def gh_def by fastforce
  have fg_eqs_fh: "f ∘c g = f ∘c h"
    using coequalizer_def gh_def by blast    
  then have "id(X)∘c g = id(X) ∘c  h"
    using W_def assms(1,3) monomorphism_def2 by blast     
  then obtain j where j_def: "j: Y → X ∧ j ∘c f =  id(X)"
    using assms(1)  W_def  coequalizer_def2 by (typecheck_cfuncs, blast)
  have "id(Y) ∘c f = f ∘c id(X)"
    using assms(1) id_left_unit2 id_right_unit2 by auto
  also have "... = (f ∘c j) ∘c f"
     using assms(1) comp_associative2 j_def by fastforce
  ultimately have "id(Y) = f ∘c j"
    by (typecheck_cfuncs, metis W_def assms(1) coequalizer_is_epimorphism epimorphism_def3 j_def)
  then show "isomorphism f"
    using  assms(1) cfunc_type_def isomorphism_def j_def by fastforce  
qed

text ‹The two lemmas below correspond to Proposition 2.3.6 in Halvorson.›
lemma epimorphism_coequalizer_kernel_pair:
  assumes "f : X → Y" "epimorphism f"
  shows "coequalizer Y f (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)"
  unfolding coequalizer_def
proof (rule exI[where x = X], rule exI[where x="X ⇘f⇙×c⇘f⇙ X"], safe)
  show "fibered_product_left_proj X f f X : X ⇘f⇙×c⇘f⇙ X → X"
    using assms by typecheck_cfuncs
  show "fibered_product_right_proj X f f X : X ⇘f⇙×c⇘f⇙ X → X"
    using assms by typecheck_cfuncs
  show "f : X →Y"
    using assms by typecheck_cfuncs
  show "f ∘c fibered_product_left_proj X f f X = f ∘c fibered_product_right_proj X f f X"
    using fibered_product_is_pullback assms unfolding is_pullback_def by auto
next
  fix g E
  assume g_type: "g : X → E"
  assume g_eq: "g ∘c fibered_product_left_proj X f f X = g ∘c fibered_product_right_proj X f f X"

  define  F where F_def: "F = quotient_set X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
  obtain  q where q_def: "q = equiv_class (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)" and
  q_type[type_rule]: "q : X → F"
    using F_def assms(1) equiv_class_type kernel_pair_equiv_rel by auto
  obtain  f_bar where f_bar_def: "f_bar = quotient_func f (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)" and
  f_bar_type[type_rule]: "f_bar : F → Y" 
    using F_def assms(1) const_on_rel_def fibered_product_pair_member kernel_pair_equiv_rel quotient_func_type by auto
  have fibr_proj_left_type[type_rule]: "fibered_product_left_proj F (f_bar) (f_bar) F : F ⇘(f_bar)⇙×c⇘(f_bar)⇙ F → F"
    by typecheck_cfuncs
  have fibr_proj_right_type[type_rule]: "fibered_product_right_proj F (f_bar) (f_bar) F : F ⇘(f_bar)⇙×c⇘(f_bar)⇙ F → F"
    by typecheck_cfuncs
  (*Outline*)
  (* show f_bar is iso using argument from the bottom of page 43, with g = q (axiom 6's q) and m = f_bar *)
    (* b : X f×cf X → F m×cm F exists because fibered_product_morphism X f f X is an equalizer *)
    (* b exists and is an epimorphism by kernel_pair_connection *)
    (* also have "fibered_product_left_proj E m m E ∘c b = fibered_product_right_proj E m m E ∘c b" *)
    (* then "fibered_product_left_proj E m m E = fibered_product_right_proj E m m E", since b is epi *)
    (* then m is a monomorphism by kern_pair_proj_iso_TFAE2 *)
    (* but m is also an epimorphism since f = m ∘c g and f and g are epi, by comp_epi_imp_epi *)
    (* so m = f_bar is an isomorphism by epi_mon_is_iso *)
  (* take g_bar : F → E and the inverse of f_bar to satisfy the required thesis *)
  have f_eqs: "f_bar ∘c q = f"
    proof - 
      have fact1: "equiv_rel_on X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
        by (meson assms(1) kernel_pair_equiv_rel)
      have fact2: "const_on_rel X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) f"
        using assms(1) const_on_rel_def fibered_product_pair_member by presburger
      show ?thesis
        using assms(1) f_bar_def fact1 fact2 q_def quotient_func_eq by blast
  qed

  have "∃! b. b : X ⇘f⇙×c⇘f⇙ X → F ⇘(f_bar)⇙×c⇘(f_bar)⇙ F ∧
    fibered_product_left_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_left_proj X f f X ∧
    fibered_product_right_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_right_proj X f f X ∧
    epimorphism b"
  proof(rule kernel_pair_connection[where Y = Y])
    show "f : X → Y"
      using assms by typecheck_cfuncs
    show "q : X → F"
      by typecheck_cfuncs
    show "epimorphism q"
      using assms(1) canonical_quot_map_is_epi kernel_pair_equiv_rel q_def by blast
    show "f_bar ∘c q = f"
      by (simp add: f_eqs)
    show "q ∘c fibered_product_left_proj X f f X = q ∘c fibered_product_right_proj X f f X"
      by (metis assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def)
    show "f_bar : F → Y" 
      by typecheck_cfuncs
  qed

  (* b exists and is an epimorphism by kernel_pair_connection *)
  (* also have "fibered_product_left_proj E m m E ∘c b = fibered_product_right_proj E m m E ∘c b" *)
  then obtain b where b_type[type_rule]: "b : X ⇘f⇙×c⇘f⇙ X → F ⇘(f_bar)⇙×c⇘(f_bar)⇙ F" and
   left_b_eqs: "fibered_product_left_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_left_proj X f f X" and
   right_b_eqs:  "fibered_product_right_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_right_proj X f f X" and
   epi_b: "epimorphism b"
    by auto

 (* then "fibered_product_left_proj E m m E = fibered_product_right_proj E m m E", since b is epi *)
  have "fibered_product_left_proj F (f_bar) (f_bar) F = fibered_product_right_proj F (f_bar) (f_bar) F"
  proof - 
    have "(fibered_product_left_proj F (f_bar) (f_bar) F) ∘c b = q ∘c fibered_product_left_proj X f f X"
      by (simp add: left_b_eqs)
    also have "... = q ∘c fibered_product_right_proj X f f X"
      using assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
    also have "... = fibered_product_right_proj F (f_bar) (f_bar) F ∘c b"
      by (simp add: right_b_eqs)
    finally have "fibered_product_left_proj F (f_bar) (f_bar) F ∘c b = fibered_product_right_proj F (f_bar) (f_bar) F ∘c b".
    then show ?thesis
      using b_type epi_b epimorphism_def2 fibr_proj_left_type fibr_proj_right_type by blast
  qed

  (* b exists and is an epimorphism by kernel_pair_connection *)
  (* also have "fibered_product_left_proj E m m E ∘c b = fibered_product_right_proj E m m E ∘c b" *)
  then obtain b where b_type[type_rule]: "b : X ⇘f⇙×c⇘f⇙ X → F ⇘(f_bar)⇙×c⇘(f_bar)⇙ F" and
   left_b_eqs: "fibered_product_left_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_left_proj X f f X" and
   right_b_eqs:  "fibered_product_right_proj F (f_bar) (f_bar) F ∘c b = q ∘c fibered_product_right_proj X f f X" and
   epi_b: "epimorphism b"
    using b_type epi_b left_b_eqs right_b_eqs by blast
  
 (* then "fibered_product_left_proj E m m E = fibered_product_right_proj E m m E", since b is epi *)
  have "fibered_product_left_proj F (f_bar) (f_bar) F = fibered_product_right_proj F (f_bar) (f_bar) F"
  proof - 
    have "(fibered_product_left_proj F (f_bar) (f_bar) F) ∘c b = q ∘c fibered_product_left_proj X f f X"
      by (simp add: left_b_eqs)
    also have "... = q ∘c fibered_product_right_proj X f f X"
      using assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
    also have "... = fibered_product_right_proj F (f_bar) (f_bar) F ∘c b"
      by (simp add: right_b_eqs)
    finally have "fibered_product_left_proj F (f_bar) (f_bar) F ∘c b = fibered_product_right_proj F (f_bar) (f_bar) F ∘c b".
    then show ?thesis
      using b_type epi_b epimorphism_def2 fibr_proj_left_type fibr_proj_right_type by blast
  qed
  (* then m = f_bar is a monomorphism by kern_pair_proj_iso_TFAE2 *)
  then have mono_fbar: "monomorphism(f_bar)"
    by (typecheck_cfuncs, simp add:  kern_pair_proj_iso_TFAE2)
  (* but m = f_bar is also an epimorphism since f = m ∘c g and f and g = q are epi, by comp_epi_imp_epi *)
  have "epimorphism(f_bar)"
    by (typecheck_cfuncs, metis assms(2) cfunc_type_def comp_epi_imp_epi f_eqs q_type)
  (* so m = f_bar is an isomorphism by epi_mon_is_iso *)
  then have "isomorphism(f_bar)"
    by (simp add: epi_mon_is_iso mono_fbar)

  (* take  g_bar : F → E and the inverse of f_bar to satisfy the required thesis *)
  (* Recall that f_bar : F → Y"*)

  obtain f_bar_inv where f_bar_inv_type[type_rule]: "f_bar_inv: Y → F" and
                            f_bar_inv_eq1: "f_bar_inv ∘c f_bar = id(F)" and  
                            f_bar_inv_eq2: "f_bar ∘c f_bar_inv = id(Y)"
    using ‹isomorphism f_bar› cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)
  
  obtain g_bar where g_bar_def: "g_bar = quotient_func g (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    by auto
  have "const_on_rel X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) g"
    unfolding const_on_rel_def 
    by (meson assms(1) fibered_product_pair_member2 g_eq g_type)
  then have g_bar_type[type_rule]: "g_bar : F → E"
    using F_def assms(1) g_bar_def g_type kernel_pair_equiv_rel quotient_func_type by blast
  obtain k where k_def: "k = g_bar ∘c f_bar_inv" and k_type[type_rule]: "k : Y → E"
    by (typecheck_cfuncs, simp) 
  then show "∃k. k : Y → E ∧ k ∘c f = g"
    by (smt (z3) ‹const_on_rel X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) g› assms(1) comp_associative2 f_bar_inv_eq1 f_bar_inv_type f_bar_type f_eqs g_bar_def g_bar_type g_type id_left_unit2 kernel_pair_equiv_rel q_def q_type quotient_func_eq)
next
  show "⋀F k y.
       k ∘c f : X → F ⟹
       (k ∘c f) ∘c fibered_product_left_proj X f f X = (k ∘c f) ∘c fibered_product_right_proj X f f X ⟹
       k : Y → F ⟹ y : Y → F ⟹ y ∘c f = k ∘c f ⟹ k = y"
    using assms epimorphism_def2 by blast
qed

lemma epimorphisms_are_regular:
  assumes "f : X → Y" "epimorphism f"
  shows "regular_epimorphism f"
  by (meson assms(2) cfunc_type_def epimorphism_coequalizer_kernel_pair regular_epimorphism_def)

subsection ‹Epi-monic Factorization›

lemma epi_monic_factorization:
  assumes f_type[type_rule]: "f : X → Y"
  shows "∃ g m E. g : X → E ∧ m : E → Y 
    ∧ coequalizer E g (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)
    ∧ monomorphism m ∧ f = m ∘c g
    ∧ (∀x. x : E → Y ⟶ f = x ∘c g ⟶ x = m)"
proof -
  obtain q where q_def: "q = equiv_class (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    by auto
  obtain E where E_def: "E = quotient_set X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    by auto
  obtain m where m_def: "m = quotient_func f (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X)"
    by auto
  show "∃ g m E. g : X → E ∧ m : E → Y 
    ∧ coequalizer E g (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)
    ∧ monomorphism m ∧ f = m ∘c g
    ∧ (∀x. x : E → Y ⟶ f = x ∘c g ⟶ x = m)"
  proof (rule exI[where x=q], rule exI [where x=m], rule exI[where x=E], safe)
    show q_type[type_rule]: "q : X → E"
      unfolding q_def E_def using kernel_pair_equiv_rel by (typecheck_cfuncs, blast)
    
    have f_const: "const_on_rel X (X ⇘f⇙×c⇘f⇙ X, fibered_product_morphism X f f X) f"
      unfolding const_on_rel_def using assms fibered_product_pair_member by auto
    then show m_type[type_rule]: "m : E → Y"
      unfolding m_def E_def using kernel_pair_equiv_rel by (typecheck_cfuncs, blast)
    
    show q_coequalizer: "coequalizer E q (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)"
      unfolding q_def fibered_product_left_proj_def fibered_product_right_proj_def E_def
      using canonical_quotient_map_is_coequalizer f_type kernel_pair_equiv_rel by auto 
    then have q_epi: "epimorphism q"
      using coequalizer_is_epimorphism by auto 

    show m_mono: "monomorphism m"
    proof -
      have q_eq: "q ∘c fibered_product_left_proj X f f X = q ∘c fibered_product_right_proj X f f X"
        using canonical_quotient_map_is_coequalizer coequalizer_def f_type fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
      then have "∃!b. b : X ⇘f⇙×c⇘f⇙ X → E ⇘m⇙×c⇘m⇙ E ∧
        fibered_product_left_proj E m m E ∘c b = q ∘c fibered_product_left_proj X f f X ∧
        fibered_product_right_proj E m m E ∘c b = q ∘c fibered_product_right_proj X f f X ∧
        epimorphism b"
        by (typecheck_cfuncs, intro kernel_pair_connection,
            simp_all add: q_epi, metis f_const kernel_pair_equiv_rel m_def q_def quotient_func_eq)
      then obtain b where b_type[type_rule]: "b : X ⇘f⇙×c⇘f⇙ X → E ⇘m⇙×c⇘m⇙ E" and
        b_left_eq: "fibered_product_left_proj E m m E ∘c b = q ∘c fibered_product_left_proj X f f X" and
        b_right_eq: "fibered_product_right_proj E m m E ∘c b = q ∘c fibered_product_right_proj X f f X" and
        b_epi: "epimorphism b"
        by auto

      have "fibered_product_left_proj E m m E ∘c b = fibered_product_right_proj E m m E ∘c b"
        using b_left_eq b_right_eq q_eq by force
      then have "fibered_product_left_proj E m m E = fibered_product_right_proj E m m E"
        using b_epi cfunc_type_def epimorphism_def by (typecheck_cfuncs_prems, auto)
      then show "monomorphism m"
        using kern_pair_proj_iso_TFAE2 m_type by auto
    qed

    show f_eq_m_q: "f = m ∘c q"
      using f_const f_type kernel_pair_equiv_rel m_def q_def quotient_func_eq by fastforce

    show "⋀x. x : E → Y ⟹ f = x ∘c q ⟹ x = m"
    proof -
      fix x
      assume x_type[type_rule]: "x : E → Y"
      assume f_eq_x_q: "f = x ∘c q"
      have "x ∘c q = m ∘c q"
        using f_eq_m_q f_eq_x_q by auto
      then show "x = m"
        using epimorphism_def2 m_type q_epi q_type x_type by blast
    qed
  qed
qed

lemma epi_monic_factorization2:
  assumes f_type[type_rule]: "f : X → Y"
  shows "∃ g m E. g : X → E ∧ m : E → Y 
    ∧ epimorphism g ∧ monomorphism m ∧ f = m ∘c g
    ∧ (∀x. x : E → Y ⟶ f = x ∘c g ⟶ x = m)"
  using epi_monic_factorization coequalizer_is_epimorphism by (meson f_type)

subsubsection  ‹Image of a Function›

text ‹The definition below corresponds to Definition 2.3.7 in Halvorson.›
definition image_of :: "cfunc ⇒ cset ⇒ cfunc ⇒ cset" ("_⦇_⦈⇘_⇙" [101,0,0]100) where
  "image_of f A n = (SOME fA. ∃g m.
   g : A → fA ∧
   m : fA → codomain f ∧
   coequalizer fA g (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
   monomorphism m ∧ f ∘c n = m ∘c g ∧ (∀x. x : fA → codomain f ⟶ f ∘c n = x ∘c g ⟶ x = m))"

lemma image_of_def2:
  assumes "f : X → Y" "n : A → X"
  shows "∃g m.
    g : A → f⦇A⦈⇘n⇙ ∧
    m : f⦇A⦈⇘n⇙ → Y ∧
    coequalizer (f⦇A⦈⇘n⇙) g (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
    monomorphism m ∧ f ∘c n = m ∘c g ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘c n = x ∘c g ⟶ x = m)"
proof -
  have "∃g m.
    g : A → f⦇A⦈⇘n⇙ ∧
    m : f⦇A⦈⇘n⇙ → codomain f ∧
    coequalizer (f⦇A⦈⇘n⇙) g (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
    monomorphism m ∧ f ∘c n = m ∘c g ∧ (∀x. x : f⦇A⦈⇘n⇙ → codomain f ⟶ f ∘c n = x ∘c g ⟶ x = m)"
    using assms cfunc_type_def comp_type epi_monic_factorization[where f="f ∘c n", where X=A, where Y="codomain f"] 
    by (unfold image_of_def, subst someI_ex, auto)
  then show ?thesis
    using assms(1) cfunc_type_def by auto
qed

definition image_restriction_mapping :: "cfunc ⇒ cset × cfunc ⇒ cfunc" ("_↾⇘_⇙" [101,0]100) where
  "image_restriction_mapping f An = (SOME g. ∃ m. g : fst An → f⦇fst An⦈⇘snd An⇙ ∧ m : f⦇fst An⦈⇘snd An⇙ → codomain f ∧
    coequalizer (f⦇fst An⦈⇘snd An⇙) g (fibered_product_left_proj (fst An) (f ∘c snd An) (f ∘c snd An) (fst An)) (fibered_product_right_proj (fst An) (f ∘c snd An) (f ∘c snd An) (fst An)) ∧
    monomorphism m ∧ f ∘c snd An = m ∘c g ∧ (∀x. x : f⦇fst An⦈⇘snd An⇙ → codomain f ⟶ f ∘c snd An = x ∘c g ⟶ x = m))"

lemma image_restriction_mapping_def2:
  assumes "f : X → Y" "n : A → X"
  shows "∃ m. f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ m : f⦇A⦈⇘n⇙ → Y ∧
    coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
    monomorphism m ∧ f ∘c n = m ∘c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘c n = x ∘c (f↾⇘(A, n)⇙) ⟶ x = m)"
proof -
  have codom_f: "codomain f = Y"
    using assms(1) cfunc_type_def by auto
  have "∃ m. f↾⇘(A, n)⇙ : fst (A, n) → f⦇fst (A, n)⦈⇘snd (A, n)⇙ ∧ m : f⦇fst (A, n)⦈⇘snd (A, n)⇙ → codomain f ∧
    coequalizer (f⦇fst (A, n)⦈⇘snd (A, n)⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj (fst (A, n)) (f ∘c snd (A, n)) (f ∘c snd (A, n)) (fst (A, n))) (fibered_product_right_proj (fst (A, n)) (f ∘c snd (A, n)) (f ∘c snd (A, n)) (fst (A, n))) ∧
    monomorphism m ∧ f ∘c snd (A, n) = m ∘c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇fst (A, n)⦈⇘snd (A, n)⇙ → codomain f ⟶ f ∘c snd (A, n) = x ∘c (f↾⇘(A, n)⇙) ⟶ x = m)"
    unfolding image_restriction_mapping_def by (rule someI_ex, insert assms image_of_def2 codom_f, auto)
  then show ?thesis
    using codom_f by simp 
qed

definition image_subobject_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc" ("[_⦇_⦈⇘_⇙]map" [101,0,0]100) where
  "[f⦇A⦈⇘n⇙]map = (THE m. f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ m : f⦇A⦈⇘n⇙ → codomain f ∧
   coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
   monomorphism m ∧ f ∘c n = m ∘c (f↾⇘(A, n)⇙) ∧ (∀x. x : (f⦇A⦈⇘n⇙) → codomain f ⟶ f ∘c n = x ∘c (f↾⇘(A, n)⇙) ⟶ x = m))"

lemma image_subobject_mapping_def2:
  assumes "f : X → Y" "n : A → X"
  shows "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ [f⦇A⦈⇘n⇙]map : f⦇A⦈⇘n⇙ → Y ∧
    coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
    monomorphism ([f⦇A⦈⇘n⇙]map) ∧ f ∘c n = [f⦇A⦈⇘n⇙]map ∘c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘c n = x ∘c (f↾⇘(A, n)⇙) ⟶ x = [f⦇A⦈⇘n⇙]map)"
proof -
  have codom_f: "codomain f = Y"
    using assms(1) cfunc_type_def by auto
  have "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ ([f⦇A⦈⇘n⇙]map) : f⦇A⦈⇘n⇙ → codomain f ∧
   coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A) ∧
   monomorphism ([f⦇A⦈⇘n⇙]map) ∧ f ∘c n = ([f⦇A⦈⇘n⇙]map) ∘c (f↾⇘(A, n)⇙) ∧ 
   (∀x. x : (f⦇A⦈⇘n⇙) → codomain f ⟶ f ∘c n = x ∘c (f↾⇘(A, n)⇙) ⟶ x = ([f⦇A⦈⇘n⇙]map))"
    unfolding image_subobject_mapping_def
    by (rule theI', insert assms codom_f image_restriction_mapping_def2, blast)
  then show ?thesis
    using codom_f by fastforce
qed

lemma image_rest_map_type[type_rule]:
  assumes "f : X → Y" "n : A → X"
  shows "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙"
  using assms image_restriction_mapping_def2 by blast

lemma image_rest_map_coequalizer:
  assumes "f : X → Y" "n : A → X"
  shows "coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘c n) (f ∘c n) A) (fibered_product_right_proj A (f ∘c n) (f ∘c n) A)"
  using assms image_restriction_mapping_def2 by blast

lemma image_rest_map_epi:
  assumes "f : X → Y" "n : A → X"
  shows "epimorphism (f↾⇘(A, n)⇙)"
  using assms image_rest_map_coequalizer coequalizer_is_epimorphism by blast 

lemma image_subobj_map_type[type_rule]:
  assumes "f : X → Y" "n : A → X"
  shows "[f⦇A⦈⇘n⇙]map : f⦇A⦈⇘n⇙ → Y"
  using assms image_subobject_mapping_def2 by blast

lemma image_subobj_map_mono:
  assumes "f : X → Y" "n : A → X"
  shows "monomorphism ([f⦇A⦈⇘n⇙]map)"
  using assms image_subobject_mapping_def2 by blast

lemma image_subobj_comp_image_rest:
  assumes "f : X → Y" "n : A → X"
  shows "[f⦇A⦈⇘n⇙]map ∘c (f↾⇘(A, n)⇙) = f ∘c n"
  using assms image_subobject_mapping_def2 by auto

lemma image_subobj_map_unique:
  assumes "f : X → Y" "n : A → X"
  shows "x : f⦇A⦈⇘n⇙ → Y ⟹ f ∘c n = x ∘c (f↾⇘(A, n)⇙) ⟹ x = [f⦇A⦈⇘n⇙]map"
  using assms image_subobject_mapping_def2 by blast

lemma image_self:
  assumes "f : X → Y" and "monomorphism f"
  assumes "a : A → X" and "monomorphism a"
  shows "f⦇A⦈⇘a⇙ ≅ A"
proof -
  have "monomorphism (f ∘c a)"
    using assms cfunc_type_def composition_of_monic_pair_is_monic by auto
  then have "monomorphism ([f⦇A⦈⇘a⇙]map ∘c (f↾⇘(A, a)⇙))"
    using assms image_subobj_comp_image_rest by auto
  then have "monomorphism (f↾⇘(A, a)⇙)"
    by (meson assms comp_monic_imp_monic' image_rest_map_type image_subobj_map_type)
  then have "isomorphism (f↾⇘(A, a)⇙)"
    using assms epi_mon_is_iso image_rest_map_epi by blast
  then have "A ≅ f⦇A⦈⇘a⇙"
    using assms unfolding is_isomorphic_def by (intro exI[where x="f↾⇘(A, a)⇙"], typecheck_cfuncs)
  then show ?thesis
    by (simp add: isomorphic_is_symmetric)
qed

text ‹The lemma below corresponds to Proposition 2.3.8 in Halvorson.›
lemma image_smallest_subobject:
  assumes f_type[type_rule]: "f : X → Y" and a_type[type_rule]: "a : A → X"
  shows "(B, n) ⊆c Y ⟹ f factorsthru n ⟹ (f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, n)"
proof -
  assume "(B, n) ⊆c Y"
  then have n_type[type_rule]: "n : B → Y" and n_mono: "monomorphism n"
    unfolding subobject_of_def2 by auto
  assume "f factorsthru n"
  then obtain g where g_type[type_rule]: "g : X → B" and f_eq_ng: "n ∘c g = f"
    using factors_through_def2 by (typecheck_cfuncs, auto)

  have fa_type[type_rule]: "f ∘c a : A → Y"
    by (typecheck_cfuncs)

  obtain p0 where p0_def[simp]: "p0 = fibered_product_left_proj A (f∘ca) (f∘ca) A"
    by auto
  obtain p1 where p1_def[simp]: "p1 = fibered_product_right_proj A (f∘ca) (f∘ca) A"
    by auto
  obtain E where E_def[simp]: "E = A ⇘f ∘c a⇙×c⇘f ∘c a⇙ A"
    by auto

  have fa_coequalizes: "(f ∘c a) ∘c p0 = (f ∘c a) ∘c p1"
    using fa_type fibered_product_proj_eq by auto
  have ga_coequalizes: "(g ∘c a) ∘c p0 = (g ∘c a) ∘c p1"
  proof -
    from fa_coequalizes have "n ∘c ((g ∘c a) ∘c p0) = n ∘c ((g ∘c a) ∘c p1)"
      by (auto, typecheck_cfuncs, auto simp add: f_eq_ng comp_associative2)
    then show "(g ∘c a) ∘c p0 = (g ∘c a) ∘c p1"
      using n_mono unfolding monomorphism_def2 by (auto, typecheck_cfuncs_prems, meson)
  qed

  have "∀h F. h : A → F ∧ h ∘c p0 = h ∘c p1 ⟶ (∃!k. k : f⦇A⦈⇘a⇙ → F ∧ k ∘c f↾⇘(A, a)⇙ = h)"
    using image_rest_map_coequalizer[where n=a] unfolding coequalizer_def 
    by (simp, typecheck_cfuncs, auto simp add: cfunc_type_def)
  then obtain k where k_type[type_rule]: "k : f⦇A⦈⇘a⇙ → B" and k_e_eq_g: "k ∘c f↾⇘(A, a)⇙ = g ∘c a"
    using ga_coequalizes by (typecheck_cfuncs, blast)

  then have "n ∘c k = [f⦇A⦈⇘a⇙]map"
    by (typecheck_cfuncs, smt (z3) comp_associative2 f_eq_ng g_type image_rest_map_type image_subobj_map_unique k_e_eq_g)
  then show "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, n)"
    unfolding relative_subset_def2
    using image_subobj_map_mono k_type n_mono by (typecheck_cfuncs, blast)
qed

lemma images_iso:
  assumes f_type[type_rule]: "f : X → Y"
  assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z" 
  shows "(f ∘c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘c n⇙"
proof -
  have f_m_image_coequalizer:
    "coequalizer ((f ∘c m)⦇A⦈⇘n⇙) ((f ∘c m)↾⇘(A, n)⇙) 
      (fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A) 
      (fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A)"
    by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)

  have f_image_coequalizer:
    "coequalizer (f⦇A⦈⇘m ∘c n⇙) (f↾⇘(A, m ∘c n)⇙) 
      (fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A) 
      (fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A)"
    by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)

  from f_m_image_coequalizer f_image_coequalizer
  show "(f ∘c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘c n⇙"
    by (meson coequalizer_unique)
qed

lemma image_subset_conv:
  assumes f_type[type_rule]: "f : X → Y"
  assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z" 
  shows "∃i. ((f ∘c m)⦇A⦈⇘n⇙, i) ⊆c B ⟹ ∃j. (f⦇A⦈⇘m ∘c n⇙, j) ⊆c B"
proof -
  assume "∃i. ((f ∘c m)⦇A⦈⇘n⇙, i) ⊆c B"
  then obtain i where
    i_type[type_rule]: "i : (f ∘c m)⦇A⦈⇘n⇙ → B" and
    i_mono: "monomorphism i"
    unfolding subobject_of_def by force

  have "(f ∘c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘c n⇙"
    using f_type images_iso m_type n_type by blast
  then obtain k where
    k_type[type_rule]: "k : f⦇A⦈⇘m ∘c n⇙ → (f ∘c m)⦇A⦈⇘n⇙" and
    k_mono: "monomorphism k"
    by (meson is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric)
  then show "∃j. (f⦇A⦈⇘m ∘c n⇙, j) ⊆c B"
    unfolding subobject_of_def using composition_of_monic_pair_is_monic i_mono
    by (intro exI[where x="i ∘c k"], typecheck_cfuncs, simp add: cfunc_type_def)
qed

lemma image_rel_subset_conv:
  assumes f_type[type_rule]: "f : X → Y"
  assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z"
  assumes rel_sub1: "((f ∘c m)⦇A⦈⇘n⇙, [(f ∘c m)⦇A⦈⇘n⇙]map) ⊆⇘Y⇙ (B,b)"
  shows "(f⦇A⦈⇘m ∘c n⇙, [f⦇A⦈⇘m ∘c n⇙]map) ⊆⇘Y⇙ (B,b)"
  using rel_sub1 image_subobj_map_mono
  unfolding relative_subset_def2
proof (typecheck_cfuncs, safe)
  fix k
  assume k_type[type_rule]: "k : (f ∘c m)⦇A⦈⇘n⇙ → B"
  assume b_type[type_rule]: "b : B → Y"
  assume b_mono: "monomorphism b"
  assume b_k_eq_map: "b ∘c k = [(f ∘c m)⦇A⦈⇘n⇙]map"

  have f_m_image_coequalizer:
    "coequalizer ((f ∘c m)⦇A⦈⇘n⇙) ((f ∘c m)↾⇘(A, n)⇙) 
      (fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A) 
      (fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A)"
    by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
  then have f_m_image_coequalises: 
      "(f ∘c m)↾⇘(A, n)⇙ ∘c fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A
        = (f ∘c m)↾⇘(A, n)⇙ ∘c fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A"
    by (typecheck_cfuncs_prems, unfold coequalizer_def2, auto)

  have f_image_coequalizer:
    "coequalizer (f⦇A⦈⇘m ∘c n⇙) (f↾⇘(A, m ∘c n)⇙) 
      (fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A) 
      (fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A)"
    by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
  then have "⋀ h F. h : A → F ⟹
           h ∘c fibered_product_left_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A =
           h ∘c fibered_product_right_proj A (f ∘c m ∘c n) (f ∘c m ∘c n) A ⟹
           (∃!k. k : f⦇A⦈⇘m ∘c n⇙ → F ∧ k ∘c f↾⇘(A, m ∘c n)⇙ = h)"
    by (typecheck_cfuncs_prems, unfold coequalizer_def2, auto)
  then have "∃!k. k : f⦇A⦈⇘m ∘c n⇙ → (f ∘c m)⦇A⦈⇘n⇙ ∧ k ∘c f↾⇘(A, m ∘c n)⇙ = (f ∘c m)↾⇘(A, n)⇙"
    using f_m_image_coequalises by (typecheck_cfuncs, presburger)
  then obtain k' where 
    k'_type[type_rule]: "k' : f⦇A⦈⇘m ∘c n⇙ → (f ∘c m)⦇A⦈⇘n⇙" and
    k'_eq: "k' ∘c f↾⇘(A, m ∘c n)⇙ = (f ∘c m)↾⇘(A, n)⇙"
    by auto

  have k'_maps_eq: "[f⦇A⦈⇘m ∘c n⇙]map = [(f ∘c m)⦇A⦈⇘n⇙]map ∘c k'"
    by (typecheck_cfuncs, smt (z3) comp_associative2 image_subobject_mapping_def2 k'_eq)
  have k_mono: "monomorphism k"
    by (metis b_k_eq_map cfunc_type_def comp_monic_imp_monic k_type rel_sub1 relative_subset_def2)
  have k'_mono: "monomorphism k'"
    by (smt (verit, ccfv_SIG) cfunc_type_def comp_monic_imp_monic comp_type f_type image_subobject_mapping_def2 k'_maps_eq k'_type m_type n_type)

  show "∃k. k : f⦇A⦈⇘m ∘c n⇙ → B ∧ b ∘c k = [f⦇A⦈⇘m ∘c n⇙]map"
    by (intro exI[where x="k ∘c k'"], typecheck_cfuncs, simp add: b_k_eq_map comp_associative2 k'_maps_eq)
qed

text ‹The lemma below corresponds to Proposition 2.3.9 in Halvorson.›
lemma subset_inv_image_iff_image_subset:
  assumes "(A,a) ⊆c X" "(B,m) ⊆c Y" 
  assumes[type_rule]: "f : X → Y"
  shows "((A, a) ⊆⇘X⇙ (f-1⦇B⦈⇘m⇙,[f-1⦇B⦈⇘m⇙]map)) = ((f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B,m))"
proof safe
  have b_mono: "monomorphism(m)"
    using assms(2) subobject_of_def2 by blast
  have b_type[type_rule]: "m : B  → Y"
    using assms(2) subobject_of_def2 by blast
  obtain m' where m'_def: "m' = [f-1⦇B⦈⇘m⇙]map"
    by blast
  then have m'_type[type_rule]: "m' : f-1⦇B⦈⇘m⇙ → X"
    using assms(3) b_mono inverse_image_subobject_mapping_type m'_def by (typecheck_cfuncs, force)

  assume "(A, a) ⊆⇘X⇙ (f-1⦇B⦈⇘m⇙, [f-1⦇B⦈⇘m⇙]map)"
  then have a_type[type_rule]: "a : A → X" and
    a_mono: "monomorphism a" and
    k_exists: "∃k. k : A → f-1⦇B⦈⇘m⇙ ∧ [f-1⦇B⦈⇘m⇙]map ∘c k = a"
    unfolding relative_subset_def2 by auto
  then obtain k where k_type[type_rule]: "k : A → f-1⦇B⦈⇘m⇙" and k_a_eq: "[f-1⦇B⦈⇘m⇙]map ∘c k = a"
    by auto

  obtain d where d_def: "d = m' ∘c k"
    by simp

  obtain j where j_def: "j = [f⦇A⦈⇘d⇙]map"
    by simp
  then have j_type[type_rule]: "j : f⦇A⦈⇘d⇙ → Y"
    using assms(3) comp_type d_def m'_type image_subobj_map_type k_type by presburger

  obtain e where e_def: "e = f↾⇘(A, d)⇙"
    by simp
  then have e_type[type_rule]: "e : A → f⦇A⦈⇘d⇙"
    using assms(3) comp_type d_def image_rest_map_type k_type m'_type by blast

  have je_equals: "j ∘c e = f ∘c m' ∘c k"
    by (typecheck_cfuncs, simp add: d_def e_def image_subobj_comp_image_rest j_def)

  have "(f ∘c m' ∘c k) factorsthru m"
  proof(typecheck_cfuncs, unfold factors_through_def2) 

    obtain middle_arrow where middle_arrow_def: 
      "middle_arrow = (right_cart_proj X B) ∘c (inverse_image_mapping f B m)"
      by simp

    then have middle_arrow_type[type_rule]: "middle_arrow : f-1⦇B⦈⇘m⇙ → B"
      unfolding middle_arrow_def using b_mono by (typecheck_cfuncs)

    show "∃h. h : A → B ∧ m ∘c h = f ∘c m' ∘c k"
      by (intro exI[where x="middle_arrow ∘c k"], typecheck_cfuncs, 
          simp add: b_mono cfunc_type_def comp_associative2 inverse_image_mapping_eq inverse_image_subobject_mapping_def m'_def middle_arrow_def)
  qed

  then have "((f ∘c m' ∘c k)⦇A⦈⇘idc A⇙, [(f ∘c m' ∘c k)⦇A⦈⇘idc A⇙]map) ⊆⇘Y⇙ (B, m)"
    by (typecheck_cfuncs, meson assms(2) image_smallest_subobject)
  then have "((f ∘c a)⦇A⦈⇘idc A⇙, [(f ∘c a)⦇A⦈⇘idc A⇙]map) ⊆⇘Y⇙ (B, m)"
    by (simp add: k_a_eq m'_def)   
  then show "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map)⊆⇘Y⇙(B, m)"
    by (typecheck_cfuncs, metis id_right_unit2 id_type image_rel_subset_conv)
next
  have m_mono: "monomorphism(m)"
    using assms(2) subobject_of_def2 by blast
  have m_type[type_rule]: "m : B  → Y"
    using assms(2) subobject_of_def2 by blast

  assume "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, m)"
  then obtain s where                                             
      s_type[type_rule]: "s : f⦇A⦈⇘a⇙ → B" and
      m_s_eq_subobj_map: "m ∘c s = [f⦇A⦈⇘a⇙]map"
    unfolding relative_subset_def2 by auto

  have a_mono: "monomorphism a"
    using assms(1) unfolding subobject_of_def2 by auto

  have pullback_map1_type[type_rule]: "s ∘c f↾⇘(A, a)⇙ : A → B"
    using assms(1) unfolding subobject_of_def2 by (auto, typecheck_cfuncs)
  have pullback_map2_type[type_rule]: "a : A → X"
    using assms(1) unfolding subobject_of_def2 by auto
  have pullback_maps_commute: "m ∘c s ∘c f↾⇘(A, a)⇙ = f ∘c a"
    by (typecheck_cfuncs, simp add: comp_associative2 image_subobj_comp_image_rest m_s_eq_subobj_map)

  have "⋀Z k h. k : Z → B ⟹ h : Z → X ⟹ m ∘c k = f ∘c h ⟹
     (∃!j. j : Z → f-1⦇B⦈⇘m⇙ ∧
           (right_cart_proj X B ∘c inverse_image_mapping f B m) ∘c j = k ∧
           (left_cart_proj X B ∘c inverse_image_mapping f B m) ∘c j = h)"
    using inverse_image_pullback assms(3) m_mono m_type unfolding is_pullback_def by simp
  then obtain k where k_type[type_rule]: "k : A → f-1⦇B⦈⇘m⇙" and
    k_right_eq: "(right_cart_proj X B ∘c inverse_image_mapping f B m) ∘c k = s ∘c f↾⇘(A, a)⇙" and
    k_left_eq: "(left_cart_proj X B ∘c inverse_image_mapping f B m) ∘c k = a"
    using pullback_map1_type pullback_map2_type pullback_maps_commute by blast

  have "monomorphism ((left_cart_proj X B ∘c inverse_image_mapping f B m) ∘c k) ⟹ monomorphism k"
    using comp_monic_imp_monic' m_mono by (typecheck_cfuncs, blast)
  then have "monomorphism k"
    by (simp add: a_mono k_left_eq)
  then show "(A, a)⊆⇘X⇙(f-1⦇B⦈⇘m⇙, [f-1⦇B⦈⇘m⇙]map)"
    unfolding relative_subset_def2 
    using assms a_mono m_mono inverse_image_subobject_mapping_mono
  proof (typecheck_cfuncs, safe)
    assume "monomorphism k"
    then show "∃k. k : A → f-1⦇B⦈⇘m⇙ ∧ [f-1⦇B⦈⇘m⇙]map ∘c k = a"
      using assms(3) inverse_image_subobject_mapping_def2 k_left_eq k_type 
      by (intro exI[where x=k], force)
  qed
qed

text ‹The lemma below corresponds to Exercise 2.3.10 in Halvorson.›
lemma in_inv_image_of_image:
  assumes "(A,m) ⊆c X" 
  assumes[type_rule]: "f : X → Y"
  shows "(A,m) ⊆⇘X⇙ (f-1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙, [f-1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙]map)"
proof -
  have m_type[type_rule]: "m : A → X"
    using assms(1) unfolding subobject_of_def2 by auto
  have m_mono: "monomorphism m"
    using assms(1) unfolding subobject_of_def2 by auto

  have "((f⦇A⦈⇘m⇙, [f⦇A⦈⇘m⇙]map) ⊆⇘Y⇙ (f⦇A⦈⇘m⇙, [f⦇A⦈⇘m⇙]map))"
    unfolding relative_subset_def2
    using m_mono image_subobj_map_mono id_right_unit2 id_type by (typecheck_cfuncs, blast)
  then show "(A,m) ⊆⇘X⇙ (f-1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙, [f-1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙]map)"
    by (meson assms relative_subset_def2 subobject_of_def2 subset_inv_image_iff_image_subset)
qed

subsection  ‹@{term distribute_left} and @{term distribute_right} as Equivalence Relations›

lemma left_pair_subset:
  assumes "m : Y → X ×c X" "monomorphism m"
  shows "(Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z)) ⊆c (X ×c Z) ×c (X ×c Z)"
  unfolding subobject_of_def2 using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix g h A
  assume g_type: "g : A → Y ×c Z"
  assume h_type: "h : A → Y ×c Z"
  assume "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c g = (distribute_right X X Z ∘c m ×f idc Z) ∘c h"
  then have "distribute_right X X Z ∘c (m ×f idc Z) ∘c g = distribute_right X X Z ∘c (m ×f idc Z) ∘c h"
    using assms g_type h_type by (typecheck_cfuncs, simp add: comp_associative2)
  then have "(m ×f idc Z) ∘c g = (m ×f idc Z) ∘c h"
    using assms g_type h_type distribute_right_mono distribute_right_type monomorphism_def2
    by (typecheck_cfuncs, blast)
  then show "g = h"
  proof -
    have "monomorphism (m ×f idc Z)"
      using assms cfunc_cross_prod_mono id_isomorphism iso_imp_epi_and_monic by (typecheck_cfuncs, blast)
    then show "(m ×f idc Z) ∘c g = (m ×f idc Z) ∘c h ⟹ g = h"
      using assms g_type h_type unfolding monomorphism_def2 by (typecheck_cfuncs, blast)
  qed
qed

lemma right_pair_subset:
  assumes "m : Y → X ×c X" "monomorphism m"
  shows "(Z ×c Y, distribute_left Z X X ∘c (idc Z ×f m)) ⊆c (Z ×c X) ×c (Z ×c X)"
  unfolding subobject_of_def2 using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix g h A
  assume g_type: "g : A → Z ×c Y"
  assume h_type: "h : A → Z ×c Y"
  assume "(distribute_left Z X X ∘c (idc Z ×f m)) ∘c g = (distribute_left Z X X ∘c (idc Z ×f m)) ∘c h"
  then have "distribute_left Z X X ∘c (idc Z ×f m) ∘c g = distribute_left Z X X ∘c (idc Z ×f m) ∘c h"
    using assms g_type h_type by (typecheck_cfuncs, simp add: comp_associative2)
  then have "(idc Z ×f m) ∘c g = (idc Z ×f m) ∘c h"
    using assms g_type h_type distribute_left_mono distribute_left_type monomorphism_def2
    by (typecheck_cfuncs, blast)
  then show "g = h"
  proof -
    have "monomorphism (idc Z ×f m)"
      using assms cfunc_cross_prod_mono id_isomorphism id_type iso_imp_epi_and_monic by blast
    then show "(idc Z ×f m) ∘c g = (idc Z ×f m) ∘c h ⟹ g = h"
      using assms g_type h_type unfolding monomorphism_def2 by (typecheck_cfuncs, blast)
  qed
qed

lemma left_pair_reflexive:
  assumes "reflexive_on X (Y, m)"
  shows "reflexive_on (X ×c Z) (Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z))"
proof (unfold reflexive_on_def, safe)
  have "m : Y → X ×c X ∧ monomorphism m"
    using assms unfolding reflexive_on_def subobject_of_def2 by auto
  then show "(Y ×c Z, distribute_right X X Z ∘c m ×f idc Z) ⊆c (X ×c Z) ×c X ×c Z"
    by (simp add: left_pair_subset)
next
  fix xz
  have m_type: "m : Y → X ×c X"
    using assms unfolding reflexive_on_def subobject_of_def2 by auto
  assume xz_type: "xz ∈c X ×c Z"
  then obtain x z where x_type: "x ∈c X" and z_type: "z ∈c Z" and xz_def: "xz = ⟨x, z⟩"
    using cart_prod_decomp by blast
  then show "⟨xz,xz⟩ ∈⇘(X ×c Z) ×c X ×c Z⇙ (Y ×c Z, distribute_right X X Z ∘c m ×f idc Z)"
    using m_type
  proof (clarify, typecheck_cfuncs, unfold relative_member_def2, safe)
    have "monomorphism m"
      using assms unfolding reflexive_on_def subobject_of_def2 by auto
    then show "monomorphism (distribute_right X X Z ∘c m ×f idc Z)"
      using  cfunc_cross_prod_mono cfunc_type_def composition_of_monic_pair_is_monic distribute_right_mono id_isomorphism iso_imp_epi_and_monic m_type by (typecheck_cfuncs, auto)
  next
    have xzxz_type: "⟨⟨x,z⟩,⟨x,z⟩⟩ ∈c (X ×c Z) ×c X ×c Z"
      using xz_type cfunc_prod_type xz_def by blast
    obtain y where y_def: "y ∈c Y" "m ∘c y = ⟨x, x⟩"
      using assms reflexive_def2 x_type by blast
    have mid_type: "m ×f idc Z : Y ×c Z → (X ×c X) ×c Z"
      by (simp add: cfunc_cross_prod_type id_type m_type)
    have dist_mid_type:"distribute_right X X Z ∘c m ×f idc Z : Y ×c Z → (X ×c Z) ×c X ×c Z"
      using comp_type distribute_right_type mid_type by force
    have yz_type: "⟨y,z⟩ ∈c Y ×c Z"
      by (typecheck_cfuncs, simp add: ‹z ∈c Z› y_def)
    have "(distribute_right X X Z ∘c m ×f idc Z) ∘c ⟨y,z⟩  = distribute_right X X Z ∘c (m ×f id(Z)) ∘c ⟨y,z⟩"
      using comp_associative2 mid_type yz_type by (typecheck_cfuncs, auto)
    also have "...  =  distribute_right X X Z ∘c  ⟨m ∘c y,id(Z) ∘c z⟩"
      using z_type cfunc_cross_prod_comp_cfunc_prod m_type y_def by (typecheck_cfuncs, auto)
    also have distxxz: "... = distribute_right X X Z ∘c  ⟨ ⟨x, x⟩, z⟩"
      using z_type id_left_unit2 y_def by auto
    also have "... = ⟨⟨x,z⟩,⟨x,z⟩⟩"
      by (meson z_type distribute_right_ap x_type)
    ultimately show "⟨⟨x,z⟩,⟨x,z⟩⟩ factorsthru (distribute_right X X Z ∘c m ×f idc Z)"
      using dist_mid_type distxxz factors_through_def2 xzxz_type yz_type by (typecheck_cfuncs, auto)
  qed
qed

lemma right_pair_reflexive:
  assumes "reflexive_on X (Y, m)"
  shows "reflexive_on (Z ×c X) (Z ×c Y, distribute_left Z X X ∘c (idc Z ×f m))"
proof (unfold reflexive_on_def, safe)
  have "m : Y → X ×c X ∧ monomorphism m"
    using assms unfolding reflexive_on_def subobject_of_def2 by auto
  then show "(Z ×c Y, distribute_left Z X X ∘c (idc Z ×f m)) ⊆c (Z ×c X) ×c Z ×c X"
    by (simp add: right_pair_subset)
  next
  fix zx
  have m_type: "m : Y → X ×c X"
    using assms unfolding reflexive_on_def subobject_of_def2 by auto
  assume zx_type: "zx ∈c Z ×c X"
  then obtain z x where x_type: "x ∈c X" and z_type: "z ∈c Z" and zx_def: "zx = ⟨z, x⟩"
    using cart_prod_decomp by blast
  then show "⟨zx,zx⟩ ∈⇘(Z ×c X) ×c Z ×c X⇙ (Z ×c Y, distribute_left Z X X  ∘c (idc Z ×f m))"
    using m_type
  proof (clarify, typecheck_cfuncs, unfold relative_member_def2, safe)
    have "monomorphism m"
      using assms unfolding reflexive_on_def subobject_of_def2 by auto
    then show "monomorphism (distribute_left Z X X  ∘c (idc Z ×f m))"
      using  cfunc_cross_prod_mono cfunc_type_def composition_of_monic_pair_is_monic distribute_left_mono id_isomorphism iso_imp_epi_and_monic m_type by (typecheck_cfuncs, auto)
  next
    have zxzx_type: "⟨⟨z,x⟩,⟨z,x⟩⟩ ∈c (Z ×c X) ×c Z ×c X"
      using zx_type cfunc_prod_type zx_def by blast
    obtain y where y_def: "y ∈c Y" "m ∘c y = ⟨x, x⟩"
      using assms reflexive_def2 x_type by blast
        have mid_type: "(idc Z ×f m) : Z ×c Y →   Z ×c (X ×c X)"
      by (simp add: cfunc_cross_prod_type id_type m_type)
    have dist_mid_type:"distribute_left Z X X  ∘c (idc Z ×f m) : Z ×c Y → (Z ×c X) ×c Z ×c X"
      using comp_type distribute_left_type mid_type by force
    have yz_type: "⟨z,y⟩ ∈c Z ×c Y"
      by (typecheck_cfuncs, simp add: ‹z ∈c Z› y_def)
    have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c ⟨z,y⟩  = distribute_left Z X X  ∘c (idc Z ×f m) ∘c ⟨z,y⟩"
      using comp_associative2 mid_type yz_type by (typecheck_cfuncs, auto)
    also have "...  =  distribute_left Z X X  ∘c  ⟨idc Z ∘c z , m ∘c y ⟩"
      using z_type cfunc_cross_prod_comp_cfunc_prod m_type y_def by (typecheck_cfuncs, auto)
    also have distxxz: "... = distribute_left Z X X  ∘c  ⟨z, ⟨x, x⟩⟩"
      using z_type id_left_unit2 y_def by auto
    also have "... = ⟨⟨z,x⟩,⟨z,x⟩⟩"
      by (meson z_type distribute_left_ap x_type)
    ultimately show "⟨⟨z,x⟩,⟨z,x⟩⟩ factorsthru (distribute_left Z X X  ∘c (idc Z ×f m))"
      using z_type distribute_left_ap x_type dist_mid_type factors_through_def2 yz_type zxzx_type by auto
  qed
qed

lemma left_pair_symmetric:
  assumes "symmetric_on X (Y, m)"
  shows "symmetric_on (X ×c Z) (Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z))"
proof (unfold symmetric_on_def, safe)
  have "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 symmetric_on_def by auto
  then show "(Y ×c Z, distribute_right X X Z ∘c m ×f idc Z) ⊆c (X ×c Z) ×c X ×c Z"
    by (simp add: left_pair_subset)
next
  have m_def[type_rule]: "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 symmetric_on_def by auto
  fix s t 
  assume s_type[type_rule]: "s ∈c X ×c Z"
  assume t_type[type_rule]: "t ∈c X ×c Z"
  assume st_relation: "⟨s,t⟩ ∈⇘(X ×c Z) ×c X ×c Z⇙ (Y ×c Z, distribute_right X X Z ∘c m ×f idc Z)"
  
  obtain sx sz where s_def[type_rule]: " sx ∈c X" "sz ∈c Z" "s =  ⟨sx,sz⟩"
    using cart_prod_decomp s_type by blast
  obtain tx tz where t_def[type_rule]: "tx ∈c X" "tz ∈c Z" "t =  ⟨tx,tz⟩"
    using cart_prod_decomp t_type by blast 

  show "⟨t,s⟩ ∈⇘(X ×c Z) ×c (X ×c Z)⇙ (Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z))" 
    using s_def t_def m_def
  proof (typecheck_cfuncs, clarify, unfold relative_member_def2, safe)
    show "monomorphism (distribute_right X X Z ∘c m ×f idc Z)"
      using relative_member_def2 st_relation by blast

    have "⟨⟨sx,sz⟩, ⟨tx,tz⟩⟩ factorsthru (distribute_right X X Z ∘c m ×f idc Z)"
      using st_relation s_def t_def unfolding relative_member_def2 by auto
    then obtain yz where yz_type[type_rule]: "yz ∈c Y ×c Z"
      and yz_def: "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c yz = ⟨⟨sx,sz⟩, ⟨tx,tz⟩⟩"
      using s_def t_def m_def by (typecheck_cfuncs, unfold factors_through_def2, auto)
    then obtain y z where
      y_type[type_rule]: "y ∈c Y" and z_type[type_rule]: "z ∈c Z" and yz_pair: "yz = ⟨y, z⟩"
      using cart_prod_decomp by blast
    then obtain my1 my2 where my_types[type_rule]: "my1 ∈c X" "my2 ∈c X" and my_def: "m ∘c y = ⟨my1,my2⟩"
      by (metis cart_prod_decomp cfunc_type_def codomain_comp domain_comp m_def(1))
    then obtain y' where y'_type[type_rule]: "y' ∈c Y" and y'_def: "m ∘c y' = ⟨my2,my1⟩"
      using assms symmetric_def2 y_type by blast

    have "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c yz = ⟨⟨my1,z⟩, ⟨my2,z⟩⟩"
    proof -
      have "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c yz = distribute_right X X Z ∘c (m ×f idc Z) ∘c ⟨y, z⟩"
        unfolding yz_pair by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = distribute_right X X Z ∘c ⟨m ∘c y, idc Z ∘c z⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
      also have "... = distribute_right X X Z ∘c ⟨⟨my1,my2⟩, z⟩"
        unfolding my_def by (typecheck_cfuncs, simp add: id_left_unit2)
      also have "... = ⟨⟨my1,z⟩, ⟨my2,z⟩⟩"
        using distribute_right_ap by (typecheck_cfuncs, auto)
      finally show ?thesis.
    qed   
    then have "⟨⟨sx,sz⟩,⟨tx,tz⟩⟩ = ⟨⟨my1,z⟩,⟨my2,z⟩⟩"
      using yz_def by auto
    then have "⟨sx,sz⟩ = ⟨my1,z⟩ ∧ ⟨tx,tz⟩ = ⟨my2,z⟩"
      using element_pair_eq by (typecheck_cfuncs, auto)
    then have eqs: "sx = my1 ∧ sz = z ∧ tx = my2 ∧ tz = z"
      using element_pair_eq by (typecheck_cfuncs, auto)

    have "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c ⟨y',z⟩ = ⟨⟨tx,tz⟩, ⟨sx,sz⟩⟩"
    proof -
      have "(distribute_right X X Z ∘c (m ×f idc Z)) ∘c ⟨y',z⟩ = distribute_right X X Z ∘c (m ×f idc Z) ∘c ⟨y',z⟩"
        by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = distribute_right X X Z ∘c ⟨m ∘c y',idc Z ∘c z⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
      also have "... = distribute_right X X Z ∘c ⟨⟨my2,my1⟩, z⟩"
        unfolding y'_def by (typecheck_cfuncs, simp add: id_left_unit2)
      also have "... = ⟨⟨my2,z⟩, ⟨my1,z⟩⟩"
        using distribute_right_ap by (typecheck_cfuncs, auto)
      also have "... = ⟨⟨tx,tz⟩, ⟨sx,sz⟩⟩"
        using eqs by auto
      finally show ?thesis.
    qed
    then show "⟨⟨tx,tz⟩,⟨sx,sz⟩⟩ factorsthru (distribute_right X X Z ∘c m ×f idc Z)"
      by (typecheck_cfuncs, metis cfunc_prod_type eqs factors_through_def2 y'_type)
  qed
qed

lemma right_pair_symmetric:
  assumes "symmetric_on X (Y, m)"
  shows "symmetric_on (Z ×c X) (Z ×c Y, distribute_left Z X X  ∘c (idc Z ×f m))"
proof (unfold symmetric_on_def, safe)
  have "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 symmetric_on_def by auto
  then show "(Z ×c Y, distribute_left Z X X  ∘c (idc Z ×f m)) ⊆c (Z ×c X) ×c Z ×c X"
    by (simp add: right_pair_subset)
next
  have m_def[type_rule]: "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 symmetric_on_def by auto

  fix s t 
  assume s_type[type_rule]: "s ∈c Z ×c X"
  assume t_type[type_rule]: "t ∈c Z ×c X"
  assume st_relation: "⟨s,t⟩ ∈⇘(Z ×c X) ×c Z ×c X⇙ (Z ×c Y, distribute_left Z X X  ∘c (idc Z ×f m))"
  
  obtain xs zs where s_def[type_rule]: " xs ∈c Z" "zs ∈c X" "s =  ⟨xs,zs⟩"
    using cart_prod_decomp s_type by blast
  obtain xt zt where t_def[type_rule]: "xt ∈c Z" "zt ∈c X" "t =  ⟨xt,zt⟩"
    using cart_prod_decomp t_type by blast 

  show "⟨t,s⟩ ∈⇘(Z ×c X) ×c (Z ×c X)⇙ (Z ×c Y, distribute_left Z X X  ∘c (idc Z ×f m))" 
    using s_def t_def m_def
  proof (typecheck_cfuncs, clarify, unfold relative_member_def2, safe)
    show "monomorphism (distribute_left Z X X  ∘c (idc Z ×f m))"
      using relative_member_def2 st_relation by blast

    have "⟨⟨xs,zs⟩, ⟨xt,zt⟩⟩ factorsthru (distribute_left Z X X  ∘c (idc Z ×f m))"
      using st_relation s_def t_def unfolding relative_member_def2 by auto
    then obtain zy where zy_type[type_rule]: "zy ∈c Z ×c Y"
      and zy_def: "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c zy = ⟨⟨xs,zs⟩, ⟨xt,zt⟩⟩"
      using s_def t_def m_def by (typecheck_cfuncs, unfold factors_through_def2, auto)
    then obtain y z where
      y_type[type_rule]: "y ∈c Y" and z_type[type_rule]: "z ∈c Z" and yz_pair: "zy = ⟨z, y⟩"
      using cart_prod_decomp by blast
    then obtain my1 my2 where my_types[type_rule]: "my1 ∈c X" "my2 ∈c X" and my_def: "m ∘c y = ⟨my2,my1⟩"
      by (metis cart_prod_decomp cfunc_type_def codomain_comp domain_comp m_def(1))
    then obtain y' where y'_type[type_rule]: "y' ∈c Y" and y'_def: "m ∘c y' = ⟨my1,my2⟩"
      using assms symmetric_def2 y_type by blast

    have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c zy = ⟨⟨z,my2⟩, ⟨z,my1⟩⟩"
    proof -
      have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c zy = distribute_left Z X X  ∘c (idc Z ×f m) ∘c zy"
        unfolding yz_pair by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = distribute_left Z X X  ∘c ⟨idc Z ∘c z , m ∘c y⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod yz_pair)
      also have "... = distribute_left Z X X  ∘c ⟨z , ⟨my2,my1⟩⟩"
        unfolding my_def by (typecheck_cfuncs, simp add: id_left_unit2)
      also have "... = ⟨⟨z,my2⟩, ⟨z,my1⟩⟩"
        using distribute_left_ap by (typecheck_cfuncs, auto)
      finally show ?thesis.
    qed   
    then have "⟨⟨xs,zs⟩,⟨xt,zt⟩⟩ = ⟨⟨z,my2⟩,⟨z,my1⟩⟩"
      using zy_def by auto
    then have "⟨xs,zs⟩ = ⟨z,my2⟩ ∧ ⟨xt,zt⟩ = ⟨z, my1⟩"
      using element_pair_eq by (typecheck_cfuncs, auto)
    then have eqs: "xs = z ∧ zs = my2 ∧ xt = z ∧ zt = my1"
      using element_pair_eq by (typecheck_cfuncs, auto)

    have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c ⟨z,y'⟩ = ⟨⟨xt,zt⟩, ⟨xs,zs⟩⟩"
    proof -
      have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c ⟨z,y'⟩ = distribute_left Z X X  ∘c (idc Z ×f m) ∘c ⟨z,y'⟩"
        by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = distribute_left Z X X ∘c ⟨idc Z ∘c z, m ∘c y'⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
      also have "... = distribute_left Z X X ∘c ⟨z, ⟨my1,my2⟩⟩"
        unfolding y'_def by (typecheck_cfuncs, simp add: id_left_unit2)
      also have "... = ⟨⟨z,my1⟩, ⟨z,my2⟩⟩"
        using distribute_left_ap by (typecheck_cfuncs, auto)
      also have "... = ⟨⟨xt,zt⟩, ⟨xs,zs⟩⟩"
        using eqs by auto
      finally show ?thesis.
    qed
    then show "⟨⟨xt,zt⟩,⟨xs,zs⟩⟩ factorsthru (distribute_left Z X X  ∘c (idc Z ×f m))"
      by (typecheck_cfuncs, metis cfunc_prod_type eqs factors_through_def2 y'_type)
  qed
qed

lemma left_pair_transitive:
  assumes "transitive_on X (Y, m)"
  shows "transitive_on (X ×c Z) (Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z))"
proof (unfold transitive_on_def, safe)
  have "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 transitive_on_def by auto
  then show "(Y ×c Z, distribute_right X X Z ∘c m ×f idc Z) ⊆c (X ×c Z) ×c X ×c Z"
    by (simp add: left_pair_subset)
next
  have m_def[type_rule]: "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 transitive_on_def by auto

  fix s t u
  assume s_type[type_rule]: "s ∈c X ×c Z"
  assume t_type[type_rule]: "t ∈c X ×c Z"
  assume u_type[type_rule]: "u ∈c X ×c Z"

  assume st_relation: "⟨s,t⟩ ∈⇘(X ×c Z) ×c X ×c Z⇙ (Y ×c Z, distribute_right X X Z ∘c m ×f idc Z)"
  then obtain h where h_type[type_rule]: "h ∈c Y ×c Z" and h_def: "(distribute_right X X Z ∘c m ×f idc Z) ∘c h = ⟨s,t⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  then obtain hy hz where h_part_types[type_rule]: "hy ∈c Y" "hz ∈c Z" and h_decomp: "h = ⟨hy, hz⟩"
    using cart_prod_decomp by blast
  then obtain mhy1 mhy2 where mhy_types[type_rule]: "mhy1 ∈c X" "mhy2 ∈c X" and mhy_decomp:  "m ∘c hy = ⟨mhy1, mhy2⟩"
    using cart_prod_decomp by (typecheck_cfuncs, blast)

  have "⟨s,t⟩ = ⟨⟨mhy1, hz⟩, ⟨mhy2, hz⟩⟩"
  proof -
    have "⟨s,t⟩ = (distribute_right X X Z ∘c m ×f idc Z) ∘c ⟨hy, hz⟩"
      using h_decomp h_def by auto
    also have "... = distribute_right X X Z ∘c (m ×f idc Z) ∘c ⟨hy, hz⟩"
      by (typecheck_cfuncs, auto simp add: comp_associative2)
    also have "... = distribute_right X X Z ∘c ⟨m ∘c hy, hz⟩"
      by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
    also have "... = ⟨⟨mhy1, hz⟩, ⟨mhy2, hz⟩⟩"
      unfolding mhy_decomp by (typecheck_cfuncs, simp add: distribute_right_ap)
    finally show ?thesis.
  qed
  then have s_def: "s = ⟨mhy1, hz⟩" and t_def: "t = ⟨mhy2, hz⟩"
    using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)

  assume tu_relation: "⟨t,u⟩ ∈⇘(X ×c Z) ×c X ×c Z⇙ (Y ×c Z, distribute_right X X Z ∘c m ×f idc Z)"
  then obtain g where g_type[type_rule]: "g ∈c Y ×c Z" and g_def: "(distribute_right X X Z ∘c m ×f idc Z) ∘c g = ⟨t,u⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  then obtain gy gz where g_part_types[type_rule]: "gy ∈c Y" "gz ∈c Z" and g_decomp: "g = ⟨gy, gz⟩"
    using cart_prod_decomp by blast
  then obtain mgy1 mgy2 where mgy_types[type_rule]: "mgy1 ∈c X" "mgy2 ∈c X" and mgy_decomp:  "m ∘c gy = ⟨mgy1, mgy2⟩"
    using cart_prod_decomp by (typecheck_cfuncs, blast)

  have "⟨t,u⟩ = ⟨⟨mgy1, gz⟩, ⟨mgy2, gz⟩⟩"
  proof -
    have "⟨t,u⟩ = (distribute_right X X Z ∘c m ×f idc Z) ∘c ⟨gy, gz⟩"
      using g_decomp g_def by auto
    also have "... = distribute_right X X Z ∘c (m ×f idc Z) ∘c ⟨gy, gz⟩"
      by (typecheck_cfuncs, auto simp add: comp_associative2)
    also have "... = distribute_right X X Z ∘c ⟨m ∘c gy, gz⟩"
      by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
    also have "... = ⟨⟨mgy1, gz⟩, ⟨mgy2, gz⟩⟩"
      unfolding mgy_decomp by (typecheck_cfuncs, simp add: distribute_right_ap)
    finally show ?thesis.
  qed
  then have t_def2: "t = ⟨mgy1, gz⟩" and u_def: "u = ⟨mgy2, gz⟩"
    using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)

  have mhy2_eq_mgy1: "mhy2 = mgy1"
    using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
  have gy_eq_gz: "hz = gz"
    using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)

  have mhy_in_Y: "⟨mhy1, mhy2⟩ ∈⇘X ×c X⇙ (Y, m)"
    using m_def h_part_types mhy_decomp
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  have mgy_in_Y: "⟨mhy2, mgy2⟩ ∈⇘X ×c X⇙ (Y, m)"
    using m_def g_part_types mgy_decomp mhy2_eq_mgy1
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)

  have "⟨mhy1, mgy2⟩ ∈⇘X ×c X⇙ (Y, m)"
    using assms mhy_in_Y mgy_in_Y mgy_types mhy2_eq_mgy1 unfolding transitive_on_def
    by (typecheck_cfuncs, blast)
  then obtain y where y_type[type_rule]: "y ∈c Y" and y_def: "m ∘c y = ⟨mhy1, mgy2⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)

  show " ⟨s,u⟩ ∈⇘(X ×c Z) ×c X ×c Z⇙ (Y ×c Z, distribute_right X X Z ∘c (m ×f idc Z))" 
  proof (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, safe)
    show "monomorphism (distribute_right X X Z ∘c m ×f idc Z)"
      using relative_member_def2 st_relation by blast

    show "∃h. h ∈c Y ×c Z ∧ (distribute_right X X Z ∘c m ×f idc Z) ∘c h = ⟨s,u⟩"
      unfolding s_def u_def gy_eq_gz
    proof (intro exI[where x="⟨y,gz⟩"], safe, typecheck_cfuncs)
      have "(distribute_right X X Z ∘c m ×f idc Z) ∘c ⟨y,gz⟩ = distribute_right X X Z ∘c (m ×f idc Z) ∘c ⟨y,gz⟩"
        by (typecheck_cfuncs, auto simp add: comp_associative2)
      also have "... = distribute_right X X Z ∘c ⟨m ∘c y, gz⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
      also have "... = ⟨⟨mhy1,gz⟩,⟨mgy2,gz⟩⟩"
        unfolding y_def by (typecheck_cfuncs, simp add: distribute_right_ap)
      finally show "(distribute_right X X Z ∘c m ×f idc Z) ∘c ⟨y,gz⟩ = ⟨⟨mhy1,gz⟩,⟨mgy2,gz⟩⟩".
    qed
  qed
qed

lemma right_pair_transitive:
  assumes "transitive_on X (Y, m)"
  shows "transitive_on (Z ×c X) (Z ×c Y, distribute_left Z X X ∘c (idc Z ×f m))"
proof (unfold transitive_on_def, safe)
  have "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 transitive_on_def by auto
  then show "(Z ×c Y, distribute_left Z X X ∘c idc Z ×f m) ⊆c (Z ×c X) ×c Z ×c X"
    by (simp add: right_pair_subset)
next
  have m_def[type_rule]: "m : Y → X ×c X" "monomorphism m"
    using assms subobject_of_def2 transitive_on_def by auto

  fix s t u
  assume s_type[type_rule]: "s ∈c Z ×c X"
  assume t_type[type_rule]: "t ∈c Z ×c X"
  assume u_type[type_rule]: "u ∈c Z ×c X"
  assume st_relation: "⟨s,t⟩ ∈⇘(Z ×c X) ×c Z ×c X⇙ (Z ×c Y, distribute_left Z X X ∘c idc Z ×f m)"
  then obtain h where h_type[type_rule]: "h ∈c Z ×c Y" and h_def: "(distribute_left Z X X  ∘c idc Z ×f m) ∘c h = ⟨s,t⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  then obtain hy hz where h_part_types[type_rule]: "hy ∈c Y" "hz ∈c Z" and h_decomp: "h = ⟨hz, hy⟩"
    using cart_prod_decomp by blast
  then obtain mhy1 mhy2 where mhy_types[type_rule]: "mhy1 ∈c X" "mhy2 ∈c X" and mhy_decomp:  "m ∘c hy = ⟨mhy1, mhy2⟩"
    using cart_prod_decomp by (typecheck_cfuncs, blast)

  have "⟨s,t⟩ = ⟨⟨hz, mhy1⟩, ⟨hz, mhy2⟩⟩"
  proof -
    have "⟨s,t⟩ = (distribute_left Z X X  ∘c idc Z ×f m) ∘c ⟨hz, hy⟩"
      using h_decomp h_def by auto
    also have "... = distribute_left Z X X  ∘c (idc Z ×f m) ∘c ⟨hz, hy⟩"
      by (typecheck_cfuncs, auto simp add: comp_associative2)
    also have "... = distribute_left Z X X  ∘c ⟨ hz, m ∘c hy⟩"
      by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
    also have "... = ⟨⟨hz, mhy1⟩, ⟨hz, mhy2⟩⟩"
      unfolding mhy_decomp by (typecheck_cfuncs, simp add: distribute_left_ap)
    finally show ?thesis.
  qed
  then have s_def: "s = ⟨hz, mhy1⟩" and t_def: "t = ⟨hz, mhy2⟩"
    using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)

  assume tu_relation: "⟨t,u⟩ ∈⇘(Z ×c X) ×c
               Z ×c X⇙ (Z ×c Y, distribute_left Z X X ∘c idc Z ×f m)"
  then obtain g where g_type[type_rule]: "g ∈c Z ×c Y" and g_def: "(distribute_left Z X X  ∘c idc Z ×f m) ∘c g = ⟨t,u⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  then obtain gy gz where g_part_types[type_rule]: "gy ∈c Y" "gz ∈c Z" and g_decomp: "g = ⟨gz, gy⟩"
    using cart_prod_decomp by blast
  then obtain mgy1 mgy2 where mgy_types[type_rule]: "mgy1 ∈c X" "mgy2 ∈c X" and mgy_decomp:  "m ∘c gy = ⟨mgy2, mgy1⟩"
    using cart_prod_decomp by (typecheck_cfuncs, blast)

  have "⟨t,u⟩ = ⟨⟨gz, mgy2⟩, ⟨gz, mgy1⟩⟩"
  proof -
    have "⟨t,u⟩ = (distribute_left Z X X  ∘c idc Z ×f m) ∘c ⟨gz, gy⟩"
      using g_decomp g_def by auto
    also have "... = distribute_left Z X X  ∘c (idc Z ×f m) ∘c ⟨gz, gy⟩"
      by (typecheck_cfuncs, auto simp add: comp_associative2)
    also have "... = distribute_left Z X X  ∘c ⟨gz, m ∘c gy⟩"
      by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
    also have "... = ⟨⟨gz, mgy2⟩, ⟨gz, mgy1⟩⟩"
      unfolding mgy_decomp by (typecheck_cfuncs, simp add: distribute_left_ap)
    finally show ?thesis.
  qed
  then have t_def2: "t = ⟨gz, mgy2⟩" and u_def: "u = ⟨gz, mgy1⟩"
    using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)
  have mhy2_eq_mgy2: "mhy2 = mgy2"
    using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
  have gy_eq_gz: "hz = gz"
    using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
  have mhy_in_Y: "⟨mhy1, mhy2⟩ ∈⇘X ×c X⇙ (Y, m)"
    using m_def h_part_types mhy_decomp
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  have mgy_in_Y: "⟨mhy2, mgy1⟩ ∈⇘X ×c X⇙ (Y, m)"
    using m_def g_part_types mgy_decomp mhy2_eq_mgy2
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  have "⟨mhy1, mgy1⟩ ∈⇘X ×c X⇙ (Y, m)"
    using assms mhy_in_Y mgy_in_Y mgy_types mhy2_eq_mgy2 unfolding transitive_on_def
    by (typecheck_cfuncs, blast)
  then obtain y where y_type[type_rule]: "y ∈c Y" and y_def: "m ∘c y = ⟨mhy1, mgy1⟩"
    by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
  show " ⟨s,u⟩ ∈⇘(Z ×c X) ×c Z ×c X⇙ (Z ×c Y, distribute_left Z X X ∘c idc Z ×f m)" 
  proof (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, safe)
    show "monomorphism (distribute_left Z X X ∘c idc Z ×f m)"
      using relative_member_def2 st_relation by blast
    show "∃h. h ∈c Z ×c Y ∧ (distribute_left Z X X ∘c idc Z ×f m) ∘c h = ⟨s,u⟩"
      unfolding s_def u_def gy_eq_gz
    proof (intro exI[where x="⟨gz,y⟩"], safe, typecheck_cfuncs)
      have "(distribute_left Z X X  ∘c (idc Z ×f m)) ∘c ⟨gz,y⟩ = distribute_left Z X X  ∘c (idc Z ×f m) ∘c ⟨gz,y⟩"
        by (typecheck_cfuncs, auto simp add: comp_associative2)
      also have "... = distribute_left Z X X  ∘c ⟨gz, m ∘c y⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
      also have "... = ⟨⟨gz,mhy1⟩,⟨gz,mgy1⟩⟩"
        by (typecheck_cfuncs, simp add: distribute_left_ap y_def)
      finally show "(distribute_left Z X X ∘c idc Z ×f m) ∘c ⟨gz,y⟩ = ⟨⟨gz,mhy1⟩,⟨gz,mgy1⟩⟩".
    qed
  qed
qed

lemma left_pair_equiv_rel:
  assumes "equiv_rel_on X (Y, m)"
  shows "equiv_rel_on (X ×c Z) (Y ×c Z, distribute_right X X Z ∘c (m ×f id Z))"
  using assms left_pair_reflexive left_pair_symmetric left_pair_transitive
  by (unfold equiv_rel_on_def, auto)

lemma right_pair_equiv_rel:
  assumes "equiv_rel_on X (Y, m)"
  shows "equiv_rel_on (Z ×c X) (Z ×c Y, distribute_left Z X X  ∘c (id Z ×f m))"
  using assms right_pair_reflexive right_pair_symmetric right_pair_transitive
  by (unfold equiv_rel_on_def, auto)

end