Theory CartesianClosedCategory
chapter "Cartesian Closed Category"
theory CartesianClosedCategory
imports CartesianCategory
begin
text‹
A \emph{cartesian closed category} is a cartesian category such that,
for every object ‹b›, the functor ‹prod ‐ b› is a left adjoint functor.
A right adjoint to this functor takes each object ‹c› to the \emph{exponential}
‹exp b c›. The adjunction yields a natural bijection between ‹hom (prod a b) c›
and ‹hom a (exp b c)›.
›
locale cartesian_closed_category =
cartesian_category +
assumes left_adjoint_prod: "⋀b. ide b ⟹ left_adjoint_functor C C (λx. some_prod x b)"
locale elementary_cartesian_closed_category =
elementary_cartesian_category C pr0 pr1 one trm
for C :: "'a ⇒ 'a ⇒ 'a" (infixr ‹⋅› 55)
and pr0 :: "'a ⇒ 'a ⇒ 'a" (‹𝔭⇩0[_, _]›)
and pr1 :: "'a ⇒ 'a ⇒ 'a" (‹𝔭⇩1[_, _]›)
and one :: "'a" (‹𝟭›)
and trm :: "'a ⇒ 'a" (‹𝗍[_]›)
and exp :: "'a ⇒ 'a ⇒ 'a"
and eval :: "'a ⇒ 'a ⇒ 'a"
and curry :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" +
assumes eval_in_hom: "⟦ ide b; ide c ⟧ ⟹ «eval b c : prod (exp b c) b → c»"
and ide_exp [intro]: "⟦ ide b; ide c ⟧ ⟹ ide (exp b c)"
and curry_in_hom: "⟦ ide a; ide b; ide c; «g : prod a b → c» ⟧
⟹ «curry a b c g : a → exp b c»"
and uncurry_curry: "⟦ ide a; ide b; ide c; «g : prod a b → c» ⟧
⟹ eval b c ⋅ prod (curry a b c g) b = g"
and curry_uncurry: "⟦ ide a; ide b; ide c; «h : a → exp b c» ⟧
⟹ curry a b c (eval b c ⋅ prod h b) = h"
context cartesian_closed_category
begin
interpretation elementary_cartesian_category C some_pr0 some_pr1 ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_cartesian_category by blast
lemma has_exponentials:
assumes "ide b" and "ide c"
shows "∃x e. ide x ∧ «e : prod x b → c» ∧
(∀a g. ide a ∧ «g : prod a b → c» ⟶ (∃!f. «f : a → x» ∧ g = e ⋅ prod f b))"
proof -
interpret F: left_adjoint_functor C C ‹λx. prod x b›
using assms(1) left_adjoint_prod by simp
obtain x e where e: "terminal_arrow_from_functor C C (λx. prod x b) x c e"
using assms F.ex_terminal_arrow [of c] by auto
interpret e: terminal_arrow_from_functor C C ‹λx. prod x b› x c e
using e by simp
have "⋀a g. ⟦ ide a; «g : some_prod a b → c» ⟧ ⟹ ∃!f. «f : a → x» ∧ g = e ⋅ prod f b"
using e.is_terminal category_axioms F.functor_axioms
unfolding e.is_coext_def arrow_from_functor_def arrow_from_functor_axioms_def
by simp
thus ?thesis
using e.arrow by metis
qed
definition some_exp
where "some_exp b c ≡ SOME x. ide x ∧
(∃e. «e : prod x b → c» ∧
(∀a g. ide a ∧ «g : prod a b → c»
⟶ (∃!f. «f : a → x» ∧ g = e ⋅ prod f b)))"
definition some_eval
where "some_eval b c ≡ SOME e. «e : prod (some_exp b c) b → c» ∧
(∀a g. ide a ∧ «g : prod a b → c»
⟶ (∃!f. «f : a → some_exp b c» ∧ g = e ⋅ prod f b))"
definition some_curry
where "some_curry a b c g ≡ THE f. «f : a → some_exp b c» ∧ g = some_eval b c ⋅ prod f b"
lemma curry_uniqueness:
assumes "ide b" and "ide c"
shows "ide (some_exp b c)"
and "«some_eval b c : prod (some_exp b c) b → c»"
and "⟦ ide a; «g : prod a b → c» ⟧ ⟹
∃!f. «f : a → some_exp b c» ∧ g = some_eval b c ⋅ prod f b"
using assms some_exp_def some_eval_def has_exponentials
someI_ex [of "λx. ide x ∧ (∃e. «e : prod x b → c» ∧
(∀a g. ide a ∧ «g : prod a b → c»
⟶ (∃!f. «f : a → x» ∧ g = e ⋅ prod f b)))"]
someI_ex [of "λe. «e : prod (some_exp b c) b → c» ∧
(∀a g. ide a ∧ «g : prod a b → c»
⟶ (∃!f. «f : a → some_exp b c» ∧ g = e ⋅ prod f b))"]
by auto
lemma ide_exp [intro, simp]:
assumes "ide b" and "ide c"
shows "ide (some_exp b c)"
using assms curry_uniqueness(1) by force
lemma eval_in_hom [intro]:
assumes "ide b" and "ide c" and "x = prod (some_exp b c) b"
shows "«some_eval b c : x → c»"
using assms curry_uniqueness by simp
lemma uncurry_curry:
assumes "ide a" and "ide b" and "«g : prod a b → c»"
shows "«some_curry a b c g : a → some_exp b c» ∧
g = some_eval b c ⋅ prod (some_curry a b c g) b"
proof -
have "ide c"
using assms(3) by auto
thus ?thesis
using assms some_curry_def curry_uniqueness
theI' [of "λf. «f : a → some_exp b c» ∧ g = some_eval b c ⋅ prod f b"]
by simp
qed
lemma curry_uncurry:
assumes "ide b" and "ide c" and "«h : a → some_exp b c»"
shows "some_curry a b c (some_eval b c ⋅ prod h b) = h"
proof -
have "∃!f. «f : a → some_exp b c» ∧ some_eval b c ⋅ prod h b = some_eval b c ⋅ prod f b"
proof -
have "ide a ∧ «some_eval b c ⋅ prod h b : prod a b → c»"
proof (intro conjI)
show "ide a"
using assms(3) by auto
show "«some_eval b c ⋅ prod h b : prod a b → c»"
using assms by (intro comp_in_homI) auto
qed
thus ?thesis
using assms curry_uniqueness by simp
qed
moreover have "«h : a → some_exp b c» ∧ some_eval b c ⋅ prod h b = some_eval b c ⋅ prod h b"
using assms by simp
ultimately show ?thesis
using assms some_curry_def curry_uniqueness uncurry_curry
the1_equality [of "λf. «f : a → some_exp b c» ∧
some_eval b c ⋅ prod h b = some_eval b c ⋅ prod f b"]
by simp
qed
interpretation elementary_cartesian_closed_category C some_pr0 some_pr1
‹𝟭⇧?› ‹λa. 𝗍⇧?[a]› some_exp some_eval some_curry
using curry_uniqueness uncurry_curry curry_uncurry
apply unfold_locales by auto
lemma extends_to_elementary_cartesian_closed_category:
shows "elementary_cartesian_closed_category C some_pr0 some_pr1
𝟭⇧? (λa. 𝗍⇧?[a]) some_exp some_eval some_curry"
..
lemma has_as_exponential:
assumes "ide b" and "ide c"
shows "has_as_exponential b c (some_exp b c) (some_eval b c)"
proof
show "ide b" by fact
show "ide (some_exp b c)"
using assms by simp
show "«some_eval b c : some_exp b c ⊗⇧? b → c»"
using assms by auto
show "⋀a g. ⟦ide a; «g : a ⊗⇧? b → c»⟧ ⟹
∃!f. «f : a → some_exp b c» ∧ g = some_eval b c ⋅ (f ⊗⇧? b)"
by (simp add: assms curry_uniqueness(3))
qed
lemma has_as_exponential_iff:
shows "has_as_exponential b c x e ⟷
ide b ∧ «e : some_prod x b → c» ∧
(∃h. «h : x → some_exp b c» ∧ e = some_eval b c ⋅ some_prod h b ∧ iso h)"
proof
assume 1: "has_as_exponential b c x e"
moreover have 2: "has_as_exponential b c (some_exp b c) (some_eval b c)"
using 1 ide_cod has_as_exponential_def in_homE
by (metis has_as_exponential)
ultimately show "ide b ∧ «e : some_prod x b → c» ∧
(∃h. «h : x → some_exp b c» ∧ e = some_eval b c ⋅ some_prod h b ∧ iso h)"
by (metis exponentials_are_isomorphic(2) has_as_exponentialE)
next
assume 1: "ide b ∧ «e : some_prod x b → c» ∧
(∃h. «h : x → some_exp b c» ∧ e = some_eval b c ⋅ some_prod h b ∧ iso h)"
have c: "ide c"
using 1 ide_cod in_homE by metis
have 2: "has_as_exponential b c (some_exp b c) (some_eval b c)"
by (simp add: 1 c eval_in_hom curry_uniqueness(3) has_as_exponential_def)
obtain h where h: "«h : x → some_exp b c» ∧ e = some_eval b c ⋅ some_prod h b ∧ iso h"
using 1 by blast
show "has_as_exponential b c x e"
proof (unfold has_as_exponential_def, intro conjI)
show "ide b" and "ide x" and "«e : some_prod x b → c»"
using 1 h ide_dom by blast+
show "∀y g. ide y ∧ «g : some_prod y b → c»
⟶ (∃!f. «f : y → x» ∧ g = e ⋅ some_prod f b)"
proof (intro allI impI)
fix y g
assume 3: "ide y ∧ «g : some_prod y b → c»"
obtain k where k: "«k : y → some_exp b c» ∧ g = some_eval b c ⋅ some_prod k b"
by (metis 3 ‹ide b› c curry_uniqueness(3))
show "∃!f. «f : y → x» ∧ g = e ⋅ some_prod f b"
proof -
let ?f = "inv h ⋅ k"
have f: "«?f : y → x»"
by (meson comp_in_homI inv_in_hom h k)
moreover have "g = e ⋅ some_prod ?f b"
proof -
have "e ⋅ some_prod ?f b = e ⋅ some_prod (inv h ⋅ k) (b ⋅ b)"
by (simp add: 1)
also have "... = e ⋅ some_prod (inv h) b ⋅ some_prod k b"
by (metis ‹ide b› f arrI comp_ide_self interchange ide_compE)
also have "... = (e ⋅ some_prod (inv h) b) ⋅ some_prod k b"
using comp_assoc by simp
also have "... = some_eval b c ⋅ some_prod k b"
by (metis ‹«e : x ⊗⇧? b → c»› h ‹ide b› arrI inv_prod(1-2) ide_is_iso
inv_ide invert_side_of_triangle(2))
also have "... = g"
using k by blast
finally show ?thesis by blast
qed
moreover have "⋀f'. «f' : y → x» ∧ g = e ⋅ some_prod f' b ⟹ f' = ?f"
proof -
fix f'
assume f': "«f' : y → x» ∧ g = e ⋅ some_prod f' b"
have "«h ⋅ f' : y → some_exp b c» ∧ g = some_eval b c ⋅ some_prod (h ⋅ f') b"
using f' h ‹ide b› comp_assoc interchange seqI' by fastforce
hence "C h f' = C h ?f"
by (metis ‹ide b› arrI c h k cartesian_closed_category.curry_uncurry
cartesian_closed_category_axioms invert_side_of_triangle(1))
thus "f' = ?f"
using f h iso_cancel_left by auto
qed
ultimately show ?thesis by blast
qed
qed
qed
qed
end
context elementary_cartesian_closed_category
begin
lemma left_adjoint_prod:
assumes "ide b"
shows "left_adjoint_functor C C (λx. x ⊗ b)"
proof -
interpret "functor" C C ‹λx. x ⊗ b›
using assms interchange
apply unfold_locales
apply auto
using prod_def tuple_def
by auto
interpret left_adjoint_functor C C ‹λx. x ⊗ b›
proof
show "⋀c. ide c ⟹ ∃x e. terminal_arrow_from_functor C C (λx. x ⊗ b) x c e"
proof -
fix c
assume c: "ide c"
show "∃x e. terminal_arrow_from_functor C C (λx. x ⊗ b) x c e"
proof (intro exI)
interpret arrow_from_functor C C ‹λx. x ⊗ b› ‹exp b c› c ‹eval b c›
using assms c eval_in_hom
by (unfold_locales, auto)
show "terminal_arrow_from_functor C C (λx. x ⊗ b) (exp b c) c (eval b c)"
proof
show "⋀a f. arrow_from_functor C C (λx. x ⊗ b) a c f ⟹
∃!g. arrow_from_functor.is_coext C C
(λx. x ⊗ b) (exp b c) (eval b c) a f g"
proof -
fix a f
assume f: "arrow_from_functor C C (λx. x ⊗ b) a c f"
interpret f: arrow_from_functor C C ‹λx. x ⊗ b› a c f
using f by simp
show "∃!g. is_coext a f g"
proof
have a: "ide a"
using f.arrow by simp
show "is_coext a f (curry a b c f)"
unfolding is_coext_def
using assms a c curry_in_hom uncurry_curry f.arrow by simp
show "⋀g. is_coext a f g ⟹ g = curry a b c f"
unfolding is_coext_def
using assms a c curry_uncurry f.arrow by simp
qed
qed
qed
qed
qed
qed
show ?thesis ..
qed
sublocale cartesian_category C
using is_cartesian_category by simp
sublocale cartesian_closed_category C
proof -
interpret CCC: elementary_cartesian_category
C some_pr0 some_pr1 some_terminal some_terminator
using extends_to_elementary_cartesian_category by blast
show "cartesian_closed_category C"
proof
fix b
assume b: "ide b"
interpret left_adjoint_functor C C ‹λx. CCC.prod x b›
proof -
have "naturally_isomorphic C C (λx. x ⊗ b) (λx. CCC.prod x b)"
proof -
interpret CC: product_category C C ..
interpret X: binary_functor C C C ‹λfg. fst fg ⊗ snd fg›
using binary_functor_Prod(1) by auto
interpret Xb: "functor" C C ‹λx. x ⊗ b›
using b X.fixing_ide_gives_functor_2 by simp
interpret prod: binary_functor C C C ‹λfg. CCC.prod (fst fg) (snd fg)›
using CCC.binary_functor_Prod(1) by simp
interpret prod_b: "functor" C C ‹λx. CCC.prod x b›
using b prod.fixing_ide_gives_functor_2 by simp
interpret φ: transformation_by_components C C ‹λx. x ⊗ b› ‹λx. CCC.prod x b›
‹λa. CCC.tuple 𝔭⇩1[a, b] 𝔭⇩0[a, b]›
using b CCC.prod_tuple by unfold_locales auto
interpret φ: natural_isomorphism C C ‹λx. x ⊗ b› ‹λx. CCC.prod x b› φ.map
proof
fix a
assume a: "ide a"
show "iso (φ.map a)"
proof
show "inverse_arrows (φ.map a) ⟨some_pr1 a b, some_pr0 a b⟩"
using a b by auto
qed
qed
show ?thesis
using naturally_isomorphic_def φ.natural_isomorphism_axioms by blast
qed
moreover have "left_adjoint_functor C C (λx. x ⊗ b)"
using b left_adjoint_prod by simp
ultimately show "left_adjoint_functor C C (λx. CCC.prod x b)"
using left_adjoint_functor_respects_naturally_isomorphic by auto
qed
show "⋀f. ¬ arr f ⟹ some_prod f b = null"
using is_extensional by blast
show "⋀g f. seq g f ⟹ some_prod (g ⋅ f) b = some_prod g b ⋅ some_prod f b"
by simp
show "⋀y. ide y ⟹ ∃x e. terminal_arrow_from_functor (⋅) (⋅) (λx. some_prod x b) x y e"
using ex_terminal_arrow by simp
qed auto
qed
lemma is_cartesian_closed_category:
shows "cartesian_closed_category C"
..
end
end