Theory Cfunc

section ‹Basic Types and Operators for the Category of Sets›

theory Cfunc
  imports Main "HOL-Eisbach.Eisbach"
begin

typedecl cset
typedecl cfunc

text ‹We declare @{type cset} and @{type cfunc} as types to represent the sets and functions within
  ETCS, as distinct from HOL sets and functions.
  The "c" prefix here is intended to stand for "category", and emphasises that these are
  category-theoretic objects.›

text ‹The axiomatization below corresponds to Axiom 1 (Sets Is a Category) in Halvorson.›
axiomatization
  domain :: "cfunc ⇒ cset" and
  codomain :: "cfunc ⇒ cset" and
  comp :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "∘⇩c" 55) and
  id :: "cset ⇒ cfunc" ("id⇩c") 
where
  domain_comp: "domain g = codomain f ⟹ domain (g ∘⇩c f) = domain f" and
  codomain_comp: "domain g = codomain f ⟹ codomain (g ∘⇩c f) = codomain g" and
  comp_associative: "domain h = codomain g ⟹ domain g = codomain f ⟹ h ∘⇩c (g ∘⇩c f) = (h ∘⇩c g) ∘⇩c f" and
  id_domain: "domain (id X) = X" and
  id_codomain: "codomain (id X) = X" and
  id_right_unit: "f ∘⇩c id (domain f) = f" and
  id_left_unit: "id (codomain f) ∘⇩c f = f"


text ‹We define a neater way of stating types and lift the type axioms into lemmas using it.›
definition cfunc_type :: "cfunc ⇒ cset ⇒ cset ⇒ bool" ("_ : _ → _" [50, 50, 50]50) where
  "(f : X → Y) ⟷ (domain f = X ∧ codomain f = Y)"

lemma comp_type:
  "f : X → Y ⟹ g : Y → Z ⟹ g ∘⇩c f : X → Z"
  by (simp add: cfunc_type_def codomain_comp domain_comp)

lemma comp_associative2:
  "f : X → Y ⟹ g : Y → Z ⟹ h : Z → W ⟹ h ∘⇩c (g ∘⇩c f) = (h ∘⇩c g) ∘⇩c f"
  by (simp add: cfunc_type_def comp_associative)

lemma id_type: "id X : X → X"
  unfolding cfunc_type_def using id_domain id_codomain by auto

lemma id_right_unit2: "f : X → Y ⟹ f ∘⇩c id X = f"
  unfolding cfunc_type_def using id_right_unit by auto

lemma id_left_unit2: "f : X → Y ⟹ id Y ∘⇩c f = f"
  unfolding cfunc_type_def using id_left_unit by auto

subsection ‹Tactics for Applying Typing Rules›

text ‹ETCS lemmas often have assumptions on its ETCS type, which can often be cumbersome to prove.
  To simplify proofs involving ETCS types, we provide proof methods that apply type rules in a
  structured way to prove facts about ETCS function types.
  The type rules state the types of the basic constants and operators of ETCS and are declared as
  a named set of theorems called $type\_rule$.›

named_theorems type_rule

declare id_type[type_rule]
declare comp_type[type_rule]

ML_file ‹typecheck.ml›

subsubsection ‹typecheck\_cfuncs: Tactic to Construct Type Facts›

method_setup typecheck_cfuncs =
  ‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> typecheck_cfuncs_method›
  "Check types of cfuncs in current goal and add as assumptions of the current goal"

method_setup typecheck_cfuncs_all =
  ‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> typecheck_cfuncs_all_method›
  "Check types of cfuncs in all subgoals and add as assumptions of the current goal"

method_setup typecheck_cfuncs_prems =
  ‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> typecheck_cfuncs_prems_method›
  "Check types of cfuncs in assumptions of the current goal and add as assumptions of the current goal"

subsubsection ‹etcs\_rule: Tactic to Apply Rules with ETCS Typechecking›

method_setup etcs_rule = 
  ‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
    -- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> ETCS_resolve_method›
  "apply rule with ETCS type checking"

subsubsection ‹etcs\_subst: Tactic to Apply Substitutions with ETCS Typechecking›

method_setup etcs_subst = 
  ‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
    -- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> ETCS_subst_method› 
  "apply substitution with ETCS type checking"

