Theory ClosedMonoidalCategory
text‹
A \emph{closed monoidal category} is a monoidal category such that
for every object ‹b›, the functor ‹‐ ⊗ 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 (- ⊗ b) c›
and ‹hom - (exp b c)›.
In enriched category theory, the notion of ``hom-set'' from classical category
theory is generalized to that of ``hom-object'' in a monoidal category.
When the monoidal category in question is closed, much of the theory of
set-based categories can be reproduced in the more general enriched setting.
The main purpose of this section is to prepare the way for such a development;
in particular we do the main work required to show that a closed monoidal category
is ``enriched in itself.''
›
theory ClosedMonoidalCategory
imports MonoidalCategory.CartesianMonoidalCategory
begin
section "Definition and Basic Facts"
text ‹
As is pointed out in \<^cite>‹"nlab-internal-hom"›,
unless symmetry is assumed as part of the definition, there are in fact two notions
of closed monoidal category: \emph{left}-closed monoidal category and
\emph{right}-closed monoidal category.
Here we define versions with and without symmetry, so that we can identify the places
where symmetry is actually required.
›
locale closed_monoidal_category =
monoidal_category +
assumes left_adjoint_tensor: "⋀b. ide b ⟹ left_adjoint_functor C C (λx. x ⊗ b)"
locale closed_symmetric_monoidal_category =
closed_monoidal_category +
symmetric_monoidal_category
text‹
Similarly to what we have done in previous work, besides the definition of
@{locale closed_monoidal_category}, which adds an assumed property to
@{locale monoidal_category} but not any additional structure, we find it convenient
also to define ‹elementary_closed_monoidal_category›, which assumes particular
exponential structure to have been chosen, and uses this given structure to express
the properties of a closed monoidal category in a more elementary way.
›
locale elementary_closed_monoidal_category =
monoidal_category +
fixes exp :: "'a ⇒ 'a ⇒ 'a"
and eval :: "'a ⇒ 'a ⇒ 'a"
and Curry :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
assumes eval_in_hom_ax: "⟦ ide b; ide c ⟧ ⟹ «eval b c : exp b c ⊗ b → c»"
and ide_exp [intro, simp]: "⟦ ide b; ide c ⟧ ⟹ ide (exp b c)"
and Curry_in_hom_ax: "⟦ ide a; ide b; ide c; «g : a ⊗ b → c» ⟧
⟹ «Curry a b c g : a → exp b c»"
and Uncurry_Curry: "⟦ ide a; ide b; ide c; «g : a ⊗ b → c» ⟧
⟹ eval b c ⋅ (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 ⋅ (h ⊗ b)) = h"
locale elementary_closed_symmetric_monoidal_category =
symmetric_monoidal_category +
elementary_closed_monoidal_category
begin
sublocale elementary_symmetric_monoidal_category
C tensor ℐ lunit runit assoc sym
using induces_elementary_symmetric_monoidal_category⇩C⇩M⇩C by blast
end
text‹
We now show that, except for the fact that a particular choice of structure has been made,
closed monoidal categories and elementary closed monoidal categories amount to the
same thing.
›
subsection "An ECMC is a CMC"
context elementary_closed_monoidal_category
begin
notation Curry (‹Curry[_, _, _]›)
abbreviation Uncurry (‹Uncurry[_, _]›)
where "Uncurry[b, c] f ≡ eval b c ⋅ (f ⊗ b)"
lemma Curry_in_hom [intro]:
assumes "ide a" and "ide b" and "«g : a ⊗ b → c»" and "y = exp b c"
shows "«Curry[a, b, c] g : a → y»"
using assms Curry_in_hom_ax [of a b c g] by fastforce
lemma Curry_simps [simp]:
assumes "ide a" and "ide b" and "«g : a ⊗ b → c»"
shows "arr (Curry[a, b, c] g)"
and "dom (Curry[a, b, c] g) = a"
and "cod (Curry[a, b, c] g) = exp b c"
using assms Curry_in_hom by blast+
lemma eval_in_hom⇩E⇩C⇩M⇩C [intro]:
assumes "ide b" and "ide c" and "x = exp b c ⊗ b"
shows "«eval b c : x → c»"
using assms eval_in_hom_ax by blast
lemma eval_simps [simp]:
assumes "ide b" and "ide c"
shows "arr (eval b c)" and "dom (eval b c) = exp b c ⊗ b" and "cod (eval b c) = c"
using assms eval_in_hom⇩E⇩C⇩M⇩C by blast+
lemma Uncurry_in_hom [intro]:
assumes "ide b" and "ide c" and "«f : a → exp b c»" and "x = a ⊗ b"
shows "«Uncurry[b, c] f : x → c»"
using assms by auto
lemma Uncurry_simps [simp]:
assumes "ide b" and "ide c" and "«f : a → exp b c»"
shows "arr (Uncurry[b, c] f)"
and "dom (Uncurry[b, c] f) = a ⊗ b"
and "cod (Uncurry[b, c] f) = c"
using assms Uncurry_in_hom by blast+
lemma Uncurry_exp:
assumes "ide a" and "ide b"
shows "Uncurry[a, b] (exp a b) = eval a b"
using assms
by (metis comp_arr_dom eval_in_hom⇩E⇩C⇩M⇩C in_homE)
lemma comp_Curry_arr:
assumes "ide b" and "«f : x → a»" and "«g : a ⊗ b → c»"
shows "Curry[a, b, c] g ⋅ f = Curry[x, b, c] (g ⋅ (f ⊗ b))"
proof -
have a: "ide a" and c: "ide c" and x: "ide x"
using assms(2-3) by auto
have "Curry[a, b, c] g ⋅ f =
Curry[x, b, c] (Uncurry[b, c] (Curry[a, b, c] g ⋅ f))"
using assms(1-3) a c x Curry_Uncurry comp_in_homI Curry_in_hom
by presburger
also have "... = Curry[x, b, c] (eval b c ⋅ (Curry[a, b, c] g ⊗ b) ⋅ (f ⊗ b))"
using assms a c interchange
by (metis comp_ide_self Curry_in_hom ideD(1) seqI')
also have "... = Curry[x, b, c] (Uncurry[b, c] (Curry[a, b, c] g) ⋅ (f ⊗ b))"
using comp_assoc by simp
also have "... = Curry[x, b, c] (g ⋅ (f ⊗ b))"
using a c assms(1,3) Uncurry_Curry by simp
finally show ?thesis by blast
qed
lemma terminal_arrow_from_functor_eval:
assumes "ide b" and "ide c"
shows "terminal_arrow_from_functor C C (λx. T (x, b)) (exp b c) c (eval b c)"
proof -
interpret "functor" C C ‹λx. T (x, b)›
using assms(1) interchange T.is_extensional
by unfold_locales auto
interpret arrow_from_functor C C ‹λx. T (x, b)› ‹exp b c› c ‹eval b c›
using assms eval_in_hom⇩E⇩C⇩M⇩C
by unfold_locales auto
show ?thesis
proof
show "⋀a f. arrow_from_functor C C (λx. T (x, b)) a c f ⟹
∃!g. arrow_from_functor.is_coext C C
(λx. T (x, b)) (exp b c) (eval b c) a f g"
proof -
fix a f
assume f: "arrow_from_functor C C (λx. T (x, b)) a c f"
interpret f: arrow_from_functor C C ‹λx. T (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 Curry_in_hom Uncurry_Curry f.arrow by force
show "⋀g. is_coext a f g ⟹ g = Curry[a, b, c] f"
unfolding is_coext_def
using assms a Curry_Uncurry f.arrow arrI by force
qed
qed
qed
qed
lemma is_closed_monoidal_category:
shows "closed_monoidal_category C T α ι"
using T.is_extensional interchange terminal_arrow_from_functor_eval
apply unfold_locales
apply auto[5]
by metis
lemma retraction_eval_ide_self:
assumes "ide a"
shows "retraction (eval a a)"
by (metis Uncurry_Curry assms comp_lunit_lunit'(1) ide_unity comp_assoc
lunit_in_hom retractionI)
end
context elementary_closed_symmetric_monoidal_category
begin
lemma is_closed_symmetric_monoidal_category:
shows "closed_symmetric_monoidal_category C T α ι σ"
by (simp add: closed_symmetric_monoidal_category.intro
is_closed_monoidal_category symmetric_monoidal_category_axioms)
end
subsection "A CMC Extends to an ECMC"
context closed_monoidal_category
begin
lemma has_exponentials:
assumes "ide b" and "ide c"
shows "∃x e. ide x ∧ «e : x ⊗ b → c» ∧
(∀a g. ide a ∧
«g : a ⊗ b → c» ⟶ (∃!f. «f : a → x» ∧ g = e ⋅ (f ⊗ b)))"
proof -
interpret F: left_adjoint_functor C C ‹λx. x ⊗ b›
using assms(1) left_adjoint_tensor by simp
obtain x e where e: "terminal_arrow_from_functor C C (λx. x ⊗ b) x c e"
using assms F.ex_terminal_arrow [of c] by auto
interpret e: terminal_arrow_from_functor C C ‹λx. x ⊗ b› x c e
using e by simp
have "⋀a g. ⟦ ide a; «g : a ⊗ b → c» ⟧
⟹ ∃!f. «f : a → x» ∧ g = e ⋅ (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 (‹exp⇧?›)
where "exp⇧? b c ≡ SOME x. ide x ∧
(∃e. «e : x ⊗ b → c» ∧
(∀a g. ide a ∧ «g : a ⊗ b → c»
⟶ (∃!f. «f : a → x» ∧ g = e ⋅ (f ⊗ b))))"
definition some_eval (‹eval⇧?›)
where "eval⇧? b c ≡ SOME e. «e : exp⇧? b c ⊗ b → c» ∧
(∀a g. ide a ∧ «g : a ⊗ b → c»
⟶ (∃!f. «f : a → exp⇧? b c» ∧ g = e ⋅ (f ⊗ b)))"
definition some_Curry (‹Curry⇧?[_, _, _]›)
where "Curry⇧?[a, b, c] g ≡
THE f. «f : a → exp⇧? b c» ∧ g = eval⇧? b c ⋅ (f ⊗ b)"
abbreviation some_Uncurry (‹Uncurry⇧?[_, _]›)
where "Uncurry⇧?[b, c] f ≡ eval⇧? b c ⋅ (f ⊗ b)"
lemma Curry_uniqueness:
assumes "ide b" and "ide c"
shows "ide (exp⇧? b c)" and "«eval⇧? b c : exp⇧? b c ⊗ b → c»"
and "⟦ ide a; «g : a ⊗ b → c» ⟧
⟹ ∃!f. «f : a → exp⇧? b c» ∧ g = Uncurry⇧?[b, c] f"
using assms some_exp_def some_eval_def has_exponentials
someI_ex [of "λx. ide x ∧ (∃e. «e : x ⊗ b → c» ∧
(∀a g. ide a ∧ «g : a ⊗ b → c»
⟶ (∃!f. «f : a → x» ∧ g = e ⋅ (f ⊗ b))))"]
someI_ex [of "λe. «e : exp⇧? b c ⊗ b → c» ∧
(∀a g. ide a ∧ «g : a ⊗ b → c»
⟶ (∃!f. «f : a → exp⇧? b c» ∧ g = e ⋅ (f ⊗ b)))"]
by auto
lemma some_eval_in_hom [intro]:
assumes "ide b" and "ide c" and "x = exp⇧? b c ⊗ b"
shows "«eval⇧? b c : x → c»"
using assms Curry_uniqueness by simp
lemma some_Uncurry_some_Curry:
assumes "ide a" and "ide b" and "«g : a ⊗ b → c»"
shows "«Curry⇧?[a, b, c] g : a → exp⇧? b c»"
and "Uncurry⇧?[b, c] (Curry⇧?[a, b, c] g) = g"
proof -
have "ide c"
using assms(3) by auto
hence 1: "«Curry⇧?[a, b, c] g : a → exp⇧? b c» ∧
g = Uncurry⇧?[b, c] (Curry⇧?[a, b, c] g)"
using assms some_Curry_def Curry_uniqueness
theI' [of "λf. «f : a → exp⇧? b c» ∧ g = Uncurry⇧?[b, c] f"]
by simp
show "«Curry⇧?[a, b, c] g : a → exp⇧? b c»"
using 1 by simp
show "Uncurry⇧?[b, c] (Curry⇧?[a, b, c] g) = g"
using 1 by simp
qed
lemma some_Curry_some_Uncurry:
assumes "ide b" and "ide c" and "«h : a → exp⇧? b c»"
shows "Curry⇧?[a, b, c] (Uncurry⇧?[b, c] h) = h"
proof -
have "∃!f. «f : a → exp⇧? b c» ∧ Uncurry⇧?[b, c] h = Uncurry⇧?[b, c] f"
using assms ide_dom ide_in_hom
Curry_uniqueness(3) [of b c a "Uncurry⇧?[b, c] h"]
by auto
moreover have "«h : a → exp⇧? b c» ∧ Uncurry⇧?[b, c] h = Uncurry⇧?[b, c] h"
using assms by simp
ultimately show ?thesis
using assms some_Curry_def Curry_uniqueness some_Uncurry_some_Curry
the1_equality [of "λf. «f : a → some_exp b c» ∧
Uncurry⇧?[b, c] h = Uncurry⇧?[b, c] f"]
by simp
qed
lemma extends_to_elementary_closed_monoidal_category⇩C⇩M⇩C:
shows "elementary_closed_monoidal_category
C T α ι some_exp some_eval some_Curry"
using Curry_uniqueness some_Uncurry_some_Curry
some_Curry_some_Uncurry
by unfold_locales auto
end
context closed_symmetric_monoidal_category
begin
lemma extends_to_elementary_closed_symmetric_monoidal_category⇩C⇩M⇩C:
shows "elementary_closed_symmetric_monoidal_category
C T α ι σ some_exp some_eval some_Curry"
by (simp add: elementary_closed_symmetric_monoidal_category_def
extends_to_elementary_closed_monoidal_category⇩C⇩M⇩C
symmetric_monoidal_category_axioms)
end
section "Internal Hom Functors"
text ‹
For each object ‹x› of a closed monoidal category ‹C›, we can define a covariant
endofunctor ‹Exp⇧→ x -› of ‹C›, which takes each arrow ‹g› to an arrow
‹«Exp⇧→ x g : exp x (dom g) → exp x (cod g)»›. Similarly, for each object ‹y›,
we can define a contravariant endofunctor ‹Exp⇧← - y› of ‹C›, which takes each arrow
‹f› of ‹C⇧o⇧p› to an arrow ‹«Exp⇧← f y : exp (cod f) y → exp (dom f) y»› of ‹C›.
These two endofunctors commute with each other and compose to form a single binary
``internal hom'' functor ‹Exp› from ‹C⇧o⇧p × C› to ‹C›.
›
context elementary_closed_monoidal_category
begin
abbreviation cov_Exp (‹Exp⇧→›)
where "Exp⇧→ x g ≡ if arr g
then Curry[exp x (dom g), x, cod g] (g ⋅ eval x (dom g))
else null"
abbreviation cnt_Exp (‹Exp⇧←›)
where "Exp⇧← f y ≡ if arr f
then Curry[exp (cod f) y, dom f, y]
(eval (cod f) y ⋅ (exp (cod f) y ⊗ f))
else null"
lemma cov_Exp_in_hom:
assumes "ide x" and "arr g"
shows "«Exp⇧→ x g : exp x (dom g) → exp x (cod g)»"
using assms by auto
lemma cnt_Exp_in_hom:
assumes "arr f" and "ide y"
shows "«Exp⇧← f y : exp (cod f) y → exp (dom f) y»"
using assms by force
lemma cov_Exp_ide:
assumes "ide a" and "ide b"
shows "Exp⇧→ a b = exp a b"
using assms
by (metis comp_ide_arr Curry_Uncurry eval_in_hom⇩E⇩C⇩M⇩C ideD(2-3) ide_exp
ide_in_hom seqI' Uncurry_exp)
lemma cnt_Exp_ide:
assumes "ide a" and "ide b"
shows "Exp⇧← a b = exp a b"
using assms Curry_Uncurry ide_exp ide_in_hom by force
lemma cov_Exp_comp:
assumes "ide x" and "seq g f"
shows "Exp⇧→ x (g ⋅ f) = Exp⇧→ x g ⋅ Exp⇧→ x f"
proof -
have "Exp⇧→ x g ⋅ Exp⇧→ x f =
Curry[exp x (cod f), x, cod g] (g ⋅ eval x (cod f)) ⋅
Curry[exp x (dom f), x, cod f] (f ⋅ eval x (dom f))"
using assms by auto
also have "... = Curry[exp x (dom f), x, cod g]
((g ⋅ eval x (dom g)) ⋅
(Curry[exp x (dom f), x, cod f] (f ⋅ eval x (dom f)) ⊗ x))"
using assms cov_Exp_in_hom comp_Curry_arr by auto
also have "... = Exp⇧→ x (g ⋅ f)"
using assms Uncurry_Curry comp_assoc by fastforce
finally show ?thesis by simp
qed
lemma cnt_Exp_comp:
assumes "seq g f" and "ide y"
shows "Exp⇧← (g ⋅ f) y = Exp⇧← f y ⋅ Exp⇧← g y"
proof -
have "Exp⇧← f y ⋅ Exp⇧← g y =
Curry[exp (cod g) y, dom f, y]
((eval (cod f) y ⋅ (exp (cod f) y ⊗ f)) ⋅
(Curry[exp (cod g) y, cod f, y]
(eval (cod g) y ⋅ (exp (cod g) y ⊗ g)) ⊗ dom f))"
using assms
comp_Curry_arr
[of "dom f" "Curry[exp (cod g) y, cod f, y]
(eval (cod g) y ⋅ (exp (cod g) y ⊗ g))"]
by fastforce
also have "... = Curry[exp (cod g) y, dom f, y]
((Uncurry[cod f, y]
(Curry[exp (cod g) y, cod f, y]
(eval (cod g) y ⋅ (exp (cod g) y ⊗ g)))) ⋅
(exp (cod g) y ⊗ f))"
using assms interchange comp_arr_dom comp_cod_arr comp_assoc by auto
also have "... = Curry[exp (cod g) y, dom f, y]
((eval (cod g) y ⋅ (exp (cod g) y ⊗ g)) ⋅ (exp (cod g) y ⊗ f))"
using assms Uncurry_Curry by auto
also have "... = Exp⇧← (g ⋅ f) y"
using assms interchange comp_assoc by auto
finally show ?thesis by simp
qed
lemma functor_cov_Exp:
assumes "ide x"
shows "functor C C (Exp⇧→ x)"
using assms cov_Exp_ide cov_Exp_in_hom cov_Exp_comp
by unfold_locales auto
interpretation Cop: dual_category C ..
lemma functor_cnt_Exp:
assumes "ide x"
shows "functor Cop.comp C (λf. Exp⇧← f x)"
using assms cnt_Exp_ide cnt_Exp_in_hom cnt_Exp_comp
by unfold_locales auto
lemma cov_cnt_Exp_commute:
assumes "arr f" and "arr g"
shows "Exp⇧→ (dom f) g ⋅ Exp⇧← f (dom g) =
Exp⇧← f (cod g) ⋅ Exp⇧→ (cod f) g"
proof -
have "Exp⇧→ (dom f) g ⋅ Exp⇧← f (dom g) =
Curry[exp (cod f) (dom g), dom f, cod g]
((g ⋅ eval (dom f) (dom g)) ⋅
(Curry[exp (cod f) (dom g), dom f, dom g]
(eval (cod f) (dom g) ⋅ (exp (cod f) (dom g) ⊗ f)) ⊗ dom f))"
using assms cnt_Exp_in_hom comp_Curry_arr by force
also have "... = Curry[exp (cod f) (dom g), dom f, cod g]
(Uncurry[cod f, cod g] (Exp⇧→ (cod f) g) ⋅
(exp (cod f) (dom g) ⊗ f))"
using assms comp_assoc Uncurry_Curry by auto
also have "... = Curry[exp (cod f) (dom g), dom f, cod g]
(eval (cod f) (cod g) ⋅ (Exp⇧→ (cod f) g ⊗ cod f) ⋅
(exp (cod f) (dom g) ⊗ f))"
using comp_assoc by auto
also have "... = Curry[exp (cod f) (dom g), dom f, cod g]
(eval (cod f) (cod g) ⋅ (Exp⇧→ (cod f) g ⊗ f))"
using assms interchange comp_arr_dom comp_cod_arr
by (metis cov_Exp_in_hom ide_cod in_homE)
also have "... = Curry[exp (cod f) (dom g), dom f, cod g]
(eval (cod f) (cod g) ⋅
(exp (cod f) (cod g) ⊗ f) ⋅ (Exp⇧→ (cod f) g ⊗ dom f))"
using assms interchange comp_arr_dom comp_cod_arr cov_Exp_in_hom
by auto
also have "... = Exp⇧← f (cod g) ⋅ Exp⇧→ (cod f) g"
using assms cov_Exp_in_hom comp_assoc
comp_Curry_arr
[of "dom f" "Exp⇧→ (cod f) g" "exp (cod f) (dom g)" _
"eval (cod f) (cod g) ⋅ (exp (cod f) (cod g) ⊗ f)" "cod g"]
by simp
finally show ?thesis by simp
qed
definition Exp
where "Exp f g ≡ Exp⇧→ (dom f) g ⋅ Exp⇧← f (dom g)"
lemma Exp_in_hom:
assumes "arr f" and "arr g"
shows "«Exp f g : Exp (cod f) (dom g) → Exp (dom f) (cod g)»"
using Exp_def assms(1-2) cnt_Exp_ide cov_Exp_ide by auto
lemma Exp_ide:
assumes "ide a" and "ide b"
shows "Exp a b = exp a b"
unfolding Exp_def
using assms cov_Exp_ide cnt_Exp_ide by simp
lemma Exp_comp:
assumes "seq g f" and "seq k h"
shows "Exp (g ⋅ f) (k ⋅ h) = Exp f k ⋅ Exp g h"
proof -
have "Exp (g ⋅ f) (k ⋅ h) = Exp⇧→ (dom f) (k ⋅ h) ⋅ Exp⇧← (g ⋅ f) (dom h)"
unfolding Exp_def
using assms by auto
also have "... = (Exp⇧→ (dom f) k ⋅ Exp⇧→ (dom f) h) ⋅
(Exp⇧← f (dom h) ⋅ Exp⇧← g (dom h))"
using assms cov_Exp_comp cnt_Exp_comp by auto
also have "... = (Exp⇧→ (dom f) k ⋅ Exp⇧← f (dom k)) ⋅
(Exp⇧→ (dom g) h ⋅ Exp⇧← g (dom h))"
using assms comp_assoc cov_cnt_Exp_commute
by (metis (no_types, lifting) seqE)
also have "... = Exp f k ⋅ Exp g h"
unfolding Exp_def by blast
finally show ?thesis by blast
qed
interpretation CopxC: product_category Cop.comp C ..
lemma functor_Exp:
shows "binary_functor Cop.comp C C (λfg. Exp (fst fg) (snd fg))"
using Exp_in_hom
apply unfold_locales
apply auto[4]
using Exp_def
apply auto[2]
using Exp_comp
by fastforce
lemma Exp_x_ide:
assumes "ide y"
shows "(λx. Exp x y) = (λx. Exp⇧← x y)"
using assms Exp_ide Exp_def comp_cod_arr cov_Exp_ide by auto
lemma Exp_ide_y:
assumes "ide x"
shows "(λy. Exp x y) = (λy. Exp⇧→ x y)"
using assms Exp_ide Exp_def comp_arr_dom cnt_Exp_ide by auto
lemma Uncurry_Exp_dom:
assumes "arr f"
shows "Uncurry (dom f) (cod f) (Exp (dom f) f) = f ⋅ eval (dom f) (dom f)"
proof -
have "Uncurry[dom f, cod f] (Exp (dom f) f) =
Uncurry[dom f, cod f]
(Curry[exp (dom f) (dom f), dom f, cod f] (f ⋅ eval (dom f) (dom f)) ⋅
Curry[exp (dom f) (dom f), dom f, dom f] (eval (dom f) (dom f)))"
unfolding Exp_def
using assms Curry_Uncurry comp_arr_dom by simp
also have "... = Uncurry[dom f, cod f]
(Curry[exp (dom f) (dom f), dom f, cod f]
((f ⋅ eval (dom f) (dom f)) ⋅
(Curry[exp (dom f) (dom f), dom f, dom f]
(eval (dom f) (dom f)) ⊗ dom f)))"
using assms comp_Curry_arr
by (metis comp_in_homI' Curry_in_hom eval_in_hom⇩E⇩C⇩M⇩C ide_dom
ide_exp in_homE)
also have "... = f ⋅ eval (dom f) (dom f)"
using assms Uncurry_Curry eval_in_hom⇩E⇩C⇩M⇩C comp_assoc by simp
finally show ?thesis by simp
qed
subsection "Exponentiation by Unity"
text‹
In this section we define and develop the properties of inverse arrows
‹Up a : a → exp ℐ a› and ‹Dn a : exp ℐ a → a›, which exist in any closed monoidal
category.
›
interpretation elementary_monoidal_category C tensor unity lunit runit assoc
using induces_elementary_monoidal_category by blast
abbreviation Up
where "Up a ≡ Curry[a, ℐ, a] 𝗋[a]"
abbreviation Dn
where "Dn a ≡ eval ℐ a ⋅ 𝗋⇧-⇧1[exp ℐ a]"
lemma isomorphic_exp_unity:
assumes "ide a"
shows "«Up a : a → exp ℐ a»"
and "«Dn a : exp ℐ a → a»"
and "inverse_arrows (Up a) (Dn a)"
and "isomorphic (exp ℐ a) a"
proof -
show 1: "«Up a : a → exp ℐ a»"
using assms ide_unity Curry_in_hom by blast
show 2: "«Dn a : exp ℐ a → a»"
using assms eval_in_hom⇩E⇩C⇩M⇩C [of ℐ a] runit_in_hom ide_unity by blast
show "inverse_arrows (Up a) (Dn a)"
proof
show "ide ((Dn a) ⋅ Up a)"
by (metis (no_types, lifting) ‹«Up a : a → exp ℐ a»›
assms comp_runit_runit'(1) ide_unity in_homE comp_assoc
runit'_naturality runit_in_hom Uncurry_Curry)
show "ide (Up a ⋅ Dn a)"
proof -
have "Up a ⋅ Dn a = (Curry[a, ℐ, a] 𝗋[a] ⋅ eval ℐ a) ⋅ 𝗋⇧-⇧1[exp ℐ a]"
using comp_assoc by simp
also have "... =
Curry[exp ℐ a ⊗ ℐ, ℐ, a] (𝗋[a] ⋅ (eval ℐ a ⊗ ℐ)) ⋅ 𝗋⇧-⇧1[exp ℐ a]"
using assms comp_Curry_arr
by (metis eval_in_hom_ax ide_unity runit_in_hom)
also have "... =
Curry[exp ℐ a ⊗ ℐ, ℐ, a] (eval ℐ a ⋅ 𝗋[exp ℐ a ⊗ ℐ]) ⋅ 𝗋⇧-⇧1[exp ℐ a]"
using assms runit_naturality
by (metis (no_types, lifting) eval_in_hom⇩E⇩C⇩M⇩C ide_unity in_homE)
also have "... = (Curry[exp ℐ a, ℐ, a] (eval ℐ a) ⋅ 𝗋[exp ℐ a]) ⋅ 𝗋⇧-⇧1[exp ℐ a]"
by (metis assms comp_Curry_arr eval_in_hom⇩E⇩C⇩M⇩C ide_exp ide_unity
runit_commutes_with_R runit_in_hom)
also have "... = Curry[exp ℐ a, ℐ, a] (eval ℐ a) ⋅ 𝗋[exp ℐ a] ⋅ 𝗋⇧-⇧1[exp ℐ a]"
using comp_assoc by simp
also have "... = Curry[exp ℐ a, ℐ, a] (eval ℐ a)"
by (metis assms 1 2 calculation comp_arr_ide comp_runit_runit'(1)
ide_exp ide_unity seqI')
also have "... = exp ℐ a"
using assms Curry_Uncurry
by (metis ide_exp ide_in_hom ide_unity Uncurry_exp)
finally show ?thesis
using assms ide_exp ide_unity by presburger
qed
qed
thus "isomorphic (exp ℐ a) a"
by (metis ‹«Up a : a → exp ℐ a»› in_homE isoI isomorphicI
isomorphic_symmetric)
qed
text‹
The maps ‹Up› and ‹Dn› are natural in a.
›
lemma Up_Dn_naturality:
assumes "arr f"
shows "Exp⇧→ ℐ f ⋅ Up (dom f) = Up (cod f) ⋅ f"
and "Dn (cod f) ⋅ Exp⇧→ ℐ f = f ⋅ Dn (dom f)"
proof -
show 1: "Exp⇧→ ℐ f ⋅ Up (dom f) = Up (cod f) ⋅ f"
proof -
have "Exp⇧→ ℐ f ⋅ Up (dom f) =
Curry[dom f, ℐ, cod f]
((f ⋅ eval ℐ (dom f)) ⋅ (Curry[dom f, ℐ, dom f] 𝗋[dom f] ⊗ ℐ))"
using assms comp_Curry_arr isomorphic_exp_unity(1) by auto
also have "... = Curry[dom f, ℐ, cod f] (𝗋[cod f] ⋅ (f ⊗ ℐ))"
using assms comp_assoc Uncurry_Curry runit_naturality by simp
also have "... = Up (cod f) ⋅ f"
by (metis assms comp_Curry_arr ide_cod ide_unity in_homI runit_in_hom)
finally show ?thesis by blast
qed
have "Exp⇧→ ℐ f ⋅ inv (Dn (dom f)) = inv (Dn (cod f)) ⋅ f"
using assms 1 isomorphic_exp_unity isomorphic_exp_unity
by (metis ide_cod ide_dom inverse_arrows_sym inverse_unique)
moreover have 2: "iso (Dn (cod f))"
using assms isomorphic_exp_unity [of "cod f"] by auto
moreover have 3: "iso (Dn (dom f))"
using assms isomorphic_exp_unity [of "dom f"] by auto
moreover have "seq (inv (Dn (cod f))) f"
using assms 2 by auto
ultimately show "Dn (cod f) ⋅ Exp⇧→ ℐ f = f ⋅ Dn (dom f)"
using assms 2 3 inv_inv iso_inv_iso comp_assoc isomorphic_exp_unity
invert_opposite_sides_of_square
[of "inv (eval ℐ (cod f) ⋅ 𝗋⇧-⇧1[exp ℐ (cod f)])" f "Exp⇧→ ℐ f"
"inv (eval ℐ (dom f) ⋅ 𝗋⇧-⇧1[exp ℐ (dom f)])"]
by metis
qed
subsection "Internal Currying"
text ‹
Currying internalizes to an isomorphism between ‹exp (x ⊗ a) b› and ‹exp x (exp a b)›.
›
abbreviation curry
where "curry x b c ≡
Curry[exp (x ⊗ b) c, x, exp b c]
(Curry[exp (x ⊗ b) c ⊗ x, b, c]
(eval (x ⊗ b) c ⋅ 𝖺[exp (x ⊗ b) c, x, b]))"
abbreviation uncurry
where "uncurry x b c ≡
Curry[exp x (exp b c), x ⊗ b, c]
(eval b c ⋅ (eval x (exp b c) ⊗ b) ⋅ 𝖺⇧-⇧1[exp x (exp b c), x, b])"
lemma internal_curry:
assumes "ide x" and "ide a" and "ide b"
shows "«curry x a b : exp (x ⊗ a) b → exp x (exp a b)»"
and "«uncurry x a b : exp x (exp a b) → exp (x ⊗ a) b»"
and "inverse_arrows (curry x a b) (uncurry x a b)"
proof -
show 1: "«curry x a b : exp (x ⊗ a) b → exp x (exp a b)»"
using assms
by (meson assoc_in_hom comp_in_homI Curry_in_hom eval_in_hom⇩E⇩C⇩M⇩C
ide_exp tensor_preserves_ide)
show 2: "«uncurry x a b : exp x (exp a b) → exp (x ⊗ a) b»"
using assms ide_exp by auto
show "inverse_arrows (curry x a b) (uncurry x a b)"
(is "inverse_arrows
(Curry (exp (x ⊗ a) b) x (exp a b)
(Curry (exp (x ⊗ a) b ⊗ x) a b ?F))
(Curry (exp x (exp a b)) (x ⊗ a) b ?G)")
proof
have F: "«?F : (exp (x ⊗ a) b ⊗ x) ⊗ a → b»"
using assms ide_exp by simp
have G: "«?G : exp x (exp a b) ⊗ x ⊗ a → b»"
using assms ide_exp by auto
show "ide (uncurry x a b ⋅ curry x a b)"
proof -
have "uncurry x a b ⋅ curry x a b =
Curry[exp (x ⊗ a) b, x ⊗ a, b] (?G ⋅ (curry x a b ⊗ x ⊗ a))"
using assms F 1 ide_exp comp_Curry_arr comp_assoc by auto
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval a b ⋅ (eval x (exp a b) ⊗ a) ⋅ 𝖺⇧-⇧1[exp x (exp a b), x, a] ⋅
(curry x a b ⊗ x ⊗ a))"
using comp_assoc by simp
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval a b ⋅ (eval x (exp a b) ⊗ a) ⋅
((curry x a b ⊗ x) ⊗ a) ⋅ 𝖺⇧-⇧1[exp (x ⊗ a) b, x, a])"
using assms 1 comp_assoc assoc'_naturality [of "curry x a b" x a]
ide_char in_homE
by metis
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval a b ⋅ ((eval x (exp a b) ⊗ a) ⋅ ((curry x a b ⊗ x) ⊗ a)) ⋅
𝖺⇧-⇧1[exp (x ⊗ a) b, x, a])"
using comp_assoc by simp
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval a b ⋅ (Uncurry[x, exp a b] (curry x a b) ⊗ a) ⋅
𝖺⇧-⇧1[exp (x ⊗ a) b, x, a])"
using assms comp_ide_self
interchange [of "eval x (exp a b)"
"Curry[exp (x ⊗ a) b, x, exp a b]
(Curry[exp (x ⊗ a) b ⊗ x, a, b] ?F) ⊗ x"
a a]
by fastforce
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval a b ⋅
(Curry[exp (x ⊗ a) b ⊗ x, a, b] ?F ⊗ a) ⋅
𝖺⇧-⇧1[exp (x ⊗ a) b, x, a])"
using assms F ide_exp comp_assoc comp_ide_self
Uncurry_Curry
[of "exp (x ⊗ a) b" x "exp a b" "Curry[exp (x ⊗ a) b ⊗ x, a, b] ?F"]
by fastforce
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b]
(eval (x ⊗ a) b ⋅ 𝖺[exp (x ⊗ a) b, x, a] ⋅
𝖺⇧-⇧1[exp (x ⊗ a) b, x, a])"
using assms Uncurry_Curry
by (metis F ide_exp comp_assoc tensor_preserves_ide)
also have "... = Curry[exp (x ⊗ a) b, x ⊗ a, b] (eval (x ⊗ a) b)"
using assms Uncurry_exp by simp
also have "... = exp (x ⊗ a) b"
using assms Curry_Uncurry
by (metis Curry_Uncurry ide_exp ide_in_hom tensor_preserves_ide
Uncurry_exp)
finally have "uncurry x a b ⋅ curry x a b = exp (x ⊗ a) b"
by blast
thus ?thesis
using assms by simp
qed
show "ide (curry x a b ⋅ uncurry x a b)"
proof -
have "curry x a b ⋅ uncurry x a b =
Curry[exp x (exp a b), x, exp a b]
(Curry[exp (x ⊗ a) b ⊗ x, a, b] ?F ⋅ (uncurry x a b ⊗ x))"
using assms 2 F Curry_in_hom comp_Curry_arr by simp
also have "... = Curry[exp x (exp a b), x, exp a b]
(Curry[exp x (exp a b) ⊗ x, a, b]
(eval (x ⊗ a) b ⋅ 𝖺[exp (x ⊗ a) b, x, a] ⋅
((uncurry x a b ⊗ x) ⊗ a)))"
proof -
have "Curry[exp (x ⊗ a) b ⊗ x, a, b] ?F ⋅ (uncurry x a b ⊗ x) =
Curry[exp x (exp a b) ⊗ x, a, b] (?F ⋅ ((uncurry x a b ⊗ x) ⊗ a))"
using assms(1-2) 2 F comp_Curry_arr ide_in_hom by auto
thus ?thesis
using comp_assoc by simp
qed
also have "... = Curry[exp x (exp a b), x, exp a b]
(Curry[exp x (exp a b) ⊗ x, a, b]
(eval (x ⊗ a) b ⋅
(uncurry x a b ⊗ x ⊗ a) ⋅ 𝖺[exp x (exp a b), x, a]))"
using assms 2
assoc_naturality [of "Curry (exp x (exp a b)) (x ⊗ a) b ?G" x a]
by auto
also have "... = Curry[exp x (exp a b), x, exp a b]
(Curry[exp x (exp a b) ⊗ x, a, b]
(eval a b ⋅ (eval x (exp a b) ⊗ a) ⋅
𝖺⇧-⇧1[exp x (exp a b), x, a] ⋅ 𝖺[exp x (exp a b), x, a]))"
using assms Uncurry_Curry
by (metis G ide_exp comp_assoc tensor_preserves_ide)
also have "... = Curry[exp x (exp a b), x, exp a b]
(Curry[exp x (exp a b) ⊗ x, a, b]
(Uncurry[a, b] (eval x (exp a b))))"
using assms
by (metis G arrI cod_assoc' comp_arr_dom comp_assoc_assoc'(2)
ide_exp seqE)
also have "... = Curry[exp x (exp a b), x, exp a b] (eval x (exp a b))"
by (simp add: assms(1-3) Curry_Uncurry eval_in_hom⇩E⇩C⇩M⇩C)
also have "... = exp x (exp a b)"
using assms Curry_Uncurry Uncurry_exp
by (metis ide_exp ide_in_hom)
finally have "curry x a b ⋅ uncurry x a b = exp x (exp a b)"
by blast
thus ?thesis
using assms by fastforce
qed
qed
qed
text ‹
Internal currying and uncurrying are the components of natural isomorphisms between
the contravariant functors ‹Exp⇧← (‐ ⊗ b) c› and ‹Exp⇧← ‐ (exp b c)›.
›
lemma uncurry_naturality:
assumes "ide b" and "ide c" and "Cop.arr f"
shows "uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c) =
Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅ (uncurry (Cop.dom f) b c ⊗ f ⊗ b))"
and "Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c =
Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅ (uncurry (Cop.dom f) b c ⊗ f ⊗ b))"
and "uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c) =
Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c"
proof -
interpret xb: "functor" Cop.comp Cop.comp ‹λx. x ⊗ b›
using assms(1) T.fixing_ide_gives_functor_2 [of b]
by (simp add: category_axioms dual_category.intro dual_functor.intro
dual_functor.is_functor)
interpret F: "functor" Cop.comp C ‹λx. Exp⇧← x (exp b c)›
using assms functor_cnt_Exp by blast
have *: "⋀x. Cop.ide x ⟹
Uncurry (x ⊗ b) c (uncurry x b c) =
eval b c ⋅ (eval x (exp b c) ⊗ b) ⋅ 𝖺⇧-⇧1[exp x (exp b c), x, b]"
using assms Uncurry_Curry Cop.ide_char by auto
show 1: "uncurry (Cop.cod f) b c ⋅ cnt_Exp f (exp b c) =
Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅ (uncurry (Cop.dom f) b c ⊗ f ⊗ b))"
proof -
have "uncurry (Cop.cod f) b c ⋅ cnt_Exp f (exp b c) =
Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
((eval b c ⋅
(eval (Cop.cod f) (exp b c) ⊗ b) ⋅
𝖺⇧-⇧1[exp (Cop.cod f) (exp b c), (Cop.cod f), b]) ⋅
(cnt_Exp f (exp b c) ⊗ Cop.cod f ⊗ b))"
using assms ide_exp cnt_Exp_in_hom comp_Curry_arr by auto
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
((eval b c ⋅
(eval (Cop.cod f) (exp b c) ⊗ b) ⋅
((cnt_Exp f (exp b c) ⊗ Cop.cod f) ⊗ b)) ⋅
𝖺⇧-⇧1[exp (Cop.dom f) (exp b c), Cop.cod f, b])"
using assms comp_assoc
assoc'_naturality [of "cnt_Exp f (exp b c)" "Cop.cod f" b]
by auto
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(Uncurry[b, c]
(Uncurry[Cop.cod f, exp b c]
(Curry[exp (Cop.dom f) (exp b c), Cop.cod f, exp b c]
(eval (Cop.dom f) (exp b c) ⋅
(exp (Cop.dom f) (exp b c) ⊗ f)))) ⋅
𝖺⇧-⇧1[exp (Cop.dom f) (exp b c), Cop.cod f, b])"
using assms interchange by simp
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval b c ⋅
((eval (Cop.dom f) (exp b c) ⋅
(exp (Cop.dom f) (exp b c) ⊗ f)) ⊗ b) ⋅
𝖺⇧-⇧1[exp (Cop.dom f) (exp b c), Cop.cod f, b])"
using assms Uncurry_Curry comp_assoc by force
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval b c ⋅
((eval (Cop.dom f) (exp b c) ⊗ b) ⋅
((exp (Cop.dom f) (exp b c) ⊗ f) ⊗ b)) ⋅
𝖺⇧-⇧1[exp (Cop.dom f) (exp b c), Cop.cod f, b])"
using assms interchange by simp
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
((eval b c ⋅ (eval (Cop.dom f) (exp b c) ⊗ b) ⋅
𝖺⇧-⇧1[exp (Cop.dom f) (exp b c), cod f, b]) ⋅
(exp (Cop.dom f) (exp b c) ⊗ f ⊗ b))"
using assms assoc'_naturality [of "exp (Cop.dom f) (exp b c)" f b] comp_assoc
by simp
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(Uncurry[Cop.dom f ⊗ b, c]
(uncurry (Cop.dom f) b c) ⋅
(exp (Cop.dom f) (exp b c) ⊗ f ⊗ b))"
using assms * by simp
also have "... =
Curry (exp (Cop.dom f) (exp b c)) (Cop.cod f ⊗ b) c
(eval (Cop.dom f ⊗ b) c ⋅
(uncurry (Cop.dom f) b c ⊗ (Cop.dom f ⊗ b) ⋅ (f ⊗ b)))"
using assms ide_exp internal_curry(2) interchange comp_assoc
comp_arr_dom [of "uncurry (Cop.dom f) b c"]
by auto
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅
(uncurry (Cop.dom f) b c ⊗ f ⊗ b))"
using assms(1,3) comp_cod_arr interchange by fastforce
finally show ?thesis by blast
qed
show 2: "Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c = ..."
proof -
have "Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c =
Curry[exp (Cop.dom f ⊗ b) c, Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅ (exp (Cop.dom f ⊗ b) c ⊗ f ⊗ b)) ⋅
uncurry (Cop.dom f) b c"
using assms comp_arr_dom by simp
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
((eval (Cop.dom f ⊗ b) c ⋅
(exp (Cop.dom f ⊗ b) c ⊗ f ⊗ b)) ⋅
(uncurry (Cop.dom f) b c ⊗ Cop.cod f ⊗ b))"
using assms Curry_in_hom comp_Curry_arr by force
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅
(exp (Cop.dom f ⊗ b) c ⋅ uncurry (Cop.dom f) b c
⊗ (f ⊗ b) ⋅ (Cop.cod f ⊗ b)))"
proof -
have "seq (exp (Cop.dom f ⊗ b) c) (uncurry (Cop.dom f) b c)"
using assms by fastforce
thus ?thesis
using assms internal_curry comp_assoc interchange by simp
qed
also have "... = Curry[exp (Cop.dom f) (exp b c), Cop.cod f ⊗ b, c]
(eval (Cop.dom f ⊗ b) c ⋅
(uncurry (Cop.dom f) b c ⊗ f ⊗ b))"
proof -
have "(f ⊗ b) ⋅ (Cop.cod f ⊗ b) = f ⊗ b"
using assms interchange comp_arr_dom comp_cod_arr by simp
thus ?thesis
using assms internal_curry comp_cod_arr [of "uncurry (Cop.dom f) b c"]
by simp
qed
finally show ?thesis by simp
qed
show "uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c) =
Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c"
using 1 2 by simp
qed
lemma natural_isomorphism_uncurry:
assumes "ide b" and "ide c"
shows "natural_isomorphism Cop.comp C
(λx. Exp⇧← x (exp b c)) (λx. Exp⇧← (x ⊗ b) c)
(λf. uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c))"
proof -
interpret xb: "functor" Cop.comp Cop.comp ‹λx. x ⊗ b›
using assms(1) T.fixing_ide_gives_functor_2
by (simp add: category_axioms dual_category.intro dual_functor.intro
dual_functor.is_functor)
interpret Exp_c: "functor" Cop.comp C ‹λx. Exp⇧← x c›
using assms functor_cnt_Exp by blast
interpret F: "functor" Cop.comp C ‹λx. Exp⇧← x (exp b c)›
using assms functor_cnt_Exp by blast
interpret G: "functor" Cop.comp C ‹λx. Exp⇧← (x ⊗ b) c›
proof -
interpret G: composite_functor Cop.comp Cop.comp C
‹λx. x ⊗ b› ‹λy. Exp⇧← y c›
..
have "G.map = (λx. Exp⇧← (x ⊗ b) c)"
by auto
thus "functor Cop.comp C (λx. Exp⇧← (x ⊗ b) c)"
using G.functor_axioms by metis
qed
interpret φ: transformation_by_components Cop.comp C
‹λx. Exp⇧← x (exp b c)› ‹λx. Exp⇧← (x ⊗ b) c›
‹λx. uncurry x b c›
proof
show "⋀a. Cop.ide a ⟹
«uncurry a b c : Exp⇧← a (exp b c) → Exp⇧← (a ⊗ b) c»"
using assms internal_curry(2) Cop.ide_char cnt_Exp_ide by auto
show "⋀f. Cop.arr f ⟹
uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c) =
Exp⇧← (f ⊗ b) c ⋅ uncurry (Cop.dom f) b c"
using assms uncurry_naturality by simp
qed
have "natural_isomorphism Cop.comp C
(λx. Exp⇧← x (exp b c)) (λx. Exp⇧← (x ⊗ b) c) φ.map"
proof
fix a
assume a: "Cop.ide a"
show "iso (φ.map a)"
using a assms internal_curry [of a b c] φ.map_simp_ide
inverse_arrows_sym
by auto
qed
moreover have "φ.map = (λf. uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c))"
using assms φ.map_def by auto
ultimately show ?thesis
unfolding φ.map_def by simp
qed
lemma natural_isomorphism_curry:
assumes "ide b" and "ide c"
shows "natural_isomorphism Cop.comp C
(λx. Exp⇧← (x ⊗ b) c) (λx. Exp⇧← x (exp b c))
(λf. curry (Cop.cod f) b c ⋅ Exp⇧← (f ⊗ b) c)"
proof -
interpret φ: natural_isomorphism Cop.comp C
‹λx. Exp⇧← x (exp b c)› ‹λx. Exp⇧← (x ⊗ b) c›
‹λf. uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c)›
using assms natural_isomorphism_uncurry by blast
interpret ψ: inverse_transformation Cop.comp C
‹λx. Exp⇧← x (exp b c)› ‹λx. Exp⇧← (x ⊗ b) c›
‹λf. uncurry (Cop.cod f) b c ⋅ Exp⇧← f (exp b c)›
..
have 1: "⋀a. Cop.ide a ⟹ ψ.map a = curry a b c"
proof -
fix a
assume a: "Cop.ide a"
have "inverse_arrows
(uncurry (Cop.cod a) b c ⋅ Exp⇧← a (exp b c)) (ψ.map a)"
using assms a ψ.inverts_components by blast
moreover
have "inverse_arrows
(uncurry (Cop.cod a) b c ⋅ Exp⇧← a (exp b c)) (curry a b c)"
by (metis assms a Cop.ideD(1,3) Cop.ide_char φ.F.preserves_ide
φ.preserves_reflects_arr comp_arr_ide internal_curry(3)
inverse_arrows_sym)
ultimately show "ψ.map a = curry a b c"
using internal_curry inverse_arrow_unique by simp
qed
have "ψ.map = (λf. curry (Cop.cod f) b c ⋅ Exp⇧← (f ⊗ b) c)"
proof
fix f
show "ψ.map f = curry (Cop.cod f) b c ⋅ Exp⇧← (f ⊗ b) c"
using assms 1 ψ.inverts_components internal_curry(3) ψ.is_natural_2
Cop.ide_char ψ.is_extensional
by auto
qed
thus ?thesis
using ψ.natural_isomorphism_axioms by simp
qed
subsection "Yoneda Embedding"
text ‹
The internal hom provides a closed monoidal category ‹C› with a "Yoneda embedding",
which is a mapping that takes each arrow ‹g› of ‹C› to a natural transformation from
the contravariant functor ‹Exp⇧← ‐ (dom g)› to the contravariant functor
‹Exp⇧← ‐ (cod g)›. Note that here the target category is ‹C› itself, not a category
of sets and functions as in the classical case. Note also that we are talking here
about ordinary functors and natural transformations.
We can easily prove from general considerations that the Yoneda embedding (so-defined)
is faithful. However, to obtain a fullness result requires the development of a
certain amount of enriched category theory, which we do elsewhere.
›
lemma yoneda_embedding:
assumes "«g : a → b»"
shows "natural_transformation Cop.comp C
(λx. Exp⇧← x a) (λx. Exp⇧← x b) (λx. Exp x g)"
and "Uncurry[a, b] (Exp a g ⋅ Curry[ℐ, a, a] 𝗅[a]) ⋅ 𝗅⇧-⇧1[a] = g"
proof -
interpret Exp: binary_functor Cop.comp C C ‹λfg. Exp (fst fg) (snd fg)›
using functor_Exp by blast
interpret Exp_g: natural_transformation Cop.comp C
‹λx. Exp x (dom g)› ‹λx. Exp x (cod g)› ‹λx. Exp x g›
using assms Exp.fixing_arr_gives_natural_transformation_2 [of g] by auto
show "natural_transformation Cop.comp C (λx. Exp⇧← x a) (λx. Exp⇧← x b)
(λx. Exp x g)"
using assms Exp_x_ide Exp_x_ide Exp_g.natural_transformation_axioms
by auto
show "Uncurry[a, b] (Exp a g ⋅ Curry[ℐ, a, a] 𝗅[a]) ⋅ 𝗅⇧-⇧1[a] = g"
proof -
have "Uncurry[a, b] (Exp a g ⋅ Curry[ℐ, a, a] 𝗅[a]) ⋅ 𝗅⇧-⇧1[a] =
(eval a b ⋅ (Exp a g ⊗ a) ⋅ (Curry[ℐ, a, a] 𝗅[a] ⊗ a)) ⋅ 𝗅⇧-⇧1[a]"
using assms Exp_ide lunit_in_hom
interchange [of "Exp a g" "Curry[ℐ, a, a] 𝗅[a]" a a]
by auto
also have "... = g ⋅ (eval a a ⋅ (Curry[ℐ, a, a] 𝗅[a] ⊗ a)) ⋅ 𝗅⇧-⇧1[a]"
using assms Uncurry_Exp_dom comp_assoc by (metis in_homE)
also have "... = g ⋅ 𝗅[a] ⋅ 𝗅⇧-⇧1[a]"
using assms Uncurry_Curry ide_dom ide_unity lunit_in_hom by auto
also have "... = g"
using assms comp_arr_dom by force
finally show ?thesis
by blast
qed
qed
lemma yoneda_embedding_is_faithful:
assumes "par g g'" and "(λx. Exp x g) = (λx. Exp x g')"
shows "g = g'"
proof -
have "g ⋅ eval (dom g) (dom g) = g' ⋅ eval (dom g) (dom g)"
using assms Uncurry_Exp_dom by metis
thus "g = g'"
using assms retraction_eval_ide_self retraction_is_epi
by (metis epiE eval_simps(1,3) ide_dom seqI)
qed
text ‹
The following is a version of the key fact underlying the classical Yoneda Lemma:
for any natural transformation ‹τ› from ‹Exp⇧← ‐ a› to ‹Exp⇧← ‐ b›,
there is a fixed arrow ‹g : a → b›, depending only on the single component ‹τ a›,
such that the compositions ‹τ x ⋅ e› of an arbitrary component ‹τ x› with arbitrary
global elements ‹e : ℐ → exp x a› depend on ‹τ› only via ‹g›, and hence only via ‹τ a›.
›
lemma hom_transformation_expansion:
assumes "natural_transformation
Cop.comp C (λx. Exp⇧← x a) (λx. Exp⇧← x b) τ"
and "ide a" and "ide b"
shows "«Uncurry[a, b] (τ a ⋅ Curry[ℐ, a, a] 𝗅[a]) ⋅ 𝗅⇧-⇧1[a] : a → b»"
and "⋀x e. ⟦ide x; «e : ℐ → exp x a»⟧ ⟹
τ x ⋅ e = Exp x (Uncurry[a, b] (τ a ⋅ Curry[ℐ, a, a] 𝗅[a]) ⋅ 𝗅⇧-⇧1[a]) ⋅ e"
proof -
interpret τ: natural_transformation Cop.comp C
‹λx. Exp⇧← x a› ‹λx. Exp⇧← x b› τ
using assms by blast
let ?Id_a = "Curry[ℐ, a, a] 𝗅[a]"
have Id_a: "«?Id_a : ℐ → exp a a»"
using assms ide_unity by blast
let ?g = "Uncurry[a, b] (τ a ⋅ ?Id_a) ⋅ 𝗅⇧-⇧1[a]"
show g: "«?g : a → b»"
using assms(2-3) Id_a cnt_Exp_ide by auto
have *: "⋀x e. ⟦ide x; «e : ℐ → exp x a»⟧
⟹ τ x ⋅ e = Curry[exp x a, x, b] (?g ⋅ eval x a) ⋅ e"
proof -
fix x e
assume x: "ide x"
assume e: "«e : ℐ → exp x a»"
let ?e' = "Uncurry x a e ⋅ 𝗅⇧-⇧1[x]"
have e': "«?e' : x → a»"
using assms(2) x e by blast
have 1: "e = Exp⇧← ?e' a ⋅ ?Id_a"
proof -
have "Exp⇧← ?e' a ⋅ ?Id_a =
Curry[exp a a, x, a] (eval a a ⋅ (exp a a ⊗ ?e')) ⋅ ?Id_a"
using assms(2) e' by auto
also have "... =
Curry[ℐ, x, a] (eval a a ⋅ (exp a a ⊗ ?e') ⋅ (?Id_a ⊗ x))"
using assms(2) Id_a e' x comp_Curry_arr comp_assoc by auto
also have "... = Curry[ℐ, x, a] (eval a a ⋅ (?Id_a ⊗ ?e'))"
using assms(2) e' Id_a interchange comp_arr_dom comp_cod_arr in_homE
by (metis (no_types, lifting))
also have "... = Curry ℐ x a (eval a a ⋅ (?Id_a ⊗ a) ⋅ (ℐ ⊗ ?e'))"
using assms(2) interchange
by (metis (no_types, lifting) e' Id_a comp_arr_ide comp_cod_arr ide_char
ide_unity in_homE seqI)
also have "... =
Curry[ℐ, x, a] (Uncurry a a (Curry[ℐ, a, a] 𝗅[a]) ⋅ (ℐ ⊗ ?e'))"
using comp_assoc by simp
also have "... = Curry[ℐ, x, a] (𝗅[a] ⋅ (ℐ ⊗ ?e'))"
using assms(2) Uncurry_Curry comp_assoc ide_unity lunit_in_hom
by presburger
also have "... = Curry[ℐ, x, a] (?e' ⋅ 𝗅[x])"
using assms(2) e' in_homE lunit_naturality
by (metis (no_types, lifting))
also have "... = Curry[ℐ, x, a] (Uncurry[x, a] e ⋅ 𝗅⇧-⇧1[x] ⋅ 𝗅[x])"
using comp_assoc by simp
also have "... = Curry[ℐ, x, a] (Uncurry[x, a] e)"
using assms(2) x e comp_arr_dom Uncurry_simps(2) by force
also have "... = e"
using assms(2) x e Curry_Uncurry ide_unity by blast
finally show ?thesis by simp
qed
have "τ x ⋅ e = τ x ⋅ Exp⇧← ?e' a ⋅ ?Id_a"
using 1 by simp
also have "... = (τ x ⋅ Exp⇧← ?e' a) ⋅ ?Id_a"
using comp_assoc by simp
also have "... = (Exp⇧← ?e' b ⋅ τ a) ⋅ ?Id_a"
using e' τ.naturality [of ?e'] by auto
also have "... = Curry[exp a b, x, b] (eval a b ⋅ (exp a b ⊗ ?e')) ⋅ τ a ⋅ ?Id_a"
using assms(2) e' comp_assoc by auto
also have "... =
Curry[ℐ, x, b] ((eval a b ⋅ (exp a b ⊗ ?e')) ⋅ (τ a ⋅ ?Id_a ⊗ x))"
proof -
have "«τ a ⋅ ?Id_a : ℐ → exp a b»"
using Id_a assms(2-3) in_homI cnt_Exp_ide
by (intro comp_in_homI) auto
moreover have "«eval a b ⋅ (exp a b ⊗ ?e') : exp a b ⊗ x → b»"
using assms(2-3) e' ide_in_hom by blast
ultimately show ?thesis
using x comp_Curry_arr by blast
qed
also have "... = Curry[ℐ, x, b] (eval a b ⋅ (exp a b ⊗ ?e') ⋅ (τ a ⋅ ?Id_a ⊗ x))"
using comp_assoc by simp
also have "... = Curry[ℐ, x, b] (eval a b ⋅ (exp a b ⋅ τ a ⋅ ?Id_a ⊗ ?e' ⋅ x))"
proof -
have "seq (exp a b) (τ a ⋅ Curry[ℐ, a, a] 𝗅[a])"
using assms ide_exp τ.natural_transformation_axioms Id_a Curry_Uncurry
ide_exp ide_in_hom
by auto
moreover have "seq (Uncurry[x, a] e ⋅ 𝗅⇧-⇧1[x]) x"
using x e' by auto
ultimately show ?thesis
using assms interchange by simp
qed
also have "... = Curry[ℐ, x, b] (eval a b ⋅ (τ a ⋅ ?Id_a ⊗ ?e'))"
proof -
have "exp a b ⋅ τ a ⋅ ?Id_a = τ a ⋅ ?Id_a"
using assms(2-3) e' ide_exp comp_ide_arr τ.preserves_hom cnt_Exp_ide
Id_a
by auto
moreover have "?e' ⋅ x = ?e'"
using e' comp_arr_dom by blast
ultimately show ?thesis
using interchange by simp
qed
also have "... = Curry[ℐ, x, b] (eval a b ⋅ (τ a ⋅ ?Id_a ⊗ a) ⋅ (ℐ ⊗ ?e'))"
proof -
have "(τ a ⋅ ?Id_a) ⋅ ℐ = τ a ⋅ ?Id_a"
using assms(2) comp_arr_ide
by (metis Id_a comp_arr_dom in_homE comp_assoc)
moreover have "a ⋅ ?e' = ?e'"
using e' comp_cod_arr by blast
moreover have "seq (τ a ⋅ Curry[ℐ, a, a] 𝗅[a]) ℐ"
using assms(2) cnt_Exp_ide Id_a by auto
moreover have "seq a (Uncurry[x, a] e ⋅ 𝗅⇧-⇧1[x])"
using calculation(2) e' by auto
ultimately show ?thesis
using interchange [of "τ a ⋅ ?Id_a" ℐ a ?e'] by simp
qed
also have "... = Curry[ℐ, x, b] (eval a b ⋅ (τ a ⋅ ?Id_a ⊗ a) ⋅ (𝗅⇧-⇧1[a] ⋅ 𝗅[a]) ⋅
(ℐ ⊗ eval x a ⋅ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x]))"
proof -
have "(ℐ ⊗ eval x a) ⋅ (ℐ ⊗ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x]) =
(ℐ ⊗ a) ⋅ (ℐ ⊗ eval x a) ⋅ (ℐ ⊗ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x])"
using assms e' L.as_nat_trans.is_natural_2 comp_lunit_lunit'(2) comp_assoc
by (metis (no_types, lifting) L.as_nat_trans.preserves_comp_2 in_homE)
thus ?thesis
using assms e' comp_assoc
by (elim in_homE) auto
qed
also have "... = Curry[ℐ, x, b] (?g ⋅ 𝗅[a] ⋅ (ℐ ⊗ eval x a ⋅ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x]))"
using comp_assoc by simp
also have "... = Curry[ℐ, x, b] (?g ⋅ (eval x a ⋅ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x]) ⋅ 𝗅[x])"
using lunit_naturality
by (metis (no_types, lifting) e' in_homE comp_assoc)
also have "... = Curry[ℐ, x, b] (?g ⋅ eval x a ⋅ (e ⊗ x) ⋅ 𝗅⇧-⇧1[x] ⋅ 𝗅[x])"
using comp_assoc by simp
also have "... = Curry[ℐ, x, b] (?g ⋅ eval x a ⋅ (e ⊗ x))"
using x comp_arr_dom e interchange by fastforce
also have "... = Curry[ℐ, x, b] ((?g ⋅ eval x a) ⋅ (e ⊗ x))"
using comp_assoc by simp
also have "... = Curry[exp x a, x, b] (?g ⋅ eval x a) ⋅ e"
using assms(2) x e g comp_Curry_arr by auto
finally show "τ x ⋅ e = Curry[exp x a, x, b] (?g ⋅ eval x a) ⋅ e"
by blast
qed
show "⋀x e. ⟦ide x; «e : ℐ → exp x a»⟧ ⟹ τ x ⋅ e = Exp x ?g ⋅ e"
proof -
fix x e
assume x: "ide x"
assume e: "«e : ℐ → exp x a»"
have "τ x ⋅ e = Curry[exp x a, x, b] (?g ⋅ eval x a) ⋅ e"
using x e * τ.natural_transformation_axioms by blast
also have "... = (Curry[exp x a, x, cod ?g] (?g ⋅ eval x a) ⋅
Curry[exp x a, x, a] (Uncurry[x, a] (exp x a))) ⋅ e"
proof -
have "Curry[exp x a, x, a] (Uncurry[x, a] (exp x a)) = exp x a"
using assms(2) x Curry_Uncurry ide_exp ide_in_hom by force
thus ?thesis
using g e comp_cod_arr comp_assoc by fastforce
qed
also have "... = Exp x ?g ⋅ e"
using x Exp_def cod_comp g by auto
finally show "τ x ⋅ e = Exp x ?g ⋅ e" by blast
qed
qed
section "Enriched Structure"
text ‹
In this section we do the main work involved in showing that a closed monoidal category
is ``enriched in itself''. For this, we need to define, for each object ‹a›, an arrow
‹Id a : ℐ → exp a a› to serve as the ``identity at ‹a›'', and for every three objects
‹a›, ‹b›, and ‹c›, a ``compositor'' ‹Comp a b c : exp b c ⊗ exp a b → exp a c›.
We also need to prove that these satisfy the appropriate unit and associativity laws.
Although essentially all the work is done here, the statement and proof of the the final
result is deferred to a separate theory ‹EnrichedCategory› so that a mutual dependence
between that theory and the present one is not introduced.
›
interpretation elementary_monoidal_category C tensor unity lunit runit assoc
using induces_elementary_monoidal_category by blast
definition Id
where "Id a ≡ Curry[ℐ, a, a] 𝗅[a]"
lemma Id_in_hom [intro]:
assumes "ide a"
shows "«Id a : ℐ → exp a a»"
unfolding Id_def
using assms Curry_in_hom lunit_in_hom by simp
lemma Id_simps [simp]:
assumes "ide a"
shows "arr (Id a)"
and "dom (Id a) = ℐ"
and "cod (Id a) = exp a a"
using assms Id_in_hom by blast+
text‹
The next definition follows Kelly \<^cite>‹"kelly-enriched-category"›, section 1.6.
›
definition Comp
where "Comp a b c ≡
Curry[exp b c ⊗ exp a b, a, c]
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a])"
lemma Comp_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«Comp a b c : exp b c ⊗ exp a b → exp a c»"
using assms ide_exp ide_in_hom Comp_def Curry_in_hom tensor_preserves_ide
by auto
lemma Comp_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr (Comp a b c)"
and "dom (Comp a b c) = exp b c ⊗ exp a b"
and "cod (Comp a b c) = exp a c"
using assms Comp_in_hom in_homE by blast+
lemma Comp_unit_right:
assumes "ide a" and "ide b" and "ide c"
shows "«Comp a a b ⋅ (exp a b ⊗ Id a) : exp a b ⊗ ℐ → exp a b»"
and "Comp a a b ⋅ (exp a b ⊗ Id a) = 𝗋[exp a b]"
proof -
show 0: "«Comp a a b ⋅ (exp a b ⊗ Id a) : exp a b ⊗ ℐ → exp a b»"
using assms Id_in_hom tensor_in_hom ide_in_hom ide_exp by force
show "Comp a a b ⋅ (exp a b ⊗ Id a) = 𝗋[exp a b]"
proof (intro runit_eqI)
show 1: "«Comp a a b ⋅ (exp a b ⊗ Id a) : exp a b ⊗ ℐ → exp a b»"
by fact
show "Comp a a b ⋅ (exp a b ⊗ Id a) ⊗ ℐ = (exp a b ⊗ ι) ⋅ 𝖺[exp a b, ℐ, ℐ]"
proof -
have "𝗋[exp a b] ⋅ (Comp a a b ⋅ (exp a b ⊗ Id a) ⊗ ℐ) ⋅
inv 𝖺[exp a b, ℐ, ℐ] =
𝗋[exp a b] ⋅ ((Comp a a b ⊗ ℐ) ⋅ ((exp a b ⊗ Id a) ⊗ ℐ)) ⋅
inv 𝖺[exp a b, ℐ, ℐ]"
using ‹«Comp a a b ⋅ (exp a b ⊗ Id a) : exp a b ⊗ ℐ → exp a b»› arrI
by force
also have "... = (𝗋[exp a b] ⋅ (Comp a a b ⊗ ℐ)) ⋅
((exp a b ⊗ Id a) ⊗ ℐ) ⋅ inv 𝖺[exp a b, ℐ, ℐ]"
using comp_assoc by simp
also have "... = (Comp a a b ⋅ 𝗋[exp a b ⊗ exp a a]) ⋅
((exp a b ⊗ Id a) ⊗ ℐ) ⋅ inv 𝖺[exp a b, ℐ, ℐ]"
using assms runit_naturality
by (metis Comp_simps(1-2) 1 cod_comp in_homE)
also have "... = Comp a a b ⋅
(𝗋[exp a b ⊗ exp a a] ⋅ ((exp a b ⊗ Id a) ⊗ ℐ)) ⋅
inv 𝖺[exp a b, ℐ, ℐ]"
using comp_assoc by simp
also have "... = Comp a a b ⋅ ((exp a b ⊗ Id a) ⋅ 𝗋[exp a b ⊗ ℐ]) ⋅
inv 𝖺[exp a b, ℐ, ℐ]"
using assms 1 runit_naturality
by (metis calculation in_homE comp_assoc)
also have "... = Comp a a b ⋅ (exp a b ⊗ Id a) ⋅ 𝗋[exp a b ⊗ ℐ] ⋅
inv 𝖺[exp a b, ℐ, ℐ]"
using comp_assoc by simp
also have "... = Comp a a b ⋅ (exp a b ⊗ Id a) ⋅ (exp a b ⊗ ι)"
using assms ide_unity runit_tensor' ide_exp runit_eqI unit_in_hom_ax
unit_triangle(1)
by presburger
also have "... = (Curry[exp a b ⊗ exp a a, a, b]
(eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
(exp a b ⊗ Id a)) ⋅ (exp a b ⊗ ι)"
using Comp_def comp_assoc by simp
also have "... = Curry[exp a b ⊗ ℐ, a, b]
((eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a)) ⋅
(exp a b ⊗ ι)"
proof -
have "«exp a b ⊗ Id a : exp a b ⊗ ℐ → exp a b ⊗ exp a a»"
using assms by auto
moreover have "«eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a] :
(exp a b ⊗ exp a a) ⊗ a → b»"
using assms tensor_in_hom ide_in_hom ide_exp eval_in_hom⇩E⇩C⇩M⇩C
by force
ultimately show ?thesis
using assms comp_Curry_arr by simp
qed
also have "... = 𝗋[exp a b] ⋅ (exp a b ⊗ ι)"
proof -
have 1: "Uncurry[a, b]
(Curry[exp a b ⊗ ℐ, a, b]
((eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a))) =
(eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a)"
proof -
have "«(eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a) : (exp a b ⊗ ℐ) ⊗ a → b»"
using assms tensor_in_hom ide_in_hom eval_in_hom⇩E⇩C⇩M⇩C ide_exp
by force
thus ?thesis
using assms Uncurry_Curry by auto
qed
also have "... = (eval a b ⋅ (exp a b ⊗ eval a a) ⋅ (exp a b ⊗ Id a ⊗ a)) ⋅
𝖺[exp a b, ℐ, a]"
using assms ide_exp comp_assoc assoc_naturality [of "exp a b" "Id a" a]
by auto
also have "... = (eval a b ⋅ (exp a b ⊗ Uncurry[a, a] (Id a))) ⋅
𝖺[exp a b, ℐ, a]"
using assms interchange
by (metis (no_types, lifting) ide_exp lunit_in_hom Uncurry_Curry
ide_unity comp_ide_self ideD(1) in_homE Id_def)
also have "... = (eval a b ⋅ (exp a b ⊗ 𝗅[a])) ⋅ 𝖺[exp a b, ℐ, a]"
by (metis (no_types, lifting) assms(1) lunit_in_hom Uncurry_Curry
ide_unity Id_def)
also have 2: "... = (eval a b ⋅ (exp a b ⊗ a) ⋅ (exp a b ⊗ 𝗅[a])) ⋅
𝖺[exp a b, ℐ, a]"
using assms interchange 𝔩_ide_simp by auto
also have "... = Uncurry[a, b] (exp a b) ⋅ (exp a b ⊗ 𝗅[a]) ⋅ 𝖺[exp a b, ℐ, a]"
using comp_assoc by simp
also have "... = Uncurry a b 𝗋[exp a b]"
using assms triangle ide_exp 2 comp_assoc by auto
finally have "Uncurry[a, b]
(Curry[exp a b ⊗ ℐ, a, b]
((eval a b ⋅ (exp a b ⊗ eval a a) ⋅
𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a))) =
Uncurry[a, b] 𝗋[exp a b]"
by blast
hence "Curry[exp a b ⊗ ℐ, a, b]
((eval a b ⋅ (exp a b ⊗ eval a a) ⋅ 𝖺[exp a b, exp a a, a]) ⋅
((exp a b ⊗ Id a) ⊗ a)) =
𝗋[exp a b]"
using assms 1 Curry_Uncurry runit_in_hom by force
thus ?thesis
by presburger
qed
finally have "𝗋[exp a b] ⋅
(Comp a a b ⋅ (exp a b ⊗ Id a) ⊗ ℐ) ⋅ inv 𝖺[exp a b, ℐ, ℐ] =
𝗋[exp a b] ⋅ (exp a b ⊗ ι)"
by blast
hence "(Comp a a b ⋅ (exp a b ⊗ Id a) ⊗ ℐ) ⋅ inv 𝖺[exp a b, ℐ, ℐ] =
exp a b ⊗ ι"
using assms ide_exp iso_cancel_left [of "𝗋[exp a b]"] iso_runit by fastforce
thus ?thesis
by (metis assms(1-2) 0 R.as_nat_trans.is_natural_1 comp_assoc_assoc'(2)
ide_exp ide_unity in_homE comp_assoc)
qed
qed
qed
lemma Comp_unit_left:
assumes "ide a" and "ide b" and "ide c"
shows "«Comp a b b ⋅ (Id b ⊗ exp a b) : ℐ ⊗ exp a b → exp a b»"
and "Comp a b b ⋅ (Id b ⊗ exp a b) = 𝗅[exp a b]"
proof -
show 0: "«Comp a b b ⋅ (Id b ⊗ exp a b) : ℐ ⊗ exp a b → exp a b»"
using assms ide_exp by simp
show "Comp a b b ⋅ (Id b ⊗ exp a b) = 𝗅[exp a b]"
proof (intro lunit_eqI)
show "«Comp a b b ⋅ (Id b ⊗ exp a b) : ℐ ⊗ exp a b → exp a b»"
by fact
show "ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b) = (ι ⊗ exp a b) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, exp a b]"
proof -
have "𝗅[exp a b] ⋅ (ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b] =
𝗅[exp a b] ⋅ ((ℐ ⊗ Comp a b b) ⋅ (ℐ ⊗ Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b]"
using assms 0 interchange [of ℐ ℐ "Comp a b b" "Id b ⊗ exp a b"] by auto
also have "... = (𝗅[exp a b] ⋅ (ℐ ⊗ Comp a b b)) ⋅
(ℐ ⊗ Id b ⊗ exp a b) ⋅ 𝖺[ℐ, ℐ, exp a b]"
using comp_assoc by simp
also have "... = (Comp a b b ⋅ 𝗅[exp b b ⊗ exp a b]) ⋅ (ℐ ⊗ Id b ⊗ exp a b) ⋅
𝖺[ℐ, ℐ, exp a b]"
using assms lunit_naturality
by (metis 0 Comp_simps(1-2) cod_comp in_homE)
also have "... = Comp a b b ⋅
(𝗅[exp b b ⊗ exp a b] ⋅ (ℐ ⊗ Id b ⊗ exp a b)) ⋅
𝖺[ℐ, ℐ, exp a b]"
using comp_assoc by simp
also have "... =
(Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝗅[ℐ ⊗ exp a b] ⋅ 𝖺[ℐ, ℐ, exp a b]"
using assms 0 lunit_naturality calculation in_homE comp_assoc by metis
also have "... = (Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ (ι ⊗ exp a b)"
using assms(1-2) ide_exp ide_unity lunit_eqI lunit_tensor' unit_in_hom_ax
unit_triangle(2)
by presburger
also have "... = 𝗅[exp a b] ⋅ (ι ⊗ exp a b)"
proof (unfold Comp_def)
have "(Curry[exp b b ⊗ exp a b, a, b]
(eval b b ⋅ (exp b b ⊗ eval a b) ⋅ 𝖺[exp b b, exp a b, a]) ⋅
(Id b ⊗ exp a b)) ⋅
(ι ⊗ exp a b) =
Curry[ℐ ⊗ exp a b, a, b]
((eval b b ⋅ (exp b b ⊗ eval a b) ⋅ 𝖺[exp b b, exp a b, a]) ⋅
((Id b ⊗ exp a b) ⊗ a)) ⋅
(ι ⊗ exp a b)"
proof -
have "«eval b b ⋅ (exp b b ⊗ eval a b) ⋅ 𝖺[exp b b, exp a b, a]
: (exp b b ⊗ exp a b) ⊗ a → b»"
using assms ide_exp tensor_in_hom ide_in_hom ide_exp eval_in_hom⇩E⇩C⇩M⇩C
by force
moreover have "«Id b ⊗ exp a b : ℐ ⊗ exp a b → exp b b ⊗ exp a b»"
using assms ide_exp by force
ultimately show ?thesis
using assms comp_Curry_arr by force
qed
also have "... = Curry[ℐ ⊗ exp a b, a, b]
(eval b b ⋅ ((exp b b ⊗ eval a b) ⋅ (Id b ⊗ exp a b ⊗ a)) ⋅
𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
using assms assoc_naturality [of "Id b" "exp a b" a] ide_exp comp_assoc
by force
also have "... = Curry[ℐ ⊗ exp a b, a, b]
((eval b b ⋅ (Id b ⊗ Uncurry a b (exp a b))) ⋅
𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
by (simp add: assms Uncurry_exp comp_cod_arr comp_assoc interchange)
also have "... = Curry[ℐ ⊗ exp a b, a, b]
((eval b b ⋅ (Id b ⊗ eval a b)) ⋅ 𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
using assms comp_arr_dom
by (metis eval_in_hom⇩E⇩C⇩M⇩C in_homE)
also have "... = Curry[ℐ ⊗ exp a b, a, b]
(((eval b b ⋅ (Id b ⊗ b)) ⋅ (ℐ ⊗ eval a b)) ⋅ 𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
proof -
have "Id b ⊗ eval a b = (Id b ⊗ b) ⋅ (ℐ ⊗ eval a b)"
using assms interchange
by (metis Id_simps(1-2) comp_arr_dom comp_ide_arr eval_in_hom⇩E⇩C⇩M⇩C
ide_in_hom seqI')
thus ?thesis using comp_assoc by simp
qed
also have "... = Curry[ℐ ⊗ exp a b, a, b]
((𝗅[b] ⋅ (ℐ ⊗ eval a b)) ⋅ 𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
using assms Id_def Uncurry_Curry lunit_in_hom ide_unity by simp
also have "... = Curry[ℐ ⊗ exp a b, a, b]
(eval a b ⋅ 𝗅[exp a b ⊗ a] ⋅ 𝖺[ℐ, exp a b, a]) ⋅
(ι ⊗ exp a b)"
using assms lunit_naturality eval_in_hom⇩E⇩C⇩M⇩C in_homE lunit_naturality
comp_assoc
by metis
also have "... = Curry[ℐ ⊗ exp a b, a, b]
(Uncurry[a, b] 𝗅[exp a b]) ⋅ (ι ⊗ exp a b)"
using assms ide_exp lunit_tensor' by force
also have "... = 𝗅[exp a b] ⋅ (ι ⊗ exp a b)"
using assms Curry_Uncurry lunit_in_hom ide_exp by auto
finally show "(Curry[exp b b ⊗ exp a b, a, b]
(eval b b ⋅ (exp b b ⊗ eval a b) ⋅ 𝖺[exp b b, exp a b, a]) ⋅
(Id b ⊗ exp a b)) ⋅
(ι ⊗ exp a b) =
𝗅[exp a b] ⋅ (ι ⊗ exp a b)"
by blast
qed
finally have 1: "𝗅[exp a b] ⋅
(ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b] =
𝗅[exp a b] ⋅ (ι ⊗ exp a b)"
by blast
have "(ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b] =
(inv 𝗅[exp a b] ⋅ 𝗅[exp a b]) ⋅
(ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b]"
using assms comp_cod_arr by simp
also have "... = (inv 𝗅[exp a b] ⋅ 𝗅[exp a b]) ⋅ (ι ⊗ exp a b)"
using 1 comp_assoc by simp
also have "... = ι ⊗ exp a b"
using assms comp_cod_arr [of "ι ⊗ exp a b" "𝗅⇧-⇧1[exp a b] ⋅ 𝗅[exp a b]"] arrI
by auto
finally have "(ℐ ⊗ Comp a b b ⋅ (Id b ⊗ exp a b)) ⋅ 𝖺[ℐ, ℐ, exp a b] =
ι ⊗ exp a b"
by blast
thus ?thesis
using assms(1-2) 0 L.as_nat_trans.is_natural_1 comp_assoc_assoc'(1)
ide_exp ide_unity in_homE comp_assoc
by metis
qed
qed
qed
lemma Comp_assoc⇩E⇩C⇩M⇩C:
assumes "ide a" and "ide b" and "ide c" and "ide d"
shows "«Comp a b d ⋅ (Comp b c d ⊗ exp a b) :
(exp c d ⊗ exp b c) ⊗ exp a b → exp a d»"
and "Comp a b d ⋅ (Comp b c d ⊗ exp a b) =
Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅ 𝖺[exp c d, exp b c, exp a b]"
proof -
show "«Comp a b d ⋅ (Comp b c d ⊗ exp a b) :
(exp c d ⊗ exp b c) ⊗ exp a b → exp a d»"
using assms by auto
show "Comp a b d ⋅ (Comp b c d ⊗ exp a b) =
Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅ 𝖺[exp c d, exp b c, exp a b]"
proof -
have 1: "Uncurry[a, d] (Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b]) =
Uncurry[a, d] (Comp a b d ⋅ (Comp b c d ⊗ exp a b))"
proof -
have "Uncurry[a, d]
(Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b]) =
Uncurry[a, d]
(Curry[exp c d ⊗ exp a c, a, d]
(eval c d ⋅ (exp c d ⊗ eval a c) ⋅ 𝖺[exp c d, exp a c, a]) ⋅
(exp c d ⊗ Comp a b c) ⋅ 𝖺[exp c d, exp b c, exp a b])"
using Comp_def by simp
also have "... = Uncurry[a, d]
(Curry[(exp c d ⊗ exp b c) ⊗ exp a b, a, d]
((eval c d ⋅ (exp c d ⊗ eval a c) ⋅ 𝖺[exp c d, exp a c, a]) ⋅
((exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b] ⊗ a)))"
using assms
comp_Curry_arr
[of a "(exp c d ⊗ Comp a b c) ⋅ 𝖺[exp c d, exp b c, exp a b]"
"(exp c d ⊗ exp b c) ⊗ exp a b" "exp c d ⊗ exp a c"
"eval c d ⋅ (exp c d ⊗ eval a c) ⋅ 𝖺[exp c d, exp a c, a]" d]
by auto
also have "... = eval c d ⋅(exp c d ⊗ eval a c) ⋅
(𝖺[exp c d, exp a c, a] ⋅ ((exp c d ⊗ Comp a b c) ⊗ a)) ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using assms Uncurry_Curry ide_exp interchange comp_assoc by simp
also have "... = eval c d ⋅
(exp c d ⊗ eval a c) ⋅
(𝖺[exp c d, exp a c, a] ⋅
((exp c d ⊗
Curry[exp b c ⊗ exp a b, a, c]
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a]))
⊗ a)) ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
unfolding Comp_def by simp
also have "... = eval c d ⋅
(exp c d ⊗ eval a c) ⋅
((exp c d ⊗
Curry[exp b c ⊗ exp a b, a, c]
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a])
⊗ a) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a]) ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using assms assoc_naturality [of "exp c d" _ a] Comp_def Comp_simps(1-3)
ide_exp ide_char
by (metis (no_types, lifting) mem_Collect_eq)
also have "... = eval c d ⋅
((exp c d ⊗ eval a c) ⋅
(exp c d ⊗
Curry[exp b c ⊗ exp a b, a, c]
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅ 𝖺[exp b c, exp a b, a])
⊗ a)) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using comp_assoc by simp
also have "... = eval c d ⋅
(exp c d ⊗
Uncurry[a, c]
(Curry[exp b c ⊗ exp a b, a, c]
(eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a]))) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using assms Comp_def Comp_in_hom interchange by auto
also have "... = eval c d ⋅
(exp c d ⊗ (eval b c ⋅ (exp b c ⊗ eval a b) ⋅
𝖺[exp b c, exp a b, a])) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using assms ide_exp tensor_in_hom ide_in_hom ide_exp eval_in_hom⇩E⇩C⇩M⇩C
assoc_in_hom Uncurry_Curry
by force
also have "... = eval c d ⋅
((exp c d ⊗ eval b c) ⋅
(exp c d ⊗ exp b c ⊗ eval a b) ⋅
(exp c d ⊗ 𝖺[exp b c, exp a b, a])) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using assms ide_exp tensor_in_hom interchange by auto
also have "... = eval c d ⋅
(exp c d ⊗ eval b c) ⋅
(exp c d ⊗ exp b c ⊗ eval a b) ⋅
(exp c d ⊗ 𝖺[exp b c, exp a b, a]) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
using comp_assoc by simp
finally have *: "Uncurry[a, d] (Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b]) =
eval c d ⋅
(exp c d ⊗ eval b c) ⋅
(exp c d ⊗ exp b c ⊗ eval a b) ⋅
(exp c d ⊗ 𝖺[exp b c, exp a b, a]) ⋅
𝖺[exp c d, exp b c ⊗ exp a b, a] ⋅
(𝖺[exp c d, exp b c, exp a b] ⊗ a)"
by blast
have "Uncurry[a, d] (Comp a b d ⋅ (Comp b c d ⊗ exp a b)) =
Uncurry[a, d]
(Curry[exp b d ⊗ exp a b, a, d]
(eval b d ⋅ (exp b d ⊗ eval a b) ⋅ 𝖺[exp b d, exp a b, a]) ⋅
(Comp b c d ⊗ exp a b))"
using Comp_def by simp
also have "... = Uncurry[a, d]
(Curry[(exp c d ⊗ exp b c) ⊗ exp a b, a, d]
(eval b d ⋅ (exp b d ⊗ eval a b) ⋅ 𝖺[exp b d, exp a b, a] ⋅
((Comp b c d ⊗ exp a b) ⊗ a)))"
proof -
have "«Comp b c d ⊗ exp a b :
(exp c d ⊗ exp b c) ⊗ exp a b → exp b d ⊗ exp a b»"
using assms ide_exp by force
moreover have "«eval b d ⋅ (exp b d ⊗ eval a b) ⋅ 𝖺[exp b d, exp a b, a]
: (exp b d ⊗ exp a b) ⊗ a → d»"
using assms ide_exp tensor_in_hom ide_in_hom ide_exp eval_in_hom⇩E⇩C⇩M⇩C
by force
ultimately show ?thesis
using comp_Curry_arr assms comp_assoc by auto
qed
also have "... = eval b d ⋅ (exp b d ⊗ eval a b) ⋅ 𝖺[exp b d, exp a b, a] ⋅
((Comp b c d ⊗ exp a b) ⊗ a)"
using assms ide_exp Uncurry_Curry by force
also have "... = eval b d ⋅
((exp b d ⊗ eval a b) ⋅ (Comp b c d ⊗ exp a b ⊗ a)) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
using assms ide_exp comp_assoc
assoc_naturality [of "Comp b c d" "exp a b" a]
by force
also have "... = eval b d ⋅ (Comp b c d ⊗ eval a b) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
by (simp add: assms comp_arr_dom comp_cod_arr interchange)
also have "... = eval b d ⋅
(Curry[exp c d ⊗ exp b c, b, d]
(eval c d ⋅ (exp c d ⊗ eval b c) ⋅ 𝖺[exp c d, exp b c, b])
⊗ eval a b) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
unfolding Comp_def by simp
also have "... = eval b d ⋅
((Curry[exp c d ⊗ exp b c, b, d]
(eval c d ⋅ (exp c d ⊗ eval b c) ⋅ 𝖺[exp c d, exp b c, b])
⊗ b) ⋅
((exp c d ⊗ exp b c) ⊗ eval a b)) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
by (metis (no_types, lifting) assms Comp_def Comp_simps(1-2)
comp_arr_dom comp_cod_arr eval_simps(1,3) interchange)
also have "... = Uncurry[b, d]
(Curry[exp c d ⊗ exp b c, b, d]
(eval c d ⋅ (exp c d ⊗ eval b c) ⋅ 𝖺[exp c d, exp b c, b])) ⋅
((exp c d ⊗ exp b c) ⊗ eval a b) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
using comp_assoc by simp
also have "... = eval c d ⋅
(exp c d ⊗ eval b c) ⋅
(𝖺[exp c d, exp b c, b] ⋅
((exp c d ⊗ exp b c) ⊗ eval a b)) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
using assms ide_exp Uncurry_Curry comp_assoc by auto
also have "... = eval c d ⋅
(exp c d ⊗ eval b c) ⋅
((exp c d ⊗ exp b c ⊗ eval a b) ⋅
𝖺[exp c d, exp b c, exp a b ⊗ a]) ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
using assoc_naturality [of "exp c d" "exp b c" "eval a b"]
by (metis assms arr_cod cod_cod Curry_in_hom dom_dom eval_in_hom⇩E⇩C⇩M⇩C
ide_exp in_homE)
also have "... = eval c d ⋅
(exp c d ⊗ eval b c) ⋅
(exp c d ⊗ exp b c ⊗ eval a b) ⋅
𝖺[exp c d, exp b c, exp a b ⊗ a] ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
using comp_assoc by simp
finally have **: "Uncurry[a, d] (Comp a b d ⋅ (Comp b c d ⊗ exp a b)) =
eval c d ⋅
(exp c d ⊗ eval b c) ⋅
(exp c d ⊗ exp b c ⊗ eval a b) ⋅
𝖺[exp c d, exp b c, exp a b ⊗ a] ⋅
𝖺[exp c d ⊗ exp b c, exp a b, a]"
by blast
show ?thesis
using * ** assms ide_exp pentagon by force
qed
have "Comp a b d ⋅ (Comp b c d ⊗ exp a b) =
Curry[(exp c d ⊗ exp b c) ⊗ exp a b, a, d]
(Uncurry[a, d] (Comp a b d ⋅ (Comp b c d ⊗ exp a b)))"
using assms ide_exp Curry_Uncurry by fastforce
also have "... = Curry[(exp c d ⊗ exp b c) ⊗ exp a b, a, d]
(Uncurry[a, d] (Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b]))"
using 1 by simp
also have "... = Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅
𝖺[exp c d, exp b c, exp a b]"
using assms ide_exp Curry_Uncurry by simp
finally show "Comp a b d ⋅ (Comp b c d ⊗ exp a b) =
Comp a c d ⋅ (exp c d ⊗ Comp a b c) ⋅ 𝖺[exp c d, exp b c, exp a b]"
by blast
qed
qed
end
end