Theory Equalizer

section ‹Equalizers and Subobjects›

theory Equalizer
  imports Terminal
begin

subsection ‹Equalizers›

definition equalizer :: "cset ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ bool" where
  "equalizer E m f g ⟷ (∃ X Y. (f : X → Y) ∧ (g : X → Y) ∧ (m : E → X)
    ∧ (f ∘⇩c m = g ∘⇩c m)
    ∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h)))"

lemma equalizer_def2:
  assumes "f : X → Y" "g : X → Y" "m : E → X"
  shows "equalizer E m f g ⟷ ((f ∘⇩c m = g ∘⇩c m)
    ∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h)))"
  using assms unfolding equalizer_def by (auto simp add: cfunc_type_def)

lemma equalizer_eq:
  assumes "f : X → Y" "g : X → Y" "m : E → X"
  assumes "equalizer E m f g"
  shows "f ∘⇩c m = g ∘⇩c m"
  using assms equalizer_def2 by auto

lemma similar_equalizers:
  assumes "f : X → Y" "g : X → Y" "m : E → X"
  assumes "equalizer E m f g"
  assumes "h : F → X" "f ∘⇩c h = g ∘⇩c h"
  shows "∃! k. k : F → E ∧ m ∘⇩c k = h"
  using assms equalizer_def2 by auto

text ‹The definition above and the axiomatization below correspond to Axiom 4 (Equalizers) in Halvorson.›
axiomatization where
  equalizer_exists: "f : X → Y ⟹ g : X → Y ⟹ ∃ E m. equalizer E m f g"

lemma equalizer_exists2:
  assumes "f : X → Y" "g : X → Y"
  shows "∃ E m. m : E → X ∧ f ∘⇩c m = g ∘⇩c m ∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h))"
proof -
  obtain E m where "equalizer E m f g"
    using assms equalizer_exists by blast
  then show ?thesis
    unfolding equalizer_def
  proof (intro exI[where x=E], intro exI[where x=m], safe)
    fix X' Y'
    assume f_type2: "f : X' → Y'"
    assume g_type2: "g : X' → Y'"
    assume m_type: "m : E → X'"
    assume fm_eq_gm: "f ∘⇩c m = g ∘⇩c m"
    assume equalizer_unique: "∀h F. h : F → X' ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E ∧ m ∘⇩c k = h)"

    show m_type2: "m : E → X"
      using assms(2) cfunc_type_def g_type2 m_type by auto

    show "⋀ h F. h : F → X ⟹ f ∘⇩c h = g ∘⇩c h ⟹ ∃k. k : F → E ∧ m ∘⇩c k = h"
      by (metis m_type2 cfunc_type_def equalizer_unique m_type)

    show "⋀ F k y. m ∘⇩c k : F → X ⟹ f ∘⇩c m ∘⇩c k = g ∘⇩c m ∘⇩c k ⟹ k : F → E ⟹ y : F → E
        ⟹ m ∘⇩c y = m ∘⇩c k ⟹ k = y"
      using comp_type equalizer_unique m_type by blast
  qed
qed 

text ‹The lemma below corresponds to Exercise 2.1.31 in Halvorson.›
lemma equalizers_isomorphic:
  assumes "equalizer E m f g" "equalizer E' m' f g"
  shows "∃ k. k : E → E' ∧ isomorphism k ∧ m = m' ∘⇩c k"