method etcs_assocl declares type_rule = (etcs_subst comp_associative2)+
method etcs_assocr declares type_rule = (etcs_subst sym[OF comp_associative2])+

method_setup etcs_subst_asm = 
  ‹Runtime.exn_trace (fn _ => Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
    -- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> ETCS_subst_asm_method)› 
  "apply substitution to assumptions of the goal, with ETCS type checking"

method etcs_assocl_asm declares type_rule = (etcs_subst_asm comp_associative2)+
method etcs_assocr_asm declares type_rule = (etcs_subst_asm sym[OF comp_associative2])+

subsubsection ‹etcs\_erule: Tactic to Apply Elimination Rules with ETCS Typechecking›

method_setup etcs_erule = 
  ‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
    -- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
     >> ETCS_eresolve_method›
  "apply erule with ETCS type checking"

subsection ‹Monomorphisms, Epimorphisms and Isomorphisms›

subsubsection ‹Monomorphisms›

definition monomorphism :: "cfunc ⇒ bool" where
  "monomorphism f ⟷ (∀ g h. 
    (codomain g = domain f ∧ codomain h = domain f) ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"

lemma monomorphism_def2:
  "monomorphism f ⟷ (∀ g h A X Y. g : A → X ∧ h : A → X ∧ f : X → Y ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"
  unfolding monomorphism_def by (smt cfunc_type_def domain_comp)

lemma monomorphism_def3:
  assumes "f : X → Y"
  shows "monomorphism f ⟷ (∀ g h A. g : A → X ∧ h : A → X ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"
  unfolding monomorphism_def2 using assms cfunc_type_def by auto 

text ‹The lemma below corresponds to Exercise 2.1.7a in Halvorson.›
lemma comp_monic_imp_monic:
  assumes "domain g = codomain f"
  shows "monomorphism (g ∘⇩c f) ⟹ monomorphism f"
  unfolding monomorphism_def
proof clarify
  fix s t
  assume gf_monic: "∀s. ∀t. 
    codomain s = domain (g ∘⇩c f) ∧ codomain t = domain (g ∘⇩c f) ⟶
          (g ∘⇩c f) ∘⇩c s = (g ∘⇩c f) ∘⇩c t ⟶ s = t"
  assume codomain_s: "codomain s = domain f"
  assume codomain_t: "codomain t = domain f"
  assume "f ∘⇩c s = f ∘⇩c t"

  then have "(g ∘⇩c f) ∘⇩c s = (g ∘⇩c f) ∘⇩c t"
    by (metis assms codomain_s codomain_t comp_associative)
  then show "s = t"
    using gf_monic codomain_s codomain_t domain_comp by (simp add: assms)
qed

lemma comp_monic_imp_monic':
  assumes "f : X → Y" "g : Y → Z"
  shows "monomorphism (g ∘⇩c f) ⟹ monomorphism f"
  by (metis assms cfunc_type_def comp_monic_imp_monic)

text ‹The lemma below corresponds to Exercise 2.1.7c in Halvorson.›
lemma composition_of_monic_pair_is_monic:
  assumes "codomain f = domain g"
  shows "monomorphism f ⟹ monomorphism g ⟹ monomorphism (g ∘⇩c f)"
  unfolding monomorphism_def
proof clarify
  fix h k
  assume f_mono: "∀s t. 
    codomain s = domain f ∧ codomain t = domain f ⟶ f ∘⇩c s = f ∘⇩c t ⟶ s = t"
  assume g_mono: "∀s. ∀t. 
    codomain s = domain g ∧ codomain t = domain g ⟶ g ∘⇩c s = g ∘⇩c t ⟶ s = t"
  assume codomain_k: "codomain k = domain (g ∘⇩c f)"
  assume codomain_h: "codomain h = domain (g ∘⇩c f)"
  assume gfh_eq_gfk: "(g ∘⇩c f) ∘⇩c k = (g ∘⇩c f) ∘⇩c h"
 
  have "g ∘⇩c (f ∘⇩c h) = (g  ∘⇩c f)  ∘⇩c h"
    by (simp add: assms codomain_h comp_associative domain_comp)
  also have "... = (g ∘⇩c f) ∘⇩c k"
    by (simp add: gfh_eq_gfk)
  also have "... = g ∘⇩c (f ∘⇩c k)"
    by (simp add: assms codomain_k comp_associative domain_comp)
  ultimately have "f ∘⇩c h = f ∘⇩c k"
    using assms cfunc_type_def codomain_h codomain_k comp_type domain_comp g_mono by auto
  then show "k = h"
    by (simp add: codomain_h codomain_k domain_comp f_mono assms)
