失敗録:Δで考えると向き辻褄が合わない→トレースだ！
豊穣圏とか考えてたとき
内部hom函手でも困ってた
モノイダル閉圏における指数随伴系の自然性
内部homを用いた随伴系の自然同型
対角函手だとopの辻褄が合わない
トレースみたいなのを定義してやればいいのでは？
δ_A: %I -> A^op × A
F: A^op × A ->
$ \forall a,
そもそも圏論の等式についてを疎かにしているのが露呈している
code:enriched_category.sig
sig EnrichedCategory in CAT @ %
Data
-1-sig
MonoidalCategory V ⊗ i α λ ρ
%0-morph
.0-morph @ Ob : Class
%1-morph
hom : Ob^op × Ob -> V
ここと
code:enriched_category.sig
%2-morph
"identity element" @ id
: ! * i => Δ * hom
: Ob -> V
ここ
code:enriched_category.sig
"composition morphism" @ comp
: Ob^ × Δ × Ob^ ; hom ⊗ hom
=> Ob^ × ! × Ob^ ; hom
: Ob × Ob × Ob -> V
Axioms
%3-eq "associative"
comp ⊗ hom^; comp
=(hom×hom×hom)α; hom^ ⊗ comp; comp
: Ob^ × Δ × Δ × Ob^; (hom⊗hom)⊗hom
=> Ob^ × ! × ! × Ob^ ; hom
: Ob × Ob × Ob × Ob -> V
%3-eq "left unital"
: ⊗ hom