proof -
  have fm_eq_gm: "f ∘⇩c m = g ∘⇩c m"
    using assms(1) equalizer_def by blast
  have fm'_eq_gm': "f ∘⇩c m' = g ∘⇩c m'"
    using assms(2) equalizer_def by blast

  obtain X Y where f_type: "f : X → Y" and g_type: "g : X → Y" and m_type: "m : E → X"
    using assms(1) unfolding equalizer_def by auto

  obtain k where k_type: "k : E' → E" and mk_eq_m': "m ∘⇩c k = m'"
    by (metis assms cfunc_type_def equalizer_def)
  obtain k' where k'_type: "k' : E → E'" and m'k_eq_m: "m' ∘⇩c k' = m"
    by (metis assms cfunc_type_def equalizer_def)

  have "f ∘⇩c m ∘⇩c k ∘⇩c k' = g ∘⇩c m ∘⇩c k ∘⇩c k'"
    using comp_associative2 m_type fm_eq_gm k'_type k_type m'k_eq_m mk_eq_m' by auto

  have "k ∘⇩c k' : E → E ∧ m ∘⇩c k ∘⇩c k' = m"
    using comp_associative2 comp_type k'_type k_type m_type m'k_eq_m mk_eq_m' by auto
  then have kk'_eq_id: "k ∘⇩c k' = id E"
    using assms(1) equalizer_def id_right_unit2 id_type by blast

  have "k' ∘⇩c k : E' → E' ∧ m' ∘⇩c k' ∘⇩c k = m'"
    by (smt (z3) comp_associative2 comp_type k'_type k_type m'k_eq_m m_type mk_eq_m')
  then have k'k_eq_id: "k' ∘⇩c k = id E'"
    using assms(2) equalizer_def id_right_unit2 id_type by blast

  show "∃k. k : E → E' ∧ isomorphism k ∧ m = m' ∘⇩c k"
    using cfunc_type_def isomorphism_def k'_type k'k_eq_id k_type kk'_eq_id m'k_eq_m by (intro exI[where x=k'], auto)
qed

lemma isomorphic_to_equalizer_is_equalizer:
  assumes "φ: E' → E"
  assumes "isomorphism φ"
  assumes "equalizer E m f g" 
  assumes "f : X → Y"
  assumes "g : X → Y"
  assumes "m : E → X"
  shows   "equalizer E' (m ∘⇩c φ) f g"
proof - 
  obtain φ_inv where φ_inv_type[type_rule]: "φ_inv : E → E'" and φ_inv_φ: "φ_inv ∘⇩c φ = id(E')" and φφ_inv: "φ ∘⇩c φ_inv = id(E)"
    using assms(1,2) cfunc_type_def isomorphism_def by auto

  have equalizes: "f ∘⇩c m ∘⇩c φ = g ∘⇩c m ∘⇩c φ"
    using assms comp_associative2 equalizer_def by force
  have "∀h F. h : F → X ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E' ∧ (m ∘⇩c φ) ∘⇩c k = h)"
  proof(safe)
    fix h F
    assume h_type[type_rule]: "h : F → X"
    assume h_equalizes: "f ∘⇩c h = g ∘⇩c h"
    have k_exists_uniquely: "∃! k. k: F  → E ∧ m ∘⇩c k = h"
      using assms equalizer_def2 h_equalizes by (typecheck_cfuncs, auto)
    then obtain k where k_type[type_rule]: "k: F  → E" and k_def: "m ∘⇩c k = h"
      by blast
    then show "∃k. k : F → E' ∧ (m ∘⇩c φ) ∘⇩c k = h"
      using assms by (typecheck_cfuncs, smt (z3) φφ_inv φ_inv_type comp_associative2 comp_type id_right_unit2 k_exists_uniquely)
  next
    fix F k y
    assume "(m ∘⇩c φ) ∘⇩c k : F → X"
    assume "f ∘⇩c (m ∘⇩c φ) ∘⇩c k = g ∘⇩c (m ∘⇩c φ) ∘⇩c k"
    assume k_type[type_rule]: "k : F → E'"
    assume y_type[type_rule]: "y : F → E'"
    assume "(m ∘⇩c φ) ∘⇩c y = (m ∘⇩c φ) ∘⇩c k"
    then show "k = y"
      by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(1,2,3) cfunc_type_def comp_associative comp_type equalizer_def id_left_unit2 isomorphism_def)
  qed
  then show ?thesis
    by (smt (verit, best) assms(1,4,5,6) comp_type equalizer_def equalizes)
qed

text ‹The lemma below corresponds to Exercise 2.1.34 in Halvorson.›
lemma equalizer_is_monomorphism:
  "equalizer E m f g ⟹  monomorphism(m)"
  unfolding equalizer_def monomorphism_def
proof clarify
  fix h1 h2 X Y
  assume f_type: "f : X → Y"
  assume g_type: "g : X → Y"
  assume m_type: "m : E → X"
  assume fm_gm: "f ∘⇩c m = g ∘⇩c m"
  assume uniqueness: "∀h F. h : F → X ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E ∧ m ∘⇩c k = h)"
  assume relation_ga: "codomain h1 = domain m"
  assume relation_h: "codomain h2 = domain m" 
  assume m_ga_mh: "m ∘⇩c h1 = m ∘⇩c h2"   
  have  "f ∘⇩c m ∘⇩c h1 =  g ∘⇩c m ∘⇩c h2"
    using cfunc_type_def comp_associative f_type fm_gm g_type m_ga_mh m_type relation_h by auto
  then obtain z where "z: domain(h1) → E ∧ m ∘⇩c z = m ∘⇩c h1 ∧ 
    (∀ j. j:domain(h1) → E ∧  m ∘⇩c j = m ∘⇩c h1 ⟶ j = z)"
    using uniqueness by (smt (z3) cfunc_type_def codomain_comp domain_comp m_ga_mh m_type relation_ga)
  then show "h1 = h2"
    by (metis cfunc_type_def domain_comp m_ga_mh m_type relation_ga relation_h)
qed

text ‹The definition below corresponds to Definition 2.1.35 in Halvorson.›
definition regular_monomorphism :: "cfunc ⇒ bool"
  where "regular_monomorphism f  ⟷  
          (∃ g h. domain g = codomain f ∧ domain h = codomain f ∧ equalizer (domain f) f g h)"

text ‹The lemma below corresponds to Exercise 2.1.36 in Halvorson.›
lemma epi_regmon_is_iso:
  assumes "epimorphism f" "regular_monomorphism f"
  shows "isomorphism f"
proof -
  obtain g h where g_type: "domain g = codomain f" and
                   h_type: "domain h = codomain f" and
                   f_equalizer: "equalizer (domain f) f g h"
    using assms(2) regular_monomorphism_def by auto
  then have "g ∘⇩c f = h ∘⇩c f"
    using equalizer_def by blast
  then have "g = h"
    using assms(1) cfunc_type_def epimorphism_def equalizer_def f_equalizer by auto
  then have "g ∘⇩c id(codomain f) = h ∘⇩c id(codomain f)"
    by simp
  then obtain k where k_type: "f ∘⇩c k = id(codomain(f)) ∧ codomain k = domain f"
    by (metis cfunc_type_def equalizer_def f_equalizer id_type)
  then have "f ∘⇩c id(domain(f)) = f ∘⇩c (k ∘⇩c f)"
    by (metis comp_associative domain_comp id_domain id_left_unit id_right_unit)
  then have "monomorphism f ⟹ k ∘⇩c f = id(domain f)"
    by (metis (mono_tags) codomain_comp domain_comp id_codomain id_domain k_type monomorphism_def)
  then have "k ∘⇩c f = id(domain f)"
    using equalizer_is_monomorphism f_equalizer by blast
  then show "isomorphism f"
    by (metis domain_comp id_domain isomorphism_def k_type)  
qed

subsection ‹Subobjects›

text ‹The definition below corresponds to Definition 2.1.32 in Halvorson.›
definition factors_through :: "cfunc  ⇒ cfunc ⇒ bool" (infix "factorsthru" 90)
  where "g factorsthru f ⟷ (∃ h. (h: domain(g)→ domain(f)) ∧ f ∘⇩c h = g)"

lemma factors_through_def2:
  assumes "g : X → Z" "f : Y → Z"
  shows "g factorsthru f ⟷ (∃ h. h: X → Y ∧ f ∘⇩c h = g)"
  unfolding factors_through_def using assms by (simp add: cfunc_type_def)

text ‹The lemma below corresponds to Exercise 2.1.33 in Halvorson.›
lemma xfactorthru_equalizer_iff_fx_eq_gx:
  assumes "f: X→ Y" "g:X → Y" "equalizer E m f g" "x∈⇩c X"
  shows "x factorsthru m ⟷ f ∘⇩c x = g  ∘⇩c x"
proof safe
  assume LHS: "x factorsthru m"
  then show "f ∘⇩c x = g  ∘⇩c x"
    using assms(3) cfunc_type_def comp_associative equalizer_def factors_through_def by auto
next
  assume RHS: "f ∘⇩c x = g  ∘⇩c x"
  then show "x factorsthru m"
    unfolding cfunc_type_def factors_through_def
    by (metis RHS assms(1,3,4) cfunc_type_def equalizer_def)
qed

text ‹The definition below corresponds to Definition 2.1.37 in Halvorson.›
definition subobject_of :: "cset × cfunc ⇒ cset ⇒ bool" (infix "⊆⇩c" 50)
  where "B ⊆⇩c X ⟷ (snd B : fst B → X ∧ monomorphism (snd B))"

lemma subobject_of_def2:
  "(B,m) ⊆⇩c X = (m : B → X ∧ monomorphism m)"
  by (simp add: subobject_of_def)

definition relative_subset :: "cset × cfunc ⇒ cset ⇒ cset × cfunc ⇒ bool" ("_⊆⇘_⇙_" [51,50,51]50)
  where "B ⊆⇘X⇙ A  ⟷ 
    (snd B : fst B → X ∧ monomorphism (snd B) ∧ snd A : fst A → X ∧ monomorphism (snd A)
          ∧ (∃ k. k: fst B → fst A ∧ snd A ∘⇩c k = snd B))"

lemma relative_subset_def2: 
  "(B,m) ⊆⇘X⇙ (A,n) = (m : B → X ∧ monomorphism m ∧ n : A → X ∧ monomorphism n
          ∧ (∃ k. k: B → A ∧ n ∘⇩c k = m))"
  unfolding relative_subset_def by auto

lemma subobject_is_relative_subset: "(B,m) ⊆⇩c A ⟷ (B,m) ⊆⇘A⇙ (A, id(A))"
  unfolding relative_subset_def2 subobject_of_def2
  using cfunc_type_def id_isomorphism id_left_unit id_type iso_imp_epi_and_monic by auto

text ‹The definition below corresponds to Definition 2.1.39 in Halvorson.›
definition relative_member :: "cfunc ⇒ cset ⇒ cset × cfunc ⇒ bool" ("_ ∈⇘_⇙ _" [51,50,51]50) where
  "x ∈⇘X⇙ B ⟷ (x ∈⇩c X ∧ monomorphism (snd B) ∧ snd B : fst B → X ∧ x factorsthru (snd B))"

lemma relative_member_def2:
  "x ∈⇘X⇙ (B, m) = (x ∈⇩c X ∧ monomorphism m ∧ m : B → X ∧ x factorsthru m)"
  unfolding relative_member_def by auto

text ‹The lemma below corresponds to Proposition 2.1.40 in Halvorson.›
lemma relative_subobject_member:
  assumes "(A,n) ⊆⇘X⇙ (B,m)" "x ∈⇩c X"
  shows "x ∈⇘X⇙ (A,n) ⟹ x ∈⇘X⇙ (B,m)"
  using assms unfolding relative_member_def2 relative_subset_def2
proof clarify
  fix k
  assume m_type: "m : B → X"
  assume k_type: "k : A → B"
  assume m_monomorphism: "monomorphism m"
  assume mk_monomorphism: "monomorphism (m ∘⇩c k)"
  assume n_eq_mk: "n = m ∘⇩c k"
  assume factorsthru_mk: "x factorsthru (m ∘⇩c k)"
  
  obtain a where a_assms: "a ∈⇩c A ∧ (m ∘⇩c k) ∘⇩c a = x"
    using assms(2) cfunc_type_def domain_comp factors_through_def factorsthru_mk k_type m_type by auto
  then show "x factorsthru m "
    unfolding factors_through_def 
    using cfunc_type_def comp_type k_type m_type comp_associative
    by (intro exI[where x="k ∘⇩c a"], auto)
qed

subsection ‹Inverse Image›

text‹The definition below corresponds to a definition given by a diagram between Definition 2.1.37 and Proposition 2.1.38 in Halvorson.›
definition inverse_image :: "cfunc ⇒ cset ⇒ cfunc ⇒ cset" ("_⇧-⇧1⦇_⦈⇘_⇙" [101,0,0]100) where
  "inverse_image f B m = (SOME A. ∃ X Y k. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
    equalizer A k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B))"