qed

subsubsection ‹Epimorphisms›

definition epimorphism :: "cfunc ⇒ bool" where
  "epimorphism f ⟷ (∀ g h. 
    (domain g = codomain f ∧ domain h = codomain f) ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"

lemma epimorphism_def2:
  "epimorphism f ⟷ (∀ g h A X Y. f : X → Y ∧ g : Y → A ∧ h : Y → A ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"
  unfolding epimorphism_def by (smt cfunc_type_def codomain_comp) 

lemma epimorphism_def3:
  assumes "f : X → Y"
  shows "epimorphism f ⟷ (∀ g h A. g : Y → A ∧ h : Y → A ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"
  unfolding epimorphism_def2 using assms cfunc_type_def by auto

text ‹The lemma below corresponds to Exercise 2.1.7b in Halvorson.›
lemma comp_epi_imp_epi:
  assumes "domain g = codomain f"
  shows "epimorphism (g ∘⇩c f) ⟹ epimorphism g"
  unfolding epimorphism_def
proof clarify
  fix s t
  assume gf_epi: "∀s. ∀t.
    domain s = codomain (g ∘⇩c f) ∧ domain t = codomain (g ∘⇩c f) ⟶
          s ∘⇩c g ∘⇩c f = t ∘⇩c g ∘⇩c f ⟶ s = t"
  assume domain_s: "domain s = codomain g"
  assume domain_t: "domain t = codomain g"
  assume sf_eq_tf: "s ∘⇩c g = t ∘⇩c g"

  from sf_eq_tf have "s ∘⇩c (g ∘⇩c f) = t ∘⇩c (g ∘⇩c f)"
    by (simp add: assms comp_associative domain_s domain_t)
  then show "s = t"
    using gf_epi codomain_comp domain_s domain_t by (simp add: assms)
qed

text ‹The lemma below corresponds to Exercise 2.1.7d in Halvorson.›
lemma composition_of_epi_pair_is_epi:
assumes "codomain f = domain g"
  shows "epimorphism f ⟹ epimorphism g ⟹ epimorphism (g ∘⇩c f)"
  unfolding epimorphism_def
proof clarify
  fix h k
  assume f_epi :"∀ s h.
    (domain s = codomain f ∧ domain h = codomain f) ⟶ (s ∘⇩c f = h ∘⇩c f ⟶ s = h)"
  assume g_epi :"∀ s h.
    (domain s = codomain g ∧ domain h = codomain g) ⟶ (s ∘⇩c g = h ∘⇩c g ⟶ s = h)"
  assume domain_k: "domain k = codomain (g ∘⇩c f)"
  assume domain_h: "domain h = codomain (g ∘⇩c f)"
  assume hgf_eq_kgf: "h ∘⇩c (g ∘⇩c f) = k ∘⇩c (g ∘⇩c f)"
  
  have "(h ∘⇩c g) ∘⇩c f = h ∘⇩c (g ∘⇩c f)"
    by (simp add: assms codomain_comp comp_associative domain_h)
  also have "... = k ∘⇩c (g ∘⇩c f)"
    by (simp add: hgf_eq_kgf)
  also have "... =(k ∘⇩c g) ∘⇩c f "
    by (simp add: assms codomain_comp comp_associative domain_k)
  ultimately have "h ∘⇩c g = k ∘⇩c g"
    by (simp add: assms codomain_comp domain_comp domain_h domain_k f_epi)
  then show "h = k"
    by (simp add: codomain_comp domain_h domain_k g_epi assms)
qed

subsubsection ‹Isomorphisms›

definition isomorphism :: "cfunc ⇒ bool" where
  "isomorphism f ⟷ (∃ g. domain g = codomain f ∧ codomain g = domain f ∧ 
    g ∘⇩c f = id(domain f) ∧ f ∘⇩c g = id(domain g))"

lemma isomorphism_def2:
  "isomorphism f ⟷ (∃ g X Y. f : X → Y ∧ g : Y → X ∧ g ∘⇩c f = id X ∧ f ∘⇩c g = id Y)"
  unfolding isomorphism_def cfunc_type_def by auto

