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 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 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" "xc 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 ⊆⇘XA   
    (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 ∈⇘XB  (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-1B⦈⇘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-1B⦈⇘m)"
  assume h_type: "h : A  (f-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘m⇙]map : f-1B⦈⇘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-1B⦈⇘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-1B⦈⇘m, [f-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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-1B⦈⇘m)  inverse_image_mapping f B m c u = h,k)"
    by auto
  then have "∃!u. u : Z  (f-1B⦈⇘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-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"
  proof (clarify)
    fix u
    assume u_type[type_rule]: "u : Z  (f-1B⦈⇘m)"
    assume u_eq: "inverse_image_mapping f B m c u = h,k"

    show "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"
    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-1B⦈⇘m)"
  assume y_type: "y : Z  (f-1B⦈⇘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-1B⦈⇘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-1B⦈⇘m, left_cart_proj X B c inverse_image_mapping f B m)"
  then obtain h where h_type: "h c (f-1B⦈⇘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-1B⦈⇘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-1B⦈⇘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
  "Xf⇙×cgY = (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 (Xf⇙×cgY) 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 (Xf⇙×cgY) 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 (Xf⇙×cgY) 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 (Xf⇙×cgY) 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 (Xf⇙×cgY) (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 (Xf⇙×cgY) 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 (Xf⇙×cgY) (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 (Xf⇙×cgY) (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 : Xf⇙×cgY  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 : Xf⇙×cgY  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 : Xf⇙×cgY  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 (Xf⇙×cgY) (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  Xf⇙×cgY  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 (Xf⇙×cgY) 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  Xf⇙×cgY  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  Xf⇙×cgY 
           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  Xf⇙×cgY"

    show "j. j : A  Xf⇙×cgY 
           (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  Xf⇙×cgY" and y_type: "y : A  Xf⇙×cgY"
  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(Xf⇙×cgY,  fibered_product_morphism X f g Y)) = (f c x = g c y)"
proof
  assume "x,y ∈⇘X ×c Y(Xf⇙×cgY, fibered_product_morphism X f g Y)"
  then obtain h where
    h_type: "h c Xf⇙×cgY" 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(Xf⇙×cgY, 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 (Xf⇙×cgY, fibered_product_morphism X f g Y))"
      using assms(1,2) fibered_product_morphism_monomorphism by auto
    show "snd (Xf⇙×cgY, fibered_product_morphism X f g Y) : fst (Xf⇙×cgY, 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  Xf⇙×cgY 
            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 Xf⇙×cgY" 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 (Xf⇙×cgY, fibered_product_morphism X f g Y)) 
           snd (Xf⇙×cgY, 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 (Xf⇙×cgY, 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 (Xf⇙×cgY, 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(Xf⇙×cfX, 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(Xf⇙×cfX, fibered_product_morphism X f f X)"
  then obtain h where
    h_type: "h c Xf⇙×cfX" 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 "(Xf⇙×cfX, 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. xc Xf⇙×cfX", clarify)
  fix x
  assume x_type: "xc Xf⇙×cfX"
  then have "(f c (fibered_product_left_proj X f f X))c x = (fc (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) = fc (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 Xf⇙×cfX"
  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 : Xf⇙×cfX  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 : 𝟭  Xf⇙×cfX" "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  Xf⇙×cfX" "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 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 (Xf⇙×cfX)"
  proof (rule one_separator[where X="Xf⇙×cfX", where Y="Xf⇙×cfX"])
    show "xx c fibered_product_right_proj X f f X : Xf⇙×cfX  Xf⇙×cfX"
      using assms(1) comp_type fibered_product_right_proj_type xx_assms by blast
    show "idc (Xf⇙×cfX) : Xf⇙×cfX  Xf⇙×cfX"
      by (simp add: id_type)
  next
    fix x
    assume x_type: "x c Xf⇙×cfX"
    then obtain a where a_assms: "a,a = fibered_product_morphism X f f X c x" "a c X"
      by (smt 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 "... = idc (Xf⇙×cfX) 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 = idc (Xf⇙×cfX) 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  Xf⇙×cfX"
      "fibered_product_left_proj X f f X c q0 = id X"
      "q0 c fibered_product_left_proj X f f X = id (Xf⇙×cfX)"
    using assms(1,2) cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)

  obtain q1 where 
    q1_assms: "q1 : X  Xf⇙×cfX"
      "fibered_product_right_proj X f f X c q1 = id X"
      "q1 c fibered_product_right_proj X f f X = id (Xf⇙×cfX)"
    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:  "fc x = fc 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 : 𝟭  Xf⇙×cfX" "x,x = fibered_product_morphism X f f X c xx"
      by (smt 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 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 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 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 "(Xg⇙×cfY)  X ×c Y"
proof - 
  have "(is_pullback (Xg⇙×cfY) 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 (Xg⇙×cfY) (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