lemma inverse_image_is_equalizer:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "∃k. equalizer (f⇧-⇧1⦇B⦈⇘m⇙) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
proof -
  obtain A k where "equalizer A k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
    by (meson assms(1,2) comp_type equalizer_exists left_cart_proj_type right_cart_proj_type)
  then show "∃k. equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
    unfolding inverse_image_def using assms cfunc_type_def by (subst someI2_ex, auto)
qed

definition inverse_image_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc"  where
  "inverse_image_mapping f B m = (SOME k. ∃ X Y. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
    equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B))"

lemma inverse_image_is_equalizer2:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
proof -
  obtain k where "equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
    using assms inverse_image_is_equalizer by blast
  then have "∃ X Y. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
    equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
    unfolding inverse_image_mapping_def using assms by (subst someI_ex, auto)
  then show "equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
    using assms(2) cfunc_type_def by auto
qed

lemma inverse_image_mapping_type[type_rule]:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "inverse_image_mapping f B m : (inverse_image f B m) → X ×⇩c B"
  using assms cfunc_type_def domain_comp equalizer_def inverse_image_is_equalizer2 left_cart_proj_type by auto

lemma inverse_image_mapping_eq:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m
      = m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m"
  using assms cfunc_type_def comp_associative equalizer_def inverse_image_is_equalizer2
  by (typecheck_cfuncs, smt (verit))

lemma inverse_image_mapping_monomorphism:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "monomorphism (inverse_image_mapping f B m)"
  using assms equalizer_is_monomorphism inverse_image_is_equalizer2 by blast