lemma isomorphism_def3:
  assumes "f : X → Y"
  shows "isomorphism f ⟷ (∃ g. g : Y → X ∧ g ∘⇩c f = id X ∧ f ∘⇩c g = id Y)"
  using assms unfolding isomorphism_def2 cfunc_type_def by auto

definition inverse :: "cfunc ⇒ cfunc" ("_❙¯" [1000] 999) where
  "inverse f = (THE g. g : codomain f → domain f ∧ g ∘⇩c f = id(domain f) ∧ f ∘⇩c g = id(codomain f))"

lemma inverse_def2:
  assumes "isomorphism f"
  shows "f❙¯ : codomain f → domain f ∧ f❙¯ ∘⇩c f = id(domain f) ∧ f ∘⇩c f❙¯ = id(codomain f)"
  unfolding inverse_def
proof (rule theI', safe)
  show "∃g. g : codomain f → domain f ∧ g ∘⇩c f = id⇩c (domain f) ∧ f ∘⇩c g = id⇩c (codomain f)"
    using assms unfolding isomorphism_def cfunc_type_def by auto
next
  fix g1 g2
  assume g1_f: "g1 ∘⇩c f = id⇩c (domain f)" and f_g1: "f ∘⇩c g1 = id⇩c (codomain f)"
  assume g2_f: "g2 ∘⇩c f = id⇩c (domain f)" and f_g2: "f ∘⇩c g2 = id⇩c (codomain f)"
  assume "g1 : codomain f → domain f" "g2 : codomain f → domain f"
  then have "codomain g1 = domain f" "domain g2 = codomain f"
    unfolding cfunc_type_def by auto
  then show "g1 = g2"
    by (metis comp_associative f_g1 g2_f id_left_unit id_right_unit)
qed

lemma inverse_type[type_rule]:
  assumes "isomorphism f" "f : X → Y"
  shows "f❙¯ : Y → X"
  using assms inverse_def2 unfolding cfunc_type_def by auto

lemma inv_left:
  assumes "isomorphism f" "f : X → Y"
  shows "f❙¯ ∘⇩c f = id X"
  using assms inverse_def2 unfolding cfunc_type_def by auto

lemma inv_right:
  assumes "isomorphism f" "f : X → Y"
  shows "f ∘⇩c f❙¯ = id Y"
  using assms inverse_def2 unfolding cfunc_type_def by auto

lemma inv_iso:
  assumes "isomorphism f"
  shows "isomorphism(f❙¯)"
  using assms inverse_def2 unfolding isomorphism_def cfunc_type_def by (intro exI[where x=f], auto)

lemma inv_idempotent:
  assumes "isomorphism f"
  shows "(f❙¯)❙¯ = f"
  by (smt assms cfunc_type_def comp_associative id_left_unit inv_iso inverse_def2)

definition is_isomorphic :: "cset ⇒ cset ⇒ bool" (infix "≅" 50)  where
  "X ≅ Y ⟷ (∃ f. f : X → Y ∧ isomorphism f)"

lemma id_isomorphism: "isomorphism (id X)"
  unfolding isomorphism_def
  by (intro exI[where x= "id X"], auto simp add: id_codomain id_domain, metis id_domain id_right_unit)

lemma isomorphic_is_reflexive: "X ≅ X"
  unfolding is_isomorphic_def
  by (intro exI[where x= "id X"], auto simp add: id_domain id_codomain id_isomorphism id_type)

lemma isomorphic_is_symmetric: "X ≅ Y ⟶ Y ≅ X"
  unfolding is_isomorphic_def isomorphism_def 
  by (auto, metis cfunc_type_def)

lemma isomorphism_comp: 
  "domain f = codomain g ⟹ isomorphism f ⟹ isomorphism g ⟹ isomorphism (f ∘⇩c g)"
  unfolding isomorphism_def by (auto, smt codomain_comp comp_associative domain_comp id_right_unit)

lemma isomorphism_comp': 
  assumes "f : Y → Z" "g : X → Y"
  shows "isomorphism f ⟹ isomorphism g ⟹ isomorphism (f ∘⇩c g)"
  using assms cfunc_type_def isomorphism_comp by auto

lemma isomorphic_is_transitive: "(X ≅ Y ∧ Y ≅ Z) ⟶ X ≅ Z"
  unfolding is_isomorphic_def by (auto, metis cfunc_type_def comp_type isomorphism_comp)

lemma is_isomorphic_equiv:
  "equiv UNIV {(X, Y). X ≅ Y}"
  unfolding equiv_def
proof safe
  show "refl {(x, y). x ≅ y}"
    unfolding refl_on_def using isomorphic_is_reflexive by auto
next
  show "sym {(x, y). x ≅ y}"
    unfolding sym_def using isomorphic_is_symmetric by blast
next
  show "trans {(x, y). x ≅ y}"
    unfolding trans_def using isomorphic_is_transitive by blast
qed

text ‹The lemma below corresponds to Exercise 2.1.7e in Halvorson.›
lemma iso_imp_epi_and_monic:
  "isomorphism f ⟹ epimorphism f ∧ monomorphism f"
  unfolding isomorphism_def epimorphism_def monomorphism_def
proof safe
  fix g s t
  assume domain_g: "domain g = codomain f"
  assume codomain_g: "codomain g = domain f"
  assume gf_id: "g ∘⇩c f = id (domain f)"
  assume fg_id: "f ∘⇩c g = id (domain g)"
  assume domain_s: "domain s = codomain f"
  assume domain_t: "domain t = codomain f"
  assume sf_eq_tf: "s ∘⇩c f = t ∘⇩c f"

  have "s = s ∘⇩c id(codomain(f))"
    by (metis domain_s id_right_unit)
  also have "... = s ∘⇩c (f ∘⇩c g)"
    by (simp add: domain_g fg_id)
  also have "... = (s ∘⇩c f) ∘⇩c g"
    by (simp add: codomain_g comp_associative domain_s)
  also have "... = (t ∘⇩c f) ∘⇩c g"
    by (simp add: sf_eq_tf)
  also have "... = t ∘⇩c (f ∘⇩c g)"
    by (simp add: codomain_g comp_associative domain_t)
  also have "... = t ∘⇩c id(codomain f)"
    by (simp add: domain_g fg_id)
  also have "... = t"
    by (metis domain_t id_right_unit)    
  finally show "s = t".
next
  fix g h k
  assume domain_g: "domain g = codomain f"
  assume codomain_g: "codomain g = domain f"
  assume gf_id: "g ∘⇩c f = id (domain f)"
  assume fg_id: "f ∘⇩c g = id (domain g)"
  assume codomain_h: "codomain h = domain f"
  assume codomain_k: "codomain k = domain f"
  assume fk_eq_fh: "f ∘⇩c k = f ∘⇩c h"

  have "h = id(domain f) ∘⇩c h"
    by (metis codomain_h id_left_unit)
  also have "... = (g ∘⇩c f) ∘⇩c h"
    using gf_id by auto
  also have "... = g ∘⇩c (f ∘⇩c h)"
    by (simp add: codomain_h comp_associative domain_g)
  also have "... = g ∘⇩c (f ∘⇩c k)"
    by (simp add: fk_eq_fh)
  also have "... = (g ∘⇩c f) ∘⇩c k"
    by (simp add: codomain_k comp_associative domain_g)
  also have "... = id(domain f) ∘⇩c k"
    by (simp add: gf_id)
  also have "... = k"
    by (metis codomain_k id_left_unit)
  ultimately show "k = h"
    by simp
qed

lemma isomorphism_sandwich: 
  assumes f_type: "f : A → B" and g_type: "g : B → C" and h_type: "h: C → D"
  assumes f_iso: "isomorphism f"
  assumes h_iso: "isomorphism h"
  assumes hgf_iso: "isomorphism(h ∘⇩c g ∘⇩c f)"
  shows "isomorphism g"
proof -
  have "isomorphism(h❙¯ ∘⇩c (h ∘⇩c g ∘⇩c f) ∘⇩c f❙¯)"
    using assms by (typecheck_cfuncs, simp add: f_iso h_iso hgf_iso inv_iso isomorphism_comp')
  then show "isomorphism g"
    using assms by (typecheck_cfuncs_prems, smt comp_associative2 id_left_unit2 id_right_unit2 inv_left inv_right)
qed

end