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×cXR)))"

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×cXR  y,x ∈⇘X×cXR)))" 

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×cXR  y,z ∈⇘X×cXR  x,z ∈⇘X×cXR)))"

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×cXR  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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
proof (unfold equiv_rel_on_def, safe)
  show "reflexive_on X (Xf⇙×cfX, fibered_product_morphism X f f X)"
  proof (unfold reflexive_on_def, safe)
    show "(Xf⇙×cfX, 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(Xf⇙×cfX, fibered_product_morphism X f f X)"
      by (smt 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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
  proof (unfold symmetric_on_def, safe)
    show "(Xf⇙×cfX, 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(Xf⇙×cfX, 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(Xf⇙×cfX, fibered_product_morphism X f f X)"
      using assms fibered_product_pair_member x_type y_type by auto
  qed

  show "transitive_on X (Xf⇙×cfX, fibered_product_morphism X f f X)"
  proof (unfold transitive_on_def, safe)
    show "(Xf⇙×cfX, 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(Xf⇙×cfX, fibered_product_morphism X f f X)"
    assume yz_in: "y,z ∈⇘X ×c X(Xf⇙×cfX, 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(Xf⇙×cfX, 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×cXR  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 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="Xf⇙×cfX"], safe)
  show "fibered_product_left_proj X f f X : Xf⇙×cfX  X"
    using assms by typecheck_cfuncs
  show "fibered_product_right_proj X f f X : Xf⇙×cfX  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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
  obtain  q where q_def: "q = equiv_class (Xf⇙×cfX, 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 (Xf⇙×cfX, 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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
        by (meson assms(1) kernel_pair_equiv_rel)
      have fact2: "const_on_rel X (Xf⇙×cfX, 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 : Xf⇙×cfX  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 : Xf⇙×cfX  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 : Xf⇙×cfX  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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
    by auto
  have "const_on_rel X (Xf⇙×cfX, 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 (Xf⇙×cfX, 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 (Xf⇙×cfX, fibered_product_morphism X f f X)"
    by auto
  obtain E where E_def: "E = quotient_set X (Xf⇙×cfX, fibered_product_morphism X f f X)"
    by auto
  obtain m where m_def: "m = quotient_func f (Xf⇙×cfX, 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 (Xf⇙×cfX, 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 : Xf⇙×cfX  Em⇙×cmE 
        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 : Xf⇙×cfX  Em⇙×cmE" 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  fA⦈⇘n
    m : fA⦈⇘n Y 
    coequalizer (fA⦈⇘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 : fA⦈⇘n Y  f c n = x c g  x = m)"
proof -
  have "g m.
    g : A  fA⦈⇘n
    m : fA⦈⇘n codomain f 
    coequalizer (fA⦈⇘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 : fA⦈⇘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  ffst An⦈⇘snd An m : ffst An⦈⇘snd An codomain f 
    coequalizer (ffst 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 : ffst 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  fA⦈⇘n m : fA⦈⇘n Y 
    coequalizer (fA⦈⇘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 : fA⦈⇘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)  ffst (A, n)⦈⇘snd (A, n) m : ffst (A, n)⦈⇘snd (A, n) codomain f 
    coequalizer (ffst (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 : ffst (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
  "[fA⦈⇘n⇙]map = (THE m. f↾⇘(A, n): A  fA⦈⇘n m : fA⦈⇘n codomain f 
   coequalizer (fA⦈⇘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 : (fA⦈⇘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  fA⦈⇘n [fA⦈⇘n⇙]map : fA⦈⇘n Y 
    coequalizer (fA⦈⇘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 ([fA⦈⇘n⇙]map)  f c n = [fA⦈⇘n⇙]map c (f↾⇘(A, n))  (x. x : fA⦈⇘n Y  f c n = x c (f↾⇘(A, n))  x = [fA⦈⇘n⇙]map)"
proof -
  have codom_f: "codomain f = Y"
    using assms(1) cfunc_type_def by auto
  have "f↾⇘(A, n): A  fA⦈⇘n ([fA⦈⇘n⇙]map) : fA⦈⇘n codomain f 
   coequalizer (fA⦈⇘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 ([fA⦈⇘n⇙]map)  f c n = ([fA⦈⇘n⇙]map) c (f↾⇘(A, n))  
   (x. x : (fA⦈⇘n)  codomain f  f c n = x c (f↾⇘(A, n))  x = ([fA⦈⇘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  fA⦈⇘n⇙"
  using assms image_restriction_mapping_def2 by blast

lemma image_rest_map_coequalizer:
  assumes "f : X  Y" "n : A  X"
  shows "coequalizer (fA⦈⇘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 "[fA⦈⇘n⇙]map : fA⦈⇘n Y"
  using assms image_subobject_mapping_def2 by blast

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

lemma image_subobj_comp_image_rest:
  assumes "f : X  Y" "n : A  X"
  shows "[fA⦈⇘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 : fA⦈⇘n Y  f c n = x c (f↾⇘(A, n))  x = [fA⦈⇘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 "fA⦈⇘a A"
proof -
  have "monomorphism (f c a)"
    using assms cfunc_type_def composition_of_monic_pair_is_monic by auto
  then have "monomorphism ([fA⦈⇘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  fA⦈⇘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  (fA⦈⇘a, [fA⦈⇘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 (fca) (fca) A"
    by auto
  obtain p1 where p1_def[simp]: "p1 = fibered_product_right_proj A (fca) (fca) A"
    by auto
  obtain E where E_def[simp]: "E = Af c a⇙×cf c aA"
    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 : fA⦈⇘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 : fA⦈⇘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 = [fA⦈⇘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 "(fA⦈⇘a, [fA⦈⇘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 fA⦈⇘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 (fA⦈⇘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 fA⦈⇘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. (fA⦈⇘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 fA⦈⇘m c n⇙"
    using f_type images_iso m_type n_type by blast
  then obtain k where
    k_type[type_rule]: "k : fA⦈⇘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. (fA⦈⇘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 "(fA⦈⇘m c n, [fA⦈⇘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 (fA⦈⇘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 : fA⦈⇘m c n F  k c f↾⇘(A, m c n)= h)"
    by (typecheck_cfuncs_prems, unfold coequalizer_def2, auto)
  then have "∃!k. k : fA⦈⇘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' : fA⦈⇘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: "[fA⦈⇘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 : fA⦈⇘m c n B  b c k = [fA⦈⇘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-1B⦈⇘m,[f-1B⦈⇘m⇙]map)) = ((fA⦈⇘a, [fA⦈⇘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-1B⦈⇘m⇙]map"
    by blast
  then have m'_type[type_rule]: "m' : f-1B⦈⇘m X"
    using assms(3) b_mono inverse_image_subobject_mapping_type m'_def by (typecheck_cfuncs, force)

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

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

  obtain j where j_def: "j = [fA⦈⇘d⇙]map"
    by simp
  then have j_type[type_rule]: "j : fA⦈⇘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  fA⦈⇘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-1B⦈⇘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 "(fA⦈⇘a, [fA⦈⇘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 "(fA⦈⇘a, [fA⦈⇘a⇙]map) ⊆⇘Y(B, m)"
  then obtain s where                                             
      s_type[type_rule]: "s : fA⦈⇘a B" and
      m_s_eq_subobj_map: "m c s = [fA⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘m, [f-1B⦈⇘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-1B⦈⇘m [f-1B⦈⇘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-1fA⦈⇘m⇙⦈⇘[fA⦈⇘m⇙]map⇙, [f-1fA⦈⇘m⇙⦈⇘[fA⦈⇘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 "((fA⦈⇘m, [fA⦈⇘m⇙]map) ⊆⇘Y(fA⦈⇘m, [fA⦈⇘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-1fA⦈⇘m⇙⦈⇘[fA⦈⇘m⇙]map⇙, [f-1fA⦈⇘m⇙⦈⇘[fA⦈⇘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