text ‹The lemma below is the dual of Proposition 2.1.38 in Halvorson.›
lemma inverse_image_monomorphism:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "monomorphism (left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
  using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
  fix g h A
  assume g_type: "g : A → (f⇧-⇧1⦇B⦈⇘m⇙)"
  assume h_type: "h : A → (f⇧-⇧1⦇B⦈⇘m⇙)"
  assume left_eq: "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
    = (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
  then have "f ∘⇩c (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
    = f ∘⇩c (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
    by auto
  then have "m ∘⇩c (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
    = m ∘⇩c (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
    using assms g_type h_type
    by (typecheck_cfuncs, smt cfunc_type_def codomain_comp comp_associative domain_comp inverse_image_mapping_eq left_cart_proj_type) 
  then have right_eq: "(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
    = (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
    using assms g_type h_type monomorphism_def3 by (typecheck_cfuncs, auto)
  then have "inverse_image_mapping f B m ∘⇩c g = inverse_image_mapping f B m ∘⇩c h"
    using assms g_type h_type cfunc_type_def comp_associative left_eq left_cart_proj_type right_cart_proj_type
    by (typecheck_cfuncs, subst cart_prod_eq, auto)
  then show "g = h"
    using assms g_type h_type inverse_image_mapping_monomorphism inverse_image_mapping_type monomorphism_def3
    by blast
qed

definition inverse_image_subobject_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc" ("[_⇧-⇧1⦇_⦈⇘_⇙]map" [101,0,0]100) where
  "[f⇧-⇧1⦇B⦈⇘m⇙]map = left_cart_proj (domain f) B ∘⇩c inverse_image_mapping f B m"

lemma inverse_image_subobject_mapping_def2:
  assumes "f : X → Y"
  shows "[f⇧-⇧1⦇B⦈⇘m⇙]map = left_cart_proj X B ∘⇩c inverse_image_mapping f B m"
  using assms unfolding inverse_image_subobject_mapping_def cfunc_type_def by auto

lemma inverse_image_subobject_mapping_type[type_rule]:
  assumes "f : X → Y" "m : B → Y" "monomorphism m"
  shows "[f⇧-⇧1⦇B⦈⇘m⇙]map : f⇧-⇧1⦇B⦈⇘m⇙ → X"
  by (smt (verit, best) assms comp_type inverse_image_mapping_type inverse_image_subobject_mapping_def2 left_cart_proj_type)

lemma inverse_image_subobject_mapping_mono:
  assumes "f : X → Y" "m : B → Y" "monomorphism m"
  shows "monomorphism ([f⇧-⇧1⦇B⦈⇘m⇙]map)"
  using assms cfunc_type_def inverse_image_monomorphism inverse_image_subobject_mapping_def by fastforce

lemma inverse_image_subobject:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "(f⇧-⇧1⦇B⦈⇘m⇙, [f⇧-⇧1⦇B⦈⇘m⇙]map) ⊆⇩c X"
  unfolding subobject_of_def2
  using assms inverse_image_subobject_mapping_mono inverse_image_subobject_mapping_type
  by force

lemma inverse_image_pullback:
  assumes "m : B → Y" "f : X → Y" "monomorphism m"
  shows "is_pullback (f⇧-⇧1⦇B⦈⇘m⇙) B X Y 
    (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) m
    (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) f"
  unfolding is_pullback_def using assms
proof safe
  show right_type: "right_cart_proj X B ∘⇩c inverse_image_mapping f B m : f⇧-⇧1⦇B⦈⇘m⇙ → B"
    using assms cfunc_type_def codomain_comp domain_comp inverse_image_mapping_type
      right_cart_proj_type by auto
  show left_type: "left_cart_proj X B ∘⇩c inverse_image_mapping f B m : f⇧-⇧1⦇B⦈⇘m⇙ → X"
    using assms fst_conv inverse_image_subobject subobject_of_def by (typecheck_cfuncs)

  show "m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m =
      f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m"
    using assms inverse_image_mapping_eq by auto
next
  fix Z k h
  assume k_type: "k : Z → B" and h_type: "h : Z → X"
  assume mk_eq_fh: "m ∘⇩c k = f ∘⇩c h"

  have "equalizer (f⇧-⇧1⦇B⦈⇘m⇙) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B )"
    using assms inverse_image_is_equalizer2 by blast
  then have "∀h F. h : F → (X ×⇩c B) 
            ∧ (f ∘⇩c left_cart_proj X B) ∘⇩c h = (m ∘⇩c right_cart_proj X B) ∘⇩c h ⟶
          (∃!u. u : F → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = h)"
    unfolding equalizer_def using assms(2) cfunc_type_def domain_comp left_cart_proj_type by auto
  then have "⟨h,k⟩ : Z → X ×⇩c B  ⟹
      (f ∘⇩c left_cart_proj X B) ∘⇩c ⟨h,k⟩ = (m ∘⇩c right_cart_proj X B) ∘⇩c ⟨h,k⟩ ⟹
      (∃!u. u : Z → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩)"
    by auto
  then have "∃!u. u : Z → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩"
    using k_type h_type assms
    by (typecheck_cfuncs, smt comp_associative2 left_cart_proj_cfunc_prod left_cart_proj_type
        mk_eq_fh right_cart_proj_cfunc_prod right_cart_proj_type)
  then show "∃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"
  proof (clarify)
    fix u
    assume u_type[type_rule]: "u : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
    assume u_eq: "inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩"

    show "∃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"
    proof (rule exI[where x=u], typecheck_cfuncs, safe)

      show "(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c u = k"
        using assms u_type h_type k_type u_eq
        by (typecheck_cfuncs, metis (full_types) comp_associative2 right_cart_proj_cfunc_prod)
  
      show "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c u = h"
        using assms u_type h_type k_type u_eq
        by (typecheck_cfuncs, metis (full_types) comp_associative2 left_cart_proj_cfunc_prod)
    qed
  qed
next
  fix Z j y
  assume j_type: "j : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
  assume y_type: "y : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
  assume "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c y =
       (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j"
  then show "j = y"
    using assms j_type y_type inverse_image_mapping_type comp_type
    by (smt (verit, ccfv_threshold) inverse_image_monomorphism left_cart_proj_type monomorphism_def3)
qed

text ‹The lemma below corresponds to Proposition 2.1.41 in Halvorson.›
lemma in_inverse_image:
  assumes "f : X → Y" "(B,m) ⊆⇩c Y" "x ∈⇩c X"
  shows "(x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)) = (f ∘⇩c x ∈⇘Y⇙ (B,m))"
proof
  have m_type: "m : B → Y" "monomorphism m"
    using assms(2) unfolding subobject_of_def2 by auto

  assume "x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
  then obtain h where h_type: "h ∈⇩c (f⇧-⇧1⦇B⦈⇘m⇙)"
      and h_def: "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h = x"
    unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
  then have "f ∘⇩c x = f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"
    using assms m_type by (typecheck_cfuncs, simp add: comp_associative2 h_def)
  then have "f ∘⇩c x = (f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
    using assms m_type h_type h_def comp_associative2 by (typecheck_cfuncs, blast)
  then have "f ∘⇩c x = (m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
    using assms h_type m_type by (typecheck_cfuncs, simp add: inverse_image_mapping_eq m_type)
  then have "f ∘⇩c x = m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"
    using assms m_type h_type by (typecheck_cfuncs, smt cfunc_type_def comp_associative domain_comp)
  then have "(f ∘⇩c x) factorsthru m"
    unfolding factors_through_def using assms h_type m_type
    by (intro exI[where x="right_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"],
        typecheck_cfuncs, auto simp add: cfunc_type_def)
  then show "f ∘⇩c x ∈⇘Y⇙ (B, m)"
    unfolding relative_member_def2 using assms m_type by (typecheck_cfuncs, auto)
next
  have m_type: "m : B → Y" "monomorphism m"
    using assms(2) unfolding subobject_of_def2 by auto

  assume "f ∘⇩c x ∈⇘Y⇙ (B, m)"
  then have "∃h. h : domain (f ∘⇩c x) → domain m ∧ m ∘⇩c h = f ∘⇩c x"
    unfolding relative_member_def2 factors_through_def by auto
  then obtain h where h_type: "h ∈⇩c B" and h_def: "m ∘⇩c h = f ∘⇩c x"
    unfolding relative_member_def2 factors_through_def 
    using assms cfunc_type_def domain_comp m_type by auto
  then have "∃j. j ∈⇩c (f⇧-⇧1⦇B⦈⇘m⇙) ∧
         (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = h ∧
         (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = x"
    using inverse_image_pullback assms m_type unfolding is_pullback_def by blast
  then have "x factorsthru (left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
    using m_type assms cfunc_type_def by (typecheck_cfuncs, unfold factors_through_def, auto)
  then show "x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
    unfolding relative_member_def2 using m_type assms
    by (typecheck_cfuncs, simp add: inverse_image_monomorphism)
qed

subsection ‹Fibered Products›

text ‹The definition below corresponds to Definition 2.1.42 in Halvorson.›
definition fibered_product :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cset" ("_ ⇘_⇙×⇩c⇘_⇙ _" [66,50,50,65]65) where
  "X ⇘f⇙×⇩c⇘g⇙ Y = (SOME E. ∃ Z m. f : X → Z ∧ g : Y → Z ∧
    equalizer E m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y))"

lemma fibered_product_equalizer:
  assumes "f : X → Z" "g : Y → Z"
  shows "∃ m. equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
proof -
  obtain E m where "equalizer E m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    using assms equalizer_exists by (typecheck_cfuncs, blast)
  then have "∃x Z m. f : X → Z ∧ g : Y → Z ∧
      equalizer x m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    using assms by blast
  then have "∃ Z m. f : X → Z ∧ g : Y → Z ∧ 
      equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    unfolding fibered_product_def by (rule someI_ex)
  then show "∃m. equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    by auto
qed

definition fibered_product_morphism :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
  "fibered_product_morphism X f g Y = (SOME m. ∃ Z. f : X → Z ∧ g : Y → Z ∧
    equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y))"

lemma fibered_product_morphism_equalizer:
  assumes "f : X → Z" "g : Y → Z"
  shows "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
proof -
  have "∃x Z. f : X → Z ∧
      g : Y → Z ∧ equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) x (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    using assms fibered_product_equalizer by blast
  then have "∃Z. f : X → Z ∧ g : Y → Z ∧
    equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    unfolding fibered_product_morphism_def by (rule someI_ex)
  then show "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    by auto
qed

lemma fibered_product_morphism_type[type_rule]:
  assumes "f : X → Z" "g : Y → Z"
  shows "fibered_product_morphism X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → X ×⇩c Y"
  using assms cfunc_type_def domain_comp equalizer_def fibered_product_morphism_equalizer left_cart_proj_type by auto

lemma fibered_product_morphism_monomorphism:
  assumes "f : X → Z" "g : Y → Z"
  shows "monomorphism (fibered_product_morphism X f g Y)"
  using assms equalizer_is_monomorphism fibered_product_morphism_equalizer by blast

definition fibered_product_left_proj :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
  "fibered_product_left_proj X f g Y = (left_cart_proj X Y) ∘⇩c (fibered_product_morphism X f g Y)"

lemma fibered_product_left_proj_type[type_rule]:
  assumes "f : X → Z" "g : Y → Z"
  shows "fibered_product_left_proj X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → X"
  by (metis assms comp_type fibered_product_left_proj_def fibered_product_morphism_type left_cart_proj_type)

definition fibered_product_right_proj :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
  "fibered_product_right_proj X f g Y = (right_cart_proj X Y) ∘⇩c (fibered_product_morphism X f g Y)"

lemma fibered_product_right_proj_type[type_rule]:
  assumes "f : X → Z" "g : Y → Z"
  shows "fibered_product_right_proj X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → Y"
  by (metis assms comp_type fibered_product_right_proj_def fibered_product_morphism_type right_cart_proj_type)

lemma pair_factorsthru_fibered_product_morphism:
  assumes "f : X → Z" "g : Y → Z" "x : A → X" "y : A → Y"
  shows "f ∘⇩c x = g ∘⇩c y ⟹ ⟨x,y⟩ factorsthru fibered_product_morphism X f g Y"
  unfolding factors_through_def
proof -
  have equalizer: "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
    using fibered_product_morphism_equalizer assms by (typecheck_cfuncs, auto)

  assume "f ∘⇩c x = g ∘⇩c y"
  then have "(f ∘⇩c left_cart_proj X Y) ∘⇩c ⟨x,y⟩ = (g ∘⇩c right_cart_proj X Y) ∘⇩c ⟨x,y⟩"
    using assms by (typecheck_cfuncs, smt comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  then have "∃! h. h : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧ fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
    using assms similar_equalizers by (typecheck_cfuncs, smt (verit, del_insts)  cfunc_type_def equalizer equalizer_def)
  then show "∃h. h : domain ⟨x,y⟩ → domain (fibered_product_morphism X f g Y) ∧
        fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
    by (metis assms(1,2) cfunc_type_def domain_comp fibered_product_morphism_type)
qed

lemma fibered_product_is_pullback:
  assumes f_type[type_rule]: "f : X → Z" and g_type[type_rule]: "g : Y → Z"
  shows "is_pullback (X ⇘f⇙×⇩c⇘g⇙ Y) Y X Z  (fibered_product_right_proj X f g Y) g (fibered_product_left_proj X f g Y) f"
  unfolding is_pullback_def
  using assms fibered_product_left_proj_type fibered_product_right_proj_type
proof safe
  show "g ∘⇩c fibered_product_right_proj X f g Y = f ∘⇩c fibered_product_left_proj X f g Y"
    unfolding fibered_product_right_proj_def fibered_product_left_proj_def
    using cfunc_type_def comp_associative2 equalizer_def fibered_product_morphism_equalizer
    by (typecheck_cfuncs, auto)
next
  fix A k h
  assume k_type: "k : A → Y" and h_type: "h : A → X"
  assume k_h_commutes: "g ∘⇩c k = f ∘⇩c h"

  have "⟨h,k⟩ factorsthru fibered_product_morphism X f g Y"
    using assms h_type k_h_commutes k_type pair_factorsthru_fibered_product_morphism by auto
  then have f1: "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧ fibered_product_morphism X f g Y ∘⇩c j = ⟨h,k⟩"
    by (meson assms cfunc_prod_type factors_through_def2 fibered_product_morphism_type h_type k_type)
  then show "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧
           fibered_product_right_proj X f g Y ∘⇩c j = k ∧ fibered_product_left_proj X f g Y ∘⇩c j = h"
    unfolding fibered_product_right_proj_def fibered_product_left_proj_def 
  proof (clarify, safe)
    fix j
    assume j_type: "j : A → X ⇘f⇙×⇩c⇘g⇙ Y"

    show "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧
           (right_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y) ∘⇩c j = k ∧ (left_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y) ∘⇩c j = h"
      by (typecheck_cfuncs, smt (verit, best) f1 comp_associative2 h_type k_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
  qed
next
  fix A j y
  assume j_type: "j : A → X ⇘f⇙×⇩c⇘g⇙ Y" and y_type: "y : A → X ⇘f⇙×⇩c⇘g⇙ Y"
  assume "fibered_product_right_proj X f g Y ∘⇩c y = fibered_product_right_proj X f g Y ∘⇩c j"
  then have right_eq: "right_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c y) =
      right_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c j)"
    unfolding fibered_product_right_proj_def using assms j_type y_type
    by (typecheck_cfuncs, simp add: comp_associative2)
  assume "fibered_product_left_proj X f g Y ∘⇩c y = fibered_product_left_proj X f g Y ∘⇩c j"
  then have left_eq: "left_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c y) =
      left_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c j)"
    unfolding fibered_product_left_proj_def  using assms j_type y_type
    by (typecheck_cfuncs, simp add: comp_associative2)

  have mono: "monomorphism (fibered_product_morphism X f g Y)"
    using assms fibered_product_morphism_monomorphism by auto

  have "fibered_product_morphism X f g Y ∘⇩c y = fibered_product_morphism X f g Y ∘⇩c j"
    using right_eq left_eq cart_prod_eq fibered_product_morphism_type y_type j_type assms comp_type
    by (subst cart_prod_eq[where Z=A, where X=X, where Y=Y], auto)
  then show "j = y"
    using mono assms cfunc_type_def fibered_product_morphism_type j_type y_type
    unfolding monomorphism_def
    by auto 
qed

lemma fibered_product_proj_eq:
  assumes "f : X → Z" "g : Y → Z"
  shows "f ∘⇩c fibered_product_left_proj X f g Y = g ∘⇩c fibered_product_right_proj X f g Y"
    using fibered_product_is_pullback assms
    unfolding is_pullback_def by auto

lemma fibered_product_pair_member:
  assumes "f : X → Z" "g : Y → Z" "x ∈⇩c X" "y ∈⇩c Y"
  shows "(⟨x, y⟩ ∈⇘X ×⇩c Y⇙ (X⇘f⇙×⇩c⇘g⇙Y,  fibered_product_morphism X f g Y)) = (f ∘⇩c x = g ∘⇩c y)"
proof
  assume "⟨x,y⟩ ∈⇘X ×⇩c Y⇙ (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)"
  then obtain h where
    h_type: "h ∈⇩c X⇘f⇙×⇩c⇘g⇙Y" and h_eq: "fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
    unfolding relative_member_def2 factors_through_def
    using assms(3,4) cfunc_prod_type cfunc_type_def by auto
  
  have left_eq: "fibered_product_left_proj X f g Y ∘⇩c h = x"
    unfolding fibered_product_left_proj_def
    using assms h_type
    by (typecheck_cfuncs, smt comp_associative2 h_eq left_cart_proj_cfunc_prod)

  have right_eq: "fibered_product_right_proj X f g Y ∘⇩c h = y"
    unfolding fibered_product_right_proj_def
    using assms h_type
    by (typecheck_cfuncs, smt comp_associative2 h_eq right_cart_proj_cfunc_prod)

  have "f ∘⇩c fibered_product_left_proj X f g Y ∘⇩c h = g ∘⇩c fibered_product_right_proj X f g Y ∘⇩c h"
    using assms h_type by (typecheck_cfuncs, simp add: comp_associative2 fibered_product_proj_eq)
  then show "f ∘⇩c x = g ∘⇩c y"
    using left_eq right_eq by auto
next
  assume f_g_eq: "f ∘⇩c x = g ∘⇩c y"
  show "⟨x,y⟩ ∈⇘X ×⇩c Y⇙ (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)"
    unfolding relative_member_def factors_through_def
  proof (safe)
    show "⟨x,y⟩ ∈⇩c X ×⇩c Y"
      using assms by typecheck_cfuncs
    show "monomorphism (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y))"
      using assms(1,2) fibered_product_morphism_monomorphism by auto
    show "snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) : fst (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) → X ×⇩c Y"
      using assms(1,2) fibered_product_morphism_type by force
    have j_exists: "⋀ Z k h. k : Z → Y ⟹ h : Z → X ⟹ g ∘⇩c k = f ∘⇩c h ⟹
      (∃!j. j : Z → X ⇘f⇙×⇩c⇘g⇙ Y ∧
            fibered_product_right_proj X f g Y ∘⇩c j = k ∧
            fibered_product_left_proj X f g Y ∘⇩c j = h)"
      using fibered_product_is_pullback assms unfolding is_pullback_def by auto

    obtain j where j_type: "j ∈⇩c X ⇘f⇙×⇩c⇘g⇙ Y" and 
      j_projs: "fibered_product_right_proj X f g Y ∘⇩c j = y" "fibered_product_left_proj X f g Y ∘⇩c j = x"
      using j_exists[where Z=𝟭, where k=y, where h=x] assms f_g_eq by auto
    show "∃h. h : domain ⟨x,y⟩ → domain (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)) ∧
           snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) ∘⇩c h = ⟨x,y⟩"
    proof (intro exI[where x=j], safe)
      show "j : domain ⟨x,y⟩ → domain (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y))"
        using assms j_type cfunc_type_def by (typecheck_cfuncs, auto)

      have left_eq: "left_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y ∘⇩c j = x"
        using j_projs assms j_type comp_associative2
        unfolding fibered_product_left_proj_def by (typecheck_cfuncs, auto)

      have right_eq: "right_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y ∘⇩c j = y"
        using j_projs assms j_type comp_associative2
        unfolding fibered_product_right_proj_def by (typecheck_cfuncs, auto)

      show "snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) ∘⇩c j = ⟨x,y⟩"
        using left_eq right_eq assms j_type by (typecheck_cfuncs, simp add: cfunc_prod_unique)
    qed
  qed
qed

lemma fibered_product_pair_member2:
  assumes "f : X → Y" "g : X → E" "x ∈⇩c X" "y ∈⇩c X"
  assumes "g ∘⇩c fibered_product_left_proj X f f X = g ∘⇩c fibered_product_right_proj X f f X"
  shows "∀x y. x ∈⇩c X ⟶ y ∈⇩c X ⟶ ⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⟶ g ∘⇩c x = g ∘⇩c y"
proof(clarify)
  fix x y  
  assume x_type[type_rule]: "x ∈⇩c X"
  assume y_type[type_rule]: "y ∈⇩c X"
  assume a3: "⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
  then obtain h where
    h_type: "h ∈⇩c X⇘f⇙×⇩c⇘f⇙X" and h_eq: "fibered_product_morphism X f f X ∘⇩c h = ⟨x,y⟩"
    by (meson factors_through_def2 relative_member_def2)

  have left_eq: "fibered_product_left_proj X f f X ∘⇩c h = x"
      unfolding fibered_product_left_proj_def
      by (typecheck_cfuncs, smt (z3) assms(1) comp_associative2 h_eq h_type left_cart_proj_cfunc_prod y_type)
    
  have right_eq: "fibered_product_right_proj X f f X ∘⇩c h = y"
    unfolding fibered_product_right_proj_def
    by (typecheck_cfuncs, metis (full_types) a3 comp_associative2 h_eq h_type relative_member_def2 right_cart_proj_cfunc_prod x_type)

  then show "g ∘⇩c x = g ∘⇩c y"
    using assms(1,2,5) cfunc_type_def comp_associative fibered_product_left_proj_type fibered_product_right_proj_type h_type left_eq right_eq by fastforce
qed

lemma kernel_pair_subset:
  assumes "f: X → Y"
  shows "(X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⊆⇩c X ×⇩c X"
  using assms fibered_product_morphism_monomorphism fibered_product_morphism_type subobject_of_def2 by auto

text ‹The three lemmas below correspond to Exercise 2.1.44 in Halvorson.›
lemma kern_pair_proj_iso_TFAE1:
  assumes "f: X → Y" "monomorphism f"
  shows "(fibered_product_left_proj X f f X) = (fibered_product_right_proj X f f X)"
proof (cases "∃x. x∈⇩c X⇘f⇙×⇩c⇘f⇙X", clarify)
  fix x
  assume x_type: "x∈⇩c X⇘f⇙×⇩c⇘f⇙X"
  then have "(f ∘⇩c (fibered_product_left_proj X f f X))∘⇩c x = (f∘⇩c (fibered_product_right_proj X f f X))∘⇩c x"
    using assms cfunc_type_def comp_associative equalizer_def fibered_product_morphism_equalizer
    unfolding fibered_product_right_proj_def fibered_product_left_proj_def
    by (typecheck_cfuncs, smt (verit))
  then have "f ∘⇩c (fibered_product_left_proj X f f X) = f∘⇩c (fibered_product_right_proj X f f X)"
    using assms fibered_product_is_pullback is_pullback_def by auto
  then show "(fibered_product_left_proj X f f X) = (fibered_product_right_proj X f f X)"
    using assms cfunc_type_def fibered_product_left_proj_type fibered_product_right_proj_type monomorphism_def by auto
next
  assume "∄x. x ∈⇩c X ⇘f⇙×⇩c⇘f⇙ X"
  then show "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
    using assms fibered_product_left_proj_type fibered_product_right_proj_type one_separator by blast
qed

lemma kern_pair_proj_iso_TFAE2:
  assumes "f: X → Y" "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
  shows "monomorphism f ∧ isomorphism (fibered_product_left_proj X f f X) ∧ isomorphism (fibered_product_right_proj X f f X)"
  using assms
proof safe
  have "injective f"
    unfolding injective_def
  proof clarify
    fix x y
    assume x_type: "x ∈⇩c domain f" and y_type: "y ∈⇩c domain f"
    then have x_type2: "x ∈⇩c X" and y_type2: "y ∈⇩c X"
      using assms(1) cfunc_type_def by auto

    have x_y_type: "⟨x,y⟩ : 𝟭 → X ×⇩c X"
      using x_type2 y_type2 by (typecheck_cfuncs)
    have fibered_product_type: "fibered_product_morphism X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X ×⇩c X"
      using assms by typecheck_cfuncs

    assume "f ∘⇩c x = f ∘⇩c y"
    then have factorsthru: "⟨x,y⟩ factorsthru fibered_product_morphism X f f X"
      using assms(1) pair_factorsthru_fibered_product_morphism x_type2 y_type2 by auto
    then obtain xy where xy_assms: "xy : 𝟭 → X ⇘f⇙×⇩c⇘f⇙ X" "fibered_product_morphism X f f X ∘⇩c xy = ⟨x,y⟩"
      using factors_through_def2 fibered_product_type x_y_type by blast

    have left_proj: "fibered_product_left_proj X f f X ∘⇩c xy = x"
      unfolding fibered_product_left_proj_def using assms xy_assms
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative left_cart_proj_cfunc_prod x_type2 xy_assms(2) y_type2)
    have right_proj: "fibered_product_right_proj X f f X ∘⇩c xy = y"
      unfolding fibered_product_right_proj_def using assms xy_assms
      by (typecheck_cfuncs, metis cfunc_type_def comp_associative right_cart_proj_cfunc_prod x_type2 xy_assms(2) y_type2)
      
    show "x = y"
      using assms(2) left_proj right_proj by auto
  qed
  then show "monomorphism f"
    using injective_imp_monomorphism by blast
next
  have "diagonal X factorsthru fibered_product_morphism X f f X"
    using assms(1) diagonal_def id_type pair_factorsthru_fibered_product_morphism by fastforce
  then obtain xx where xx_assms: "xx : X → X ⇘f⇙×⇩c⇘f⇙ X" "diagonal X = fibered_product_morphism X f f X ∘⇩c xx"
    using assms(1) cfunc_type_def diagonal_type factors_through_def fibered_product_morphism_type by fastforce
  have eq1: "fibered_product_right_proj X f f X ∘⇩c xx = id X"
    by (smt (z3) assms(1) comp_associative2 diagonal_def fibered_product_morphism_type fibered_product_right_proj_def id_type right_cart_proj_cfunc_prod right_cart_proj_type xx_assms)

  have eq2: "xx ∘⇩c fibered_product_right_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
  proof (rule one_separator[where X="X ⇘f⇙×⇩c⇘f⇙ X", where Y="X ⇘f⇙×⇩c⇘f⇙ X"])
    show "xx ∘⇩c fibered_product_right_proj X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X ⇘f⇙×⇩c⇘f⇙ X"
      using assms(1) comp_type fibered_product_right_proj_type xx_assms by blast
    show "id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) : X ⇘f⇙×⇩c⇘f⇙ X → X ⇘f⇙×⇩c⇘f⇙ X"
      by (simp add: id_type)
  next
    fix x
    assume x_type: "x ∈⇩c X ⇘f⇙×⇩c⇘f⇙ X"
    then obtain a where a_assms: "⟨a,a⟩ = fibered_product_morphism X f f X ∘⇩c x" "a ∈⇩c X"
      by (smt (z3) assms cfunc_prod_comp cfunc_prod_unique comp_type fibered_product_left_proj_def
          fibered_product_morphism_type fibered_product_right_proj_def fibered_product_right_proj_type)

    have "(xx ∘⇩c fibered_product_right_proj X f f X) ∘⇩c x = xx ∘⇩c right_cart_proj X X ∘⇩c ⟨a,a⟩"
      using xx_assms x_type a_assms assms comp_associative2
      unfolding fibered_product_right_proj_def
      by (typecheck_cfuncs, auto)
    also have "... = xx ∘⇩c a"
      using a_assms(2) right_cart_proj_cfunc_prod by auto
    also have "... = x"
    proof -
      have f2: "∀c. c : 𝟭 → X ⟶ fibered_product_morphism X f f X ∘⇩c xx ∘⇩c c = diagonal X ∘⇩c c"
      proof safe
        fix c
        assume "c ∈⇩c X"
        then show "fibered_product_morphism X f f X ∘⇩c xx ∘⇩c c = diagonal X ∘⇩c c"
          using assms xx_assms by (typecheck_cfuncs, simp add: comp_associative2 xx_assms(2))
      qed
      have f4: "xx : X → codomain xx"
        using cfunc_type_def xx_assms by presburger
      have f5: "diagonal X ∘⇩c a = ⟨a,a⟩"
        using a_assms diag_on_elements by blast
      have f6: "codomain (xx ∘⇩c a) = codomain xx"
        using f4 by (meson a_assms cfunc_type_def comp_type)
      then have f9: "x : domain x → codomain xx"
        using cfunc_type_def x_type xx_assms by auto
      have f10: "∀c ca. domain (ca ∘⇩c a) = 𝟭 ∨ ¬ ca : X → c"
        by (meson a_assms cfunc_type_def comp_type)
      then have "domain ⟨a,a⟩ = 𝟭"
        using diagonal_type f5 by force
      then have f11: "domain x = 𝟭"
        using cfunc_type_def x_type by blast
      have "xx ∘⇩c a ∈⇩c codomain xx"
        using a_assms comp_type f4 by auto
      then show ?thesis
        using f11 f9 f5 f2 a_assms assms(1) cfunc_type_def fibered_product_morphism_monomorphism 
              fibered_product_morphism_type monomorphism_def x_type
        by auto
    qed
    also have "... = id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) ∘⇩c x"
      by (metis cfunc_type_def id_left_unit x_type)
    finally show "(xx ∘⇩c fibered_product_right_proj X f f X) ∘⇩c x = id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) ∘⇩c x".
  qed

  show "isomorphism (fibered_product_left_proj X f f X)"
    unfolding isomorphism_def
    by (metis assms cfunc_type_def eq1 eq2 fibered_product_right_proj_type xx_assms(1))

  then show "isomorphism (fibered_product_right_proj X f f X)"
    unfolding isomorphism_def
    using assms(2) isomorphism_def by auto
qed

lemma kern_pair_proj_iso_TFAE3:
  assumes "f: X → Y"
  assumes "isomorphism (fibered_product_left_proj X f f X)" "isomorphism (fibered_product_right_proj X f f X)"
  shows "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
proof -
  obtain q0 where 
    q0_assms: "q0 : X → X ⇘f⇙×⇩c⇘f⇙ X"
      "fibered_product_left_proj X f f X ∘⇩c q0 = id X"
      "q0 ∘⇩c fibered_product_left_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
    using assms(1,2) cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)

  obtain q1 where 
    q1_assms: "q1 : X → X ⇘f⇙×⇩c⇘f⇙ X"
      "fibered_product_right_proj X f f X ∘⇩c q1 = id X"
      "q1 ∘⇩c fibered_product_right_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
    using assms(1,3) cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)

  have "⋀x. x ∈⇩c domain f ⟹ q0 ∘⇩c x = q1 ∘⇩c x"
  proof -
    fix x 
    have fxfx:  "f∘⇩c x = f∘⇩c x"
       by simp
    assume x_type: "x ∈⇩c domain f"
    have factorsthru: "⟨x,x⟩ factorsthru fibered_product_morphism X f f X"
      using assms(1) cfunc_type_def fxfx pair_factorsthru_fibered_product_morphism x_type  by auto
    then obtain xx where xx_assms: "xx : 𝟭 → X ⇘f⇙×⇩c⇘f⇙ X" "⟨x,x⟩ = fibered_product_morphism X f f X ∘⇩c xx"
      by (smt (z3) assms(1) cfunc_type_def diag_on_elements diagonal_type domain_comp factors_through_def factorsthru fibered_product_morphism_type x_type)
      
    have projection_prop: "q0 ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx) = 
                               q1 ∘⇩c ((fibered_product_right_proj X f f X)∘⇩c xx)"
      using q0_assms q1_assms xx_assms assms by (typecheck_cfuncs, simp add: comp_associative2)
    then have fun_fact: "x = ((fibered_product_left_proj X f f X) ∘⇩c q1)∘⇩c (((fibered_product_left_proj X f f X)∘⇩c xx))"
      by (smt (z3) assms(1) cfunc_type_def comp_associative2 fibered_product_left_proj_def
          fibered_product_left_proj_type fibered_product_morphism_type fibered_product_right_proj_def
          fibered_product_right_proj_type id_left_unit2 left_cart_proj_cfunc_prod left_cart_proj_type
          q1_assms right_cart_proj_cfunc_prod right_cart_proj_type x_type xx_assms)
    then have "q1  ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx) = 
             q0  ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx)"
      using q0_assms q1_assms xx_assms assms 
      by (typecheck_cfuncs, smt cfunc_type_def comp_associative2 fibered_product_left_proj_def
          fibered_product_morphism_type fibered_product_right_proj_def left_cart_proj_cfunc_prod
          left_cart_proj_type projection_prop right_cart_proj_cfunc_prod right_cart_proj_type x_type xx_assms(2))
    then show "q0 ∘⇩c x = q1 ∘⇩c x"      
      by (smt (z3) assms(1) cfunc_type_def codomain_comp comp_associative fibered_product_left_proj_type
          fun_fact id_left_unit2 q0_assms q1_assms xx_assms)
  qed
  then have "q0 = q1"
    by (metis assms(1) cfunc_type_def one_separator_contrapos q0_assms(1) q1_assms(1))
  then show "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
    by (smt (z3) assms(1) comp_associative2 fibered_product_left_proj_type fibered_product_right_proj_type
        id_left_unit2 id_right_unit2 q0_assms q1_assms)
qed

lemma terminal_fib_prod_iso:
  assumes "terminal_object(T)"
  assumes f_type: "f : Y → T" 
  assumes g_type: "g : X → T"
  shows "(X ⇘g⇙×⇩c⇘f⇙ Y) ≅ X ×⇩c Y"
proof - 
  have "(is_pullback (X ⇘g⇙×⇩c⇘f⇙ Y) Y X T (fibered_product_right_proj X g f Y) f (fibered_product_left_proj X g f Y) g)"
    using assms pullback_iff_product fibered_product_is_pullback by (typecheck_cfuncs, blast)
  then have "(is_cart_prod (X ⇘g⇙×⇩c⇘f⇙ Y) (fibered_product_left_proj X g f Y) (fibered_product_right_proj X g f Y)  X Y)"
    using assms by (meson one_terminal_object pullback_iff_product terminal_func_type)
  then show ?thesis
    using assms by (metis canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def snd_conv)
qed

end