高次射の定義の形式化

随伴に関する注意事項 - 檜山正幸のキマイラ飼育記で書いた、「構造か命題か」の問題があるので、構造としての随伴対は、adj(L -| R) と書いて、L -| R は命題として使うことにする。

ほんとは絵で描くのが良いのだが、なんとかアスキーで定義を書いてみる。ネタは、"バスケス-マルケス 2015"（https://arxiv.org/abs/1510.04724）の付録の定義群。

随伴系を対象とする2圏を 2Adj と書いて、随伴系（0-射）のあいだの射（1-射）を定義してみる。ここで：

• v⇒ ： 二重圏の2-射をストリング図で垂直方向（ペースティング図では斜め方向）に考えたもの。
• v= ： 二重圏の明示的等号である2-射（可換四角形）を垂直方向に考えたもの。
• α ←(v-inv)→β ： αとβは互いに垂直方向に逆。
• α ←(mate)→β ： αとβは互いにメイト対応している。
• L~ は、もとの論文ではオーバーライン

For L:X→C, L~:Y→D, R:C→D, R~:D→Y
Given L -| R, L~ -| R~
For J:C→D, K:X→Y, λ:: L*T v⇒ K*L~ : X→D
Given (R*K:: v= J*R~ :C→Y) ←(v-inv)→ (J*R~ v= R*K :C→Y) ←(mate)→ (λ:: L*T v⇒ K*L~ :X→D)
Define
  Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Ψ = (J, K,λ)
End

次のように書いても同じ。

For L:X→C, L~:Y→D, R:C→D, R~:D→Y
Given L -| R, L~ -| R~
Define
  Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Ψ = (J, K,λ)
Where
 J:C→D, K:X→Y, λ:: L*T v⇒ K*L~ : X→D
 SuchThat (R*K:: v= J*R~ :C→Y) ←(v-inv)→ (J*R~ v= R*K :C→Y) ←(mate)→ (λ:: L*T v⇒ K*L~ :X→D)
End

一応これで、随伴系のあいだの1-射 Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj は定義される。絵を描かないとピンとこないと思うが。

次に2-射 Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj を定義する。Ψ'の構成素は、Ψの構成素（名）にすべてダッシュを付けたやつとする。

For α::J v⇒ J':C→D, β::K v⇒ K':X→Y
Given (λ;β)*L~ = (L*β);λ' :: L*T v⇒ K'*L~ : X→D
Define
  Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Γ = (α, β)
End

あるいは、

Define
  Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Γ = (α, β)
Where
  α::J v⇒ J':C→D, β::K v⇒ K':X→Y
  SuchThat (λ;β)*L~ = (L*β);λ' :: L*T v⇒ K'*L~ : X→D
End

ある程度は形式化した書き方が出